Paolo Modesti

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], Java
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

Publications

Journals
- Chidimma Opara, Paolo Modesti and Lewis Golightly
  Evaluating spam filters and Stylometric Detection of AI-generated phishing emails
  Expert Systems with Applications, 127044, 2025
- Rémi Garcia and 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 and 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 and 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, and 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 and 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 and 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 and 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 and Paolo Modesti
  Security Protocol Specification and Verification with AnBx
  Journal of Information Security and Applications (JISA), Volume 30, October 2016, pp. 46–63, preprint
Book Chapters
- Paolo Modesti and 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
Conferences and Workshops
- Rémi Garcia and 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 and 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 and 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 and 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
- 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, and 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
- 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 and 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 and 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
PhD Thesis
- Paolo Modesti
  Verified Security Protocol Modeling and Implementation with AnBx
  Università Ca' Foscari Venezia, 2012
Technical Reports
- Michele Bugliesi, Stefano Calzavara, Sebastian Mödersheim, and Paolo Modesti
  Security Protocol Specification and Verification with AnBx
  Technical Report CS-TR-1479, School of Computing Science, Newcastle University, 2015
- 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
- Michele Bugliesi and Paolo Modesti
  Design and Analysis of Distributed Protocols with AnBx
  Technical Report DSI CS-2010-04, Università Ca' Foscari Venezia, 2010
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)