Re: [isabelle] Advertise your work on the mailing list

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.

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

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

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.