Journal article
Efficient construction of machine-checked symbolic protocol security proofs.
- 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 inte...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Authors
Funding
Hasler Foundation
More from this funder
Bibliographic Details
- Publisher:
- IOS Press Publisher's website
- Journal:
- Journal of Computer Security Journal website
- Volume:
- 21
- Issue:
- 1
- Pages:
- 41-87
- Publication date:
- 2013-03-01
- Acceptance date:
- 2012-07-27
- DOI:
- ISSN:
-
0926-227X
Item Description
- Pubs id:
-
pubs:427697
- UUID:
-
uuid:a87cdd13-aa27-4aa2-90d4-fe2012338dbe
- Local pid:
- pubs:427697
- Source identifiers:
-
427697
- Deposit date:
- 2013-11-16
Terms of use
- Copyright holder:
- Cremers et al
- Copyright date:
- 2013
- Notes:
- © 2013 Cremers et al
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record