Verifying Security Protocols Using IsabelleIsabelle/HOL logo

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

(See also the automatically-generated theory document.)

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

Last revised: 29 October, 2013
Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge