Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
Rights / licenseIn Copyright - Non-Commercial Use Permitted
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. Show more
PublisherSwiss Federal Institute of Technology (ETH) Zurich, Institute of Information Security
SubjectDATA SECURITY + DATA PROTECTION (OPERATING SYSTEMS); NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); Theorem proving; Automatic tools; Security protocols; Formal methods; DATENSICHERHEIT + DATENSCHUTZ (BETRIEBSSYSTEME)
Organisational unit02150 - Dep. Informatik / Dep. of Computer Science
NotesTechnical Reports D-INFK.
MoreShow all metadata