You can reach me at stella.spadoni@imtlucca.it
Currently a PhD student at IMT School of Advanced Studies Lucca, Italy, supervised by Cosimo Perini Brogi. Coming from a bachelor’s in philosophy and an master’s in logic – see here for more.
Joint work with Cosimo Perini Brogi.
Cryptographic protocols constitute the cornerstone of secure communication in open distributed systems. The systematic formal verification of such protocols gained promi- nence following Gavin Lowe’s 1995 discovery of a structural flaw in the classical Needham- Schroeder Public Key protocol from 1978. This paper presents a novel formal analysis of such protocol through Computability Logic (CoL), a game-theoretic semantics and reason- ing system that models interaction between an honest agent and a hostile environment. By formalising the protocol’s execution as a game specified in the CoL fragment CL4, we demonstrate that the original vulnerability allows the environment to employ a suc- cessful Copycat Strategy isomorphic to the standard Man-in-the-Middle attack (MitM). Conversely, we prove that the revised protocol including Lowe’s fix effectively breaks this adversarial advantage, guaranteeing security against the MitM.
To be presented at ITASEC 2026.
The Fertile Steppe: Computability Logic and the decidability of one of its fragments
The present work is devoted to Computability Logic (CoL), the young and volcanic research-project developed by Giorgi Japaridze. Our main goal is to provide the reader with a clear panoramic view of this vast new land, starting from its core knots and making our way towards the outer threads, in a somewhat three-dimensional, spacial gait. Furthermore, through the present work, we provide a tentative proof for the decidability of one of CoL’s numerous axiomatisations, namely CL15. Thus, our expedition initially takes off for an aerial, perusal overview of this fertile steppe. The first chapter introduces CoL in a philosophical fashion, exposing and arguing its main key points. We then move over to unfold its semantics and syntax profiles, allowing the reader to become increasingly more familiar with this new environment. Landing on to the second chapter, we thoroughly introduce Cirquent Calculus, the new deductive system Japaridze has developed in order to axiomatise Computability Logic. Indeed, this new proof-system can also be a useful tool for many other logics. We then review each of the 17 axiomatisations found so far. The third chapter zooms-in on CL15, in order to come up with a possible solution to its open problem. We outline its soundness and completeness proofs; then provide some few deductive examples; and, finally, build a tentative proof of its decidability. Lastly, the fourth chapter focuses on the potential and actual applications of Computability Logic, both in arithmetic (clarithmetic) and in Artificial Intelligence systems (meaning knowledgebase and planning-and-action ones). We close our journey with some final remarks on the richness of this framework and, hence, the research-worthiness it entails.