Deciding Strategy Properties of Contract-Signing Protocols
Detlef Kähler, Ralf Küsters, and Thomas Wilke
Research on the automatic analysis of cryptographic protocols has so far concentrated on reachability properties, such as secrecy and authentication. In this paper, we prove that certain game-theoretic security properties, including balance for contract-signing protocols, can be decided in a Dolev-Yao style model with a bounded number of sessions. The decision algorithm that we develop is based on standard constraint-solving procedures, which, in the past, have successfully been employed in tools for reachability properties. Our result thus paves the way for extending these tools to deal with game-theoretic security properties.