Efficient construction of machine-checked symbolic protocol security proofs

Article type: Research Article

Authors: Meier, Simon^{; *} | Cremers, Cas | Basin, David

Affiliations: Institute of Information Security, ETH Zurich, Switzerland. E-mails: simon.meier@inf.ethz.ch, cas.cremers@inf.ethz.ch, david.basin@inf.ethz.ch

Correspondence: [*] Corresponding author: Simon Meier, Institute of Information Security, ETH Zurich, CH-8092 Zurich, Switzerland. E-mail: simon.meier@inf.ethz.ch

Abstract: We embed an untyped security protocol model in the interactive theorem prover Isabelle/HOL and derive a theory for constructing proofs of secrecy and authentication properties. Our theory is based on two key ingredients. The first is an inference rule for enumerating the possible origins of messages known to the intruder. The second is a class of protocol-specific invariants that formalize type assertions about variables in protocol specifications. The resulting theory is well suited for interactively constructing human-readable, protocol security proofs. We additionally give an algorithm that automatically generates Isabelle/HOL proof scripts based on this theory. We provide case studies showing that both interactive and automatic proof construction are efficient. The resulting proofs provide strong correctness guarantees since all proofs, including those deriving our theory from the security protocol model, are machine-checked.

Keywords: Security protocols, formal methods, theorem proving, automatic proof generation

DOI: 10.3233/JCS-2012-0455

Journal: Journal of Computer Security, vol. 21, no. 1, pp. 41-87, 2013