Verifying Security Protocols Using Isabelle

Introductory papers

L C Paulson.
The inductive approach to verifying cryptographic protocols. J. Computer Security 6 (1998), 85–128.
Giampaolo Bella
Inductive Verification of Cryptographic Protocols
PhD Thesis, University of Cambridge (2000)
L C Paulson.
Security protocols and their correctness.
Automated Reasoning Workshop 1998. St. Andrews, Scotland (1998)
Slides available
L C Paulson.
Proving security protocols correct.
IEEE Symposium on Logic in Computer Science. Trento, Italy (1999).
Slides available
L C Paulson.
Seven Years of Verifying Security Protocols
Schloß Dagstuhl Seminar 03451: Applied Deductive Verification (2003)
Slides available

(See the automatically-generated theory document.)

Giampaolo Bella, Fabio Massacci, L. C. Paulson and Piero Tramontano.
Formal verification of Cardholder Registration in SET. In: F. Cuppens et al. (editors), Computer Security — ESORICS 2000 (Springer LNCS 1895, 2000), 159–174.
L. C. Paulson.
Verifying the SET protocol. IJCAR 2001: International Joint Conference on Automated Reasoning, Siena, Italy.
Slides available
L. C. Paulson.
Verification of SET: the purchase phase.
Schloß Dagstuhl Seminar 01391: Specification and Analysis of Secure Cryptographic Protocols (2001)
Slides available
Giampaolo Bella, Fabio Massacci and L. C. Paulson.
The verification of an industrial payment protocol: the
SET purchase phase. In: Vijay Atluri (editor), 9th ACM Conference on Computer and Communications Security (ACM Press, 2002), pages 12–20.
L. C. Paulson.
Verifying the SET protocol: overview
Invited lecture, FASec 2002: Formal Aspects of Security. Royal Holloway College, University of London, England, December 2002.
Slides available
Giampaolo Bella, Fabio Massacci and L. C. Paulson.
Verifying the SET registration protocols. IEEE Journal on Selected Areas in Communications 21 1 (2003), 77–87.
Giampaolo Bella, Fabio Massacci and L. C. Paulson.
An overview of the verification of SET. International Journal of Information Security, in press.

Giampaolo Bella and L. C. Paulson.
Using Isabelle to prove properties of the Kerberos authentication system. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
Giampaolo Bella and L. C. Paulson.
Mechanising BAN Kerberos by the inductive method. In: Alan J. Hu and Moshe Y. Vardi (editors), Computer-Aided Verification: CAV '98 (Springer LNCS 1427, 1998), 416–427.
Giampaolo Bella and L. C. Paulson.
Kerberos version IV: inductive analysis of the secrecy goals. In: Jean-Jacques Quisquater et al. (editors), Computer Security — ESORICS 98 (Springer LNCS 1485, 1998), 361–375.
L. C. Paulson.
Inductive analysis of the Internet protocol TLS. ACM Transactions on Computer and System Security 2 3 (1999), 332–351.
Slides available
L. C. Paulson.
Relations between secrets: two formal analyses of the Yahalom protocol. J. Computer Security 9 3 (2001), 197–216.
Giampaolo Bella and L. C. Paulson.
Mechanical proofs about a non-repudiation protocol. In: Richard J. Boulton and Paul B. Jackson (editors),Theorem Proving in Higher Order Logics (Springer LNCS 2152, 2001), 91–104.
Giampaolo Bella, Cristiano Longo and L. C. Paulson.
Verifying second-level security protocols. In: David Basin and Burkhart Wolff (editors),Theorem Proving in Higher Order Logics (Springer LNCS 2758, 2003), pages 352–366.
Slides available
Giampaolo Bella.
Inductive Verification of Smart Card Protocols.. J. Computer Security 11 1 (2003), 87–132.

The proof scripts, other than those for SET, are distributed with Isabelle. Go to subdirectory HOL/Auth.

Research funded by the EPSRC, projects GR/K77051 and GR/R 01156/01.

Last revised: Tuesday, July 20, 2004