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
- 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
Conferences and Workshops
- 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)