Verifying Security Protocols Using Isabelle

• 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)
• 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 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 J. Information Security 4 (2005), 17–28.

(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.

• 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.