Security Protocols: Modelling and Verification - 2026

Instructor:
Cătălin Bîrjoveanu (catalin.birjoveanu@uaic.ro)
Objectives:
  • Understanding the need of formal methods for modeling and verification of security protocols
  • Acquiring the major modeling and verification techniques for security protocols
  • Using the studied techniques to verify various security protocols
  • Analyzing the correctness of security protocols by using specific verification tools
  • Implementing/developing tools for verifying security protocols
Topics:
  • Introduction in Modeling and Verification of Security Protocols
  • Security Protocol Attacks:
    • Design Attacks
    • Implementation Attacks
  • Secure Design Principles for Security Protocols
  • Formal Methods for Security Protocols Verification
  • AVISPA (Automated Validation of Internet Security Protocols and Applications)
  • Automated Verification of Multi-Party E-Commerce Protocols
  • Verification of Security Protocols Using Hybrid Techniques
    • Specification, Verification, Scyther
  • Type Flaw Attacks, Tagging Schemes
  • Multi-Protocol Attacks
  • Security Protocols Verification Using Tamarin
  • ProVerif (Automatic Cryptographic Protocol Verifier)
Labs:

Lab exercises that help to understand the principles of secure design of security protocols, techniques and tools to verify various security protocols and apply them to prevent attacks on security protocols. The objective of the exercises is to analyze the correctness of the security protocols both from the point of view of their design and implementation. The focus of the exercises is the application of representative techniques and tools, widely used in the field of security protocols verification: CL-AtSe from AVISPA, Scyther, Tamarin Prover, ProVerif. The exercises using CL-AtSe model checker, Scyther tool, Tamarin prover and ProVerif aim understanding in depth the way in which a security protocol must be built starting from a set of security objectives, the causes of the attacks on security protocols, multi-protocol attacks, and the impact of these attacks.


Lecture Notes References
Introduction in Modeling and Verification of Security Protocols
Whiteboard
Security Protocol Attacks
Whiteboard 		V. Cortier, S. Delaune, P. Lafourcade, A Survey of Algebraic Properties Used in Cryptographic Protocols, Journal of Computer Security, 2006.
AVISPA - Automated Validation of Internet Security Protocols and Applications
Whiteboard 		The Avispa Team, HLPSL Tutorial, 2006.
The Avispa Team, AVISPA v1.1 User Manual, 2006.
Automated Verification of Multi-Party E-Commerce Protocols (I) C. V. Bîrjoveanu and M. Bîrjoveanu, Secure Multi-Party E-Commerce Protocols, SpringerBriefs in Computer Science. Springer, Cham, 2022.
C. V. Bîrjoveanu and M. Bîrjoveanu, Automated Verification of E-Commerce Protocols for Complex Transactions, E-Business and Telecommunications. Communications in Computer and Information Science, vol. 1118 CCIS. Springer, Cham, 2019.
Automated Verification of Multi-Party E-Commerce Protocols (II)
Verification of Security Protocols using Hybrid Techniques (I) C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography series, Springer, 2012, Chapters 3, 4.
Verification of Security Protocols using Hybrid Techniques (II) C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography series, Springer, 2012, Chapter 5.
Security Protocol Verification Techniques
Type Flaw and Multi-Protocol Attacks C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography series, Springer, 2012, Chapter 6.
B. Blanchet, A. Podelski, Verification of Cryptographic Protocols: Tagging Enforces Termination, FoSSaCS 2003.
Modeling and Verifying Security Protocols Using Tamarin (I) Tamarin Prover, 2026.
Modeling and Verifying Security Protocols Using Tamarin (II)

Labs References
Security Protocol Attacks
Whiteboard
SPAN and AVISPA
Whiteboard 		AVISPA, Lecture Notes.
AVISPA: Specification and Verification (I)
Whiteboard
AVISPA: Specification and Verification (II)
Whiteboard
Verification of Security Protocols using CL-AtSe
Scyther: Installation, Modeling and Verification Verification of Security Protocols using Hybrid Techniques. Lecture Notes.
C. Cremers, Scyther User Manual, 2026.
Design and Verification of Security Protocols Using Scyther
Scyther: Modeling and Verification of the Diffie-Hellman Key Establishment Protocol
Exercises
Tamarin Prover: Installation, Modeling and Verification Modeling and Verifying Security Protocols Using Tamarin. Lecture Notes.
Tamarin Prover: Modeling and Verification
Scores