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...
| Hoofdauteurs: | , , |
|---|---|
| Formaat: | Journal article |
| Taal: | English |
| Gepubliceerd in: |
IOS Press
2013
|