Developing Security Protocols by Refinement

Main content

Below you find the Isabelle/HOL sources for our correct-by-construction security protocol development framework based on refinement.

Overview of the Isabelle/HOL theories

The theories of this development can be divided into three groups:

  1. Infrastructure for refinement of security protocols, including
    • a general theory of refinement infrastructure for modeling protocols (e.g., runs, channels, and cryptographic messages)
    • abstract models of secrecy and authentication 
  2. Development of a family of authentication protocols
    • authentication based on public-key encryption
    • authentication based on digital signatures
  3. Development of a family of key establishment protocols
    • core Kerberos IV and V
    • Needham-Schroeder Shared-Key protocol
    • Denning-Sacco protocol

Theory browsing and download

This development was done in Isabelle/HOL 2013. You may

  • Browse Isabelle documentation online [html].
    Note: The link brings you to the first group of theories above. You can find the theories corresponding to the the protocol developments at the bottom of this page.
  • The Isabelle/HOL sources are available on request (please send email to Christoph Sprenger). 


A draft of a journal paper by Christoph Sprenger and David Basin entitled Developing Security Protocols by Refinement has been submitted to JCS and is published as Technical Report 787, Department of Computer Science, ETH Zurich, July 2013 [PDF]

This framework is described in the CCS 2010 and CSF 2012 papers by the same authors. You can find links to these publications.

Page URL:
© 2017 Eidgenössische Technische Hochschule Zürich