Verifying Security Protocols Using Isabelle
A cryptographic protocol is a message exchange that uses encryption in order to achieve security goals such as secrecy or authenticity over an open network that might be controlled by a hostile party. In 1996, the problem of verifying the correctness of cryptographic protocols was still open and progress had stalled. The work described below has played a major part in solving this problem; the techniques needed to verify many types of key exchange and authentication protocols are today well understood.
The proof scripts described in the papers below are distributed with Isabelle. The SET protocol scripts are stored separately from the basic protocol library.
- Introductory Material
- Verification of the SET protocol
- Other Protocols
- Historic Papers
- L C Paulson.
The inductive approach to verifying cryptographic protocols. J. Computer Security 6 (1998), 85–128. Publisher's version - Giampaolo Bella
Inductive Verification of Cryptographic Protocols
PhD Thesis, University of Cambridge (2000) - Giampaolo Bella
Formal Correctness of Security Protocols (Springer, 2007) - 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
- 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 (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 J. Information Security 4 (2005), 17–28. - Giampaolo Bella, Fabio Massacci and L. C. Paulson.
Verifying the SET Purchase Protocols. J. Automated Reasoning 36 (2006), 5–37.
(See also the automatically-generated theory document.)
- 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 Information 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. - Giampaolo Bella and L. C. Paulson.
Accountability Protocols: Formalized and Verified. ACM Trans. on Information and System Security 9 2 (2006), 138–161. - Jean E. Martina and L. C. Paulson.
Verifying multicast-based security protocols using the inductive method.
International Journal of Information Security 14 2 (2015), 187–204. Publisher's version at www.springerlink.com
- L C Paulson.
Proving properties of security protocols by induction. 10th Computer Security Foundations Workshop (June 1997), 70–83.
Slides available - L C Paulson.
Mechanized proofs for a recursive authentication protocol. 10th Computer Security Foundations Workshop (June 1997), 84–95.
Slides:available - L C Paulson.
Mechanized proofs of security protocols: Needham-Schroeder with public keys.
Report 413, Computer Lab (1997). - 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.
Research funded by the EPSRC, projects GR/K77051 and GR/R 01156/01. 