I am a Senior Lecturer in Cybersecurity at Teesside University. My research focuses on the formal verification of security protocols, code generation for security-critical systems, and language-based security.
I build tools - most notably the AnBx compiler - that let protocol designers go from verified models to running implementations.
Selected publications:
- Global Surveillance Under the Lens: Reconstructing Passive Dolev-Yao Intruders — arXiv 2611.07170, 2026
- Security Analysis of the Open Banking Account and Transaction API Protocol — Cyber Security and Applications, 2025
- Automatic Generation of Security Protocols Attacks Specifications and Implementations — Cyber Security and Applications, 2024
- From provable models to provable implementations: translating Alice & Bob security protocols to F* — International Symposium on Foundations & Practice of Security (FPS 2025), 2025
- Evaluating Large Language Models for Symbolic Security Protocol Analysis — Electronics, 2026
Tools
- AnBx Compiler and Code Generator
(v. )
Security Protocols Specification, Verification and Implementation
Features- AnBx to AnB compiler for verification (requires the OFMC model-checker)
- Java code generator from AnBx or AnB specification
- Java library for security (AnBxJ)
- Output formats: AnB, Executable Narrations, Optimized Executable Narrations, Applied-Pi [ProVerif], F*/DY*, Java, VDM-SL
The AnBx compiler has been mentioned in the High Assurance News, July 2014, Compiler Verification by Nick P, on the Schneier on Security blog.
- AnBx IDE
Eclipse plugin supporting the AnBx/AnB language and security protocols verification tools (OFMC, ProVerif) - Android Scripts
A Script-Based Approach for Teaching and Assessing Android Application Development - SPS/APS and APCC: Protocols, Typing, and Composition
A novel tool suite by Omar Almousa, Sebastian Mödersheim, Paolo Modesti, and Luca Viganò. - download
includes APCC (Automatic Protocol Composition Checker): for a given set of protocols checks that the sufficient conditions of [AMMV15] for typing and parallel composition are met. - Moreover, I contributed to the development of:
- OFMC (Open-Source Fixed-Point Model-Checker)
- Classic AIF Framework (Set-based abstraction) - download
- LightCross: A Lightweight Smart Contract Vulnerability Detection Tool - download
Publications
Jump to:
Pre-Prints ·
Journals ·
Book Chapters ·
Conferences and Workshops ·
PhD Thesis ·
Technical Reports ·
Project Deliverables
Filter by topic:
- Pre-Prints
- Paolo Modesti
Global Surveillance Under the Lens: Reconstructing Passive Dolev-Yao Intruders
arXiv 2611.07170, 2026
- Paolo Modesti
- Journals
- Lewis Golightly, Paolo Modesti, Jie Li
Secure Consensus in Distributed Systems: Raft Protocol with Hybrid Cryptography
Electronics, Volume 15, no. 20, 4747, 2026 - Paolo Modesti, Syed Ahmed, Ioannis Sfyrakis, Derek Enodolomwanyi
Evaluating Large Language Models for Symbolic Security Protocol Analysis
Electronics, Volume 15, no. 18, 4141, 2026 - Joshua Dowrick, Paolo Modesti, Benjamin Findlay
Android anti-forensics: A systematic review of applications, techniques, and investigative challenges
Forensic Science International: Digital Investigation, Volume 58, 302159, 2026 - Ioannis Sfyrakis, Paolo Modesti, Lewis Golightly, Minaro Ikegima
LightCross: A Lightweight Smart Contract Vulnerability Detection Tool
Computers, Volume 14, no. 3, 369, 2025 - Paolo Modesti, Leo Freitas, Qudus Shotomiwa, Abdulaziz Almehrej
Security Analysis of the Open Banking Account and Transaction API Protocol
Cyber Security and Applications, Volume 3, December 2025, 100097, 2025 - Chidimma Opara, Paolo Modesti, Lewis Golightly
Evaluating spam filters and Stylometric Detection of AI-generated phishing emails
Expert Systems with Applications, Volume 276, 127044, 2025 - Rémi Garcia, Paolo Modesti
A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols
Electronics, Volume 13, no. 23, 4660, 2024, extended version - Paolo Modesti, Lewis Golightly, Louis Holmes, Chidimma Opara, Marco Moscini
Bridging the Gap: A Survey and Classification of Research-Informed Ethical Hacking Tools
Journal of Cybersecurity and Privacy, Volume 4, no. 3: 410–448, 2024, extended version - Rémi Garcia, Paolo Modesti
Automatic Generation of Security Protocols Attacks Specifications and Implementations
Cyber Security and Applications, Volume 2, January 2024, 1000138, 2024 - Lewis Golightly, Paolo Modesti, Victor Chang
Deploying Secure Distributed Systems: Comparative Analysis of GNS3 and SEED Internet Emulator
Journal of Cybersecurity and Privacy, Volume 3, no. 3: 464–492, 2023 - Lewis Golightly, Paolo Modesti, Rémi Garcia, Victor Chang
Securing Distributed Systems: A Survey on Access Control Techniques for Cloud, Blockchain, IoT and SDN
Cyber Security and Applications, Volume 1, December 2023, 100015, 2023 - Victor Chang, Lewis Golightly, Paolo Modesti, Qianwen A. Xu, Le M.T. Doan, Karl Hall, Sreeja Boddu, Anna Kobusińska
A Survey on Intrusion Detection Systems for Fog and Cloud Computing
Future Internet, Volume 14, no. 3:89, 2022 - Paolo Modesti, Siamak F. Shahandashti, Patrick McCorry, Feng Hao
Formal Modelling and Security Analysis of Bitcoin's Payment Protocol
Computers & Security, Volume 107, August 2021, 2021, preprint - Paolo Modesti
A Script-Based Approach for Teaching and Assessing Android Application Development
ACM Transactions on Computing Education, Volume 21 Issue 1, 2021, preprint - Paolo Modesti
Integrating Formal Methods for Security in Software Security Education
Informatics in Education, Volume 19 Issue 3, 2020, pp. 425–454 - Michele Bugliesi, Stefano Calzavara, Sebastian Mödersheim, Paolo Modesti
Security Protocol Specification and Verification with AnBx
Journal of Information Security and Applications (JISA), Volume 30, October 2016, pp. 46–63, preprint
- Lewis Golightly, Paolo Modesti, Jie Li
- Book Chapters
- Paolo Modesti, Rémi Garcia
Formal Modeling and Security Analysis of Security Protocols
in Handbook of Formal Analysis and Verification in Cryptography, pp. 213–274, 1st edition, CRC Press, eBook ISBN 9781003090052, 2023, preprint
- Paolo Modesti, Rémi Garcia
- Conferences and Workshops
- Rémi Garcia, Paolo Modesti, Leo Freitas
From provable models to provable implementations: translating Alice & Bob security protocols to F*
International Symposium on Foundations & Practice of Security (FPS 2025), Brest, France, 2025, accepted paper - Paolo Modesti
A Model-Driven Approach for Energy-Aware and Configurable Security Protocols in Smart Digital Systems
International Symposium on Smart Energy, Materials, Manufacturing and Digital Technologies (ISSMART 2025), Middlesbrough, UK, 2025 (oral presentation) - Rémi Garcia, Paolo Modesti
Automatic Generation of Security Protocols Attacks Specifications and Implementations
17th Workshop on Programming Languages and Analysis for Security (PLAS 2022), Virtual, 2022 (journal paper) - Abdulaziz Almehrej, Leo Freitas, Paolo Modesti
Account and Transaction Protocol of the Open Banking Standard
International Conference on Rigorous State-Based Methods (ABZ 2020), Ulm, Germany, 2020, preprint - Leo Freitas, Paolo Modesti, Martin Emms
A Methodology for Protocol Verification Applied to EMV® 1
21st Brazilian Symposium on Formal Methods (SBMF 2018), Salvador, Brazil, 2018, preprint - Rémi Garcia, Paolo Modesti
An IDE for the Design, Verification and Implementation of Security Protocols
IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW 2017) – AFFORD'17, Toulouse, France, 2017, preprint - Paolo Modesti
Security Programming with High-Level Abstractions: a Tutorial (Extended Abstract)
HEA National Conference on Learning and Teaching in Cybersecurity, Birmingham, UK, 2016, extended abstract - Paolo Modesti
AnBx: Automatic Generation and Verification of Security Protocols Implementations
International Symposium on Foundations & Practice of Security (FPS 2015), Clermont-Ferrand, France, 2015, preprint - Omar Almousa, Sebastian Mödersheim, Paolo Modesti, Luca Viganò
Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment
European Symposium on Research in Computer Security (ESORICS 2015), Vienna, Austria, 2015, extended version - Paolo Modesti
Automatic Generation of Security Protocols Implementations (Extended Abstract)
4th Cryptoforma Workshop at CSF (informal proceedings), Verona, Italy, 2015, extended abstract - Paolo Modesti
Efficient Java Code Generation of Security Protocols specified in AnB/AnBx
Workshop on Security and Trust Management (STM 2014), Wroclaw, Poland, 2014, preprint - Sebastian Mödersheim, Paolo Modesti
Verifying SeVeCom Using Set-based Abstraction
7th IEEE International Wireless Communications and Mobile Computing Conference (IWCMC 2011), Vehicular Communications Symposium, Istanbul, Turkey, 2011, preprint - Michele Bugliesi, Paolo Modesti
AnBx - Security Protocols Design and Verification
Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS 2010), Paphos, Cyprus, 2010, preprint
- Rémi Garcia, Paolo Modesti, Leo Freitas
- PhD Thesis
- Paolo Modesti
Verified Security Protocol Modeling and Implementation with AnBx
Università Ca' Foscari Venezia, 2012
- Paolo Modesti
- Technical Reports
- Michele Bugliesi, Stefano Calzavara, Sebastian Mödersheim, Paolo Modesti
Security Protocol Specification and Verification with AnBx
Technical Report CS-TR-1479, School of Computing Science, Newcastle University, 2015, PDF - Paolo Modesti
Efficient Java Code Generation of Security Protocols specified in AnB/AnBx
Technical Report CS-TR-1422, School of Computing Science, Newcastle University, 2014, PDF - Michele Bugliesi, Paolo Modesti
Design and Analysis of Distributed Protocols with AnBx
Technical Report DSI CS-2010-04, Università Ca' Foscari Venezia, 2010
- Michele Bugliesi, Stefano Calzavara, Sebastian Mödersheim, Paolo Modesti
- Project Deliverables
- FutureID, D12.3 Security Evaluation of FutureID, 2015 (lead author)
- FutureID, D12.9 Recommendations and Future Work, 2015 (contributor)
- FutureID, D24.4 Third Report on Research on Protocols and Tools for Future eID Solutions, 2015 (contributor)
- FutureID, D42.8 Development of APS-files for selected authentication protocols, 2015 (contributor)
- FutureID, D24.2 Second Report on Research on Protocols and Tools for Future eID Solutions, 2014 (contributor)