Paper Info
Title
Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
Abstract
We embed an operational semantics for security protocols in the interactive theorem prover Isabelle/HOL and derive two strong protocol-independent invariants. These invariants allow us to reason about the possible origin of messages and justify a local typing assumption for the otherwise untyped protocol variables. The two rules form the core of a theory that is well-suited for interactively constructing natural, human-readable, correctness proofs. Moreover, we develop an algorithm that automatically generates proof scripts based on these invariants. Both interactive and automatic proof construction are faster than competing approaches. Moreover, we have strong correctness guarantees since all proofs, including those deriving the underlying theory from the semantics, are machine checked.
Year
DOI
Venue
2010
10.1109/CSF.2010.23
CSF
Keywords
Field
DocType
strong invariants,local typing assumption,machine-checked protocol security proofs,possible origin,underlying theory,strong protocol-independent invariants,operational semantics,interactive theorem prover,automatic proof construction,strong correctness guarantee,correctness proof,efficient construction,proof script,embedded systems,encryption,formal method,chromium,construction industry,servers,protocols,theorem prover,semantics,theorem proving,security protocols,security protocol,formal methods
HOL,Operational semantics,Programming language,Cryptographic protocol,Computer science,Correctness,Automated theorem proving,Theoretical computer science,Mathematical proof,Formal methods,Proof assistant
Conference
Citations 
PageRank 
References 
10
0.76
22
Authors
3
Name
Order
Citations
PageRank
Simon Meier12086.89
Cas J. F. Cremers290150.06
David A. Basin34930281.93