Efficient construction of machine-checked symbolic protocol security proofs.
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...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Published: |
IOS Press
2013
|