Stella Spadoni
You can reach me at stella.spadoni[0x40]imtlucca.it
About me 
Currently a PhD student at IMT School for Advanced Studies Lucca, Italy, supervised by Cosimo Perini Brogi. Coming from a bachelor’s in Philosophy and a master’s in Logic – see here for more.
💾 MEMORY CARD:
• PLAY TIME: 2025 - 2028
• LAST LOG: Ongoing.
• PLAY TIME: 2022 - 2024
• LAST LOG: THE FERTILE STEPPE: COMPUTABILITY LOGIC AND THE DECIDABILITY OF ONE OF ITS FRAGMENTS. Supervisor: Pierluigi Minari. Co-supervisor: Andrea Cantini.
• PLAY TIME: 2019 - 2022
• LAST LOG: "THE ELEGANT VERSATILE BRAIN": A LOGICAL AND PHILOSOPHICAL TAKE ON THE UNIVERSAL TURING MACHINE. Supervisor: Andrea Cantini. Co-supervisor: Sergio Bernini.
Publications
-
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 prominence 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 reasoning 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 successful 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.
Presented at ITASEC-SERICS 2026 - Joint National Conference on CyberSecurity.
Master’s thesis
-
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.
Conference talks
- “On decidability and bounded proofs in fragments of computability logic”, S. Spadoni, Cosimo Perini Brogi. Presented at the Logic Colloquium 2026 (in conjunction with the British Logic Colloquium 2026), 29 June - 3 July 2026, Swansea University, Wales, UK;
- “On protocol security via computability logic”, Cosimo Perini Brogi, S. Spadoni, R. De Nicola. Presented at the Logic Colloquium 2026 (in conjunction with the British Logic Colloquium 2026), 29 June - 3 July 2026, Swansea University, Wales, UK;
- “Cutting Out the Middle Man: A Game-Theoretic Analysis in Computability Logic of the Needham-Schroeder Protocol”, Cosimo Perini Brogi, S. Spadoni. Presented at ITASEC-SERICS 2026 - Joint National Conference on CyberSecurity, 9 – 13 February 2026, Cagliari, Facoltà di Ingegneria e Architettura, Piazza D’Armi, Sardinia, Italy.
seevee !
An institution-driven logbook of pursued directions. Extracting it to your local storage device will alter your current inventory space.
(Don't turn off the lights)