Sciweavers

CSFW
2010
IEEE
14 years 2 months ago
Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
We embed an operational semantics for security protocols in the interactive theorem prover Isabelle/HOL and derive two strong protocol-independent invariants. These invariants allo...
Simon Meier, Cas J. F. Cremers, David A. Basin