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
-
On decidability and bounded proofs in fragments of computability logic
Joint work with Cosimo Perini Brogi.
Computability logic (CoL) reinterprets logic as a formal theory of dynamic interaction, modelling statements as computational games between predefined agents M and E. The present work tackles two open problems regarding CoL fragments CL15 and CL5. Firstly, we prove CL15 decidable: the potentially infinite search space from resource contraction can be pruned while preserving completeness, bounding contraction applications through a function of the cirquent’s complexity. Secondly, we develop a novel and purely syntactic proof that any derivable cirquent in the duplication-free version of CL5 admits a polynomial-size derivation, bounded by three structural limits (width, branch length and node size) in the bottom-up proof construction.
Presented at Logic Colloquium 2026. To appear in The Bulletin of Symbolic Logic.
-
On protocol security via computability logic
Joint work with Cosimo Perini Brogi and Rocco De Nicola.
Experience in cybersecurity shows that communication protocol design is exceptionally error-prone: security weaknesses often arise less from defects in cryptographic primitives than from flawed protocols, owing to the incorrect logical interplay among agents and potential adversaries in a network. Empirical evidence likewise suggests that `verification is only as sound as the language we used for it’. We propose computability logic (CoL) as a formal foundation for modelling, analysing and verifying secure communication protocols by treating specifications as interactive games between computational agents. We argue that CoL naturally captures protocol dynamics and formally identifies structural invariants that underlie classes of vulnerabilities and attacks. Moreover, its constructive character favours automated strategy extraction and synthesis of correct-by-construction executable artefacts from verification proofs while preserving the game-theoretic, interactive nature of protocols. We consider a CL4-based case study we presented at ITASEC 2026 to show the feasibility of our approach on representative protocol patterns, and outline theoretical and practical directions for extending the method to broader protocol families. This work in progress aims to advance logical verification methods for real-world secure communication.
Presented at Logic Colloquium 2026. To appear in The Bulletin of Symbolic Logic.
-
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
- “A Decision Algorithm for the CL15 Fragment of Computability Logic”, S. Spadoni. Presented at Women in Logic 2026 @ FLoC’26: the 9th Federated Logic Conference, 24 – 25 July 2026, Instituto Universitário de Lisboa, Portugal;
- “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)