Security Protocols: Modelling and Verification - 2025

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 of Security Protocols
  • Formal Methods for Security Protocols Verification
  • AVISPA (Automated Validation of Internet Security Protocols and Applications) Tool:
    • High Level Protocol Specification Language
    • AVISPA Back-ends
    • Security Protocols Verification using CL-AtSe (Constraint-Logic-based Attack Searcher)
  • 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
  • Tamarin
    • Modeling of Security Protocols
    • Specifying Trace Properties
    • 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 		Veronique Cortier, Stephanie Delaune, Pascal 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ătălin V. Bîrjoveanu and Mirela Bîrjoveanu, Secure Multi-Party E-Commerce Protocols, SpringerBriefs in Computer Science. Springer, Cham, 2022.
Cătălin V. Bîrjoveanu and Mirela 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) Cas Cremers, Sjouke 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) Cas Cremers, Sjouke 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 Cas Cremers, Sjouke Mauw, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography series, Springer, 2012, Chapter 6.
Bruno Blanchet, Andreas Podelski, Verification of Cryptographic Protocols: Tagging Enforces Termination, FoSSaCS 2003.
James Heather, Gavin Lowe, Steve Schneider, How to Prevent Type Flaw Attacks on Security Protocols, CSFW 2000.
Modeling and Verifying Security Protocols Using Tamarin (I) Tamarin Prover, 2024.
Modeling and Verifying Security Protocols Using Tamarin (II)

Labs References
Heartbleed Attack Lab Setup
SPAN and AVISPA
Whiteboard 		AVISPA, Lecture Notes.
AVISPA: Specification and Verification (I)
Whiteboard
AVISPA: Specification and Verification (II)
Whiteboard
Exercises
Design and Verification of Security Protocols using CL-AtSe
Scyther: Installation, Modeling and Verification Scyther v1.1.3.
Verification of Security Protocols using Hybrid Techniques. Lecture Notes.
Scyther: Modeling and Verification of the Diffie-Hellman Key Establishment Protocol
Tamarin Prover: Installation, Modeling and Verification Modeling and Verifying Security Protocols Using Tamarin. Lecture Notes.
Scyther: Type Flaw and Multi-Protocol Attacks Type Flaw and Multi-Protocol Attacks. Lecture Notes.