Security Protocols: Modelling and Verification - 2019


Objectives:



Lecture Notes References
Introduction
Security Protocol Attacks Veronique Cortier, Stephanie Delaune, Pascal Lafourcade, A Survey of Algebraic Properties Used in Cryptographic Protocols, Journal of Computer Security, 2006.
Strand Spaces F. Javier Thayer Fabrega, Jonathan C. Herzog, Joshua D. Guttman, Strand Spaces: Proving Security Protocols Correct, Journal of Computer Security, 1999.
Security Protocols Verification using Strand Spaces
Verification of E-Commerce Protocols
Verification of Multi-Party E-Commerce Protocols
Operational Semantics, Security Properties 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 Cas Cremers, Sjouke Mauw, Operational Semantics and Verification of Security Protocols, Information Security and Cryptography series, Springer, 2012, Chapter 5.
Type Flaw Attacks, Multi-Protocol Attacks, Tagging Schemes James Heather, Gavin Lowe, Steve Schneider, How to Prevent Type Flaw Attacks on Security Protocols, CSFW 2000.
Bruno Blanchet, Andreas Podelski, Verification of Cryptographic Protocols: Tagging Enforces Termination, FoSSaCS 2003.
Inductive Method Lawrence C. Paulson, The Inductive Approach to Verifying Cryptographic Protocols, Journal of Computer Security, 1998.
Isabelle/HOL Isabelle, 2018.
Giampaolo Bella, Formal Correctness of Security Protocols, Springer, 2007.
Security Protocols Verification in Isabelle/HOL

Labs References
Labs Setup Pre-built SEEDUbuntu12.04 VM
Heartbleed Attack
SPAN+AVISPA Installation Span_Avispa.ova
AVISPA AVISPA - Automated Validation of Internet Security Protocols and Applications
The Avispa Team, HLPSL Tutorial, 2006.
The Avispa Team, AVISPA v1.1 User Manual, 2006.
AVISPA: Constraint-Logic-based Attack Searcher Model-Checker
AVISPA Project
Scyther Installation Scyther v1.1.3, 2014.
Scyther Cătălin Bîrjoveanu: Operational Semantics, Security Properties, Verification of Security Protocols using Hybrid Techniques. Lecture Notes.
Scyther Project Cătălin Bîrjoveanu: Type Flaw Attacks, Multi-Protocol Attacks, Tagging Schemes. Lecture Notes.
Techniques for Security Protocols Verification