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
- 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
- Victor Chang, Lewis Golightly, Paolo Modesti, Qianwen A. Xu, Le M.T.
Doan, Karl Hall, Sreeja Boddu and Anna Kobusińska
- 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
- Abdulaziz Almehrej, Leo Freitas and Paolo Modesti
- 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, 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
- Michele Bugliesi, Stefano Calzavara, Sebastian Mödersheim, and
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)