Constraint Solving for Contract-Signing Protocols

The design of cryptographic protocols is highly error-prone, which makes formal
analysis of such protocols indispensable. For authentication and key exchange
protocols various methods and tools for fully automatic analysis are available.
The security of such protocols can be stated in terms of reachability
properties on typically infinite graphs.  However, for a broad class of
protocols, including contract signing protocols, the security requirements are
more complex and are stated in terms of game-theoretic notions. Up until
recently, nothing was known about the automatic analysis of such protocols.

In this talk, I will first provide an overview on the automatic analysis of
cryptographic protocols and introduce the basic protocol and intruder models. I
will then present new results on the automatic analysis of cryptographic
protocols with game-theoretic security requirements, including a decision
procedure based on the technique of constraint solving.

This talk is based on joint work with Detlef Kaehler and Thomas Wilke presented
at STACS 2005 and CONCUR 2005.