*To*: Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Advertise your work on the mailing list*From*: Simon Meier <iridcode at gmail.com>*Date*: Tue, 26 Oct 2010 15:19:42 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Cas Cremers <cas.cremers at gmail.com>, David Basin <basin at inf.ethz.ch>*In-reply-to*: <AD3C3C71-141A-4CBF-897B-6B751CB9C6A9@in.tum.de>*References*: <AD3C3C71-141A-4CBF-897B-6B751CB9C6A9@in.tum.de>

Hi all, Now it's your turn! at CSF 2010, we published the following results stemming from our ongoing effort to provide a simple framework for developing machine-checked protocol security proofs. *Meier, Cremers, Basin, "Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs", in CSF, 2010, pp. 231-245.* *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. A pre-release of the our Isabelle theories and the proof generation tool implemented in Haskell can be found on Simon's homepage. http://people.inf.ethz.ch/meiersi/espl/index.html Many of you know Paulson's inductive approach to security protocol verification [1]. Hence, we provide a short *comparison between the Inductive Approach and our approach.* In the Inductive Approach both the formalization of the intruder capabilities as well as the protocol specification are shallowly embedded in the definition of the inductive set of traces describing the protocol execution. The advantage of such a shallow embedding is that the expressivity for the protocol specification is limited by HOL only. However, the price one pays is that one has to come up with and prove more inductive invariants. In our approach, we use a deep embedding of a protocol specification language that represents protocols as a set of roles where a role is a linear sequence of send and receive steps. We formalize a protocol independent semantics as an inductive set of traces parametrized over the protocol being executed. This construction allows us to provide a set of protocol independent invariants strong enough for proving secrecy and authentication properties for "classical authentication protocols" (e.g. Kerberos or TLS or the protocols in the SPORE [2]) without resorting to induction over the traces. Due to our protocol independent invariants, security proof construction becomes (quite) mechanical. For secrecy and non-injective authentication properties, proof search is even that simple that we can automatically find their proofs and output them as Isabelle proof scripts. Based on these automatically proven properties, more complex properties can then be proven interactively. Note that our invariants were inspired by the theory underlying the security protocol model checker Scyther [3]. Hence, our capability for automatic proof generation comes to no surprise. The suprising fact is that a theory developed for automatic verification is also that well-suited for interactive use. *The executive summary is the following:* If the protocol you are verifying can be specified as a set of linear roles and your security property can be expressed as a predicate on traces, then our approach might provide an elegant way to construct your security proofs. If not, then Paulson's approach might suit your problem better. Nevertheless, we would still like to hear about your problem, as it may be that one of the extensions we are working on applies. best regards, Simon, Cas, David [1] Paulson, "The Inductive Approach to Verifying Cryptographic Protocols", Journal of Computer Security, vol. 6, pp. 85-128, 1998. [2] http://www.lsv.ens-cachan.fr/Software/spore/index.html [3] http://people.inf.ethz.ch/cremersc/scyther/index.html

**References**:**[isabelle] Advertise your work on the mailing list***From:*Jasmin Christian Blanchette

- Previous by Date: Re: [isabelle] Isabelle 2009-2, ProofGeneral, xemacs under CygWin with XWin
- Next by Date: Re: [isabelle] Writing a specific rule_tac application on ML level
- Previous by Thread: Re: [isabelle] Advertise your work on the mailing list
- Next by Thread: Re: [isabelle] Advertise your work on the mailing list
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list