@article{MeCrBa2013efficient,
  author    = {Simon Meier and
               Cas Cremers and
               David A. Basin},
  title     = {Efficient Construction of Machine-Checked
               Symbolic Protocol Security Proofs},
  journal   = {Journal of Computer Security},
  volume    = {21},
  number    = {1},
  year      = {2013},
  pages     = {41--87},
  ee        = {http://dx.doi.org/10.3233/JCS-2012-0455},
  doi       = {10.3233/JCS-2012-0455},
  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.},
}