User Tools

Site Tools

Deciding Strategy Properties of Contract-Signing Protocols (BibTeX)

  author      = {Detlef K{\"a}hler and Ralf K{\"u}sters and Thomas Wilke},
  title       = {{Deciding Strategy Properties of Contract-Signing Protocols}},
  journal     = {ACM Transactions on Computational Logic (TOCL)},
  year        = 2010,
  volume      = 11,
  number      = 3,
  abstract    = {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.}