Description:
<jats:p>Research on the automatic analysis of cryptographic protocols has so far concentrated on reachability properties, such as secrecy and authentication. In this article, 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.</jats:p>