User Tools

Site Tools

Constraint Solving for Contract-Signing Protocols (BibTeX)

  author      = {Detelf K{\"a}hler and Ralf K{\"u}sters},
  title       = {{Constraint Solving for Contract-Signing Protocols}},
  booktitle   = {Proceedings of the 16th International Conference on Concurrency Theory (CONCUR 2005)},
  editor      = {M.~Abadi and L.~de Alfaro},
  year        = 2005,
  pages       = {233--247},
  publisher   = {Springer},
  series      = {Lecture Notes in Computer Science},
  volume      = 3653,
  abstract    = {Research on the automatic analysis of cryptographic protocols has so far mainly concentrated on reachability properties, such as secrecy and authentication.  Only recently it was shown that certain game-theoretic security properties, such as balance for contract-signing protocols, are decidable in a Dolev-Yao style model with a bounded number of sessions but unbounded message size.  However, this result does not provide a practical algorithm as it merely bounds the size of attacks.  In this paper, we prove that game-theoretic security properties can be decided based on standard constraint solving procedures. In the past, these procedures have successfully been employed in implementations and tools for reachability properties. Our results thus pave the way for extending these tools and implementations to deal with game-theoretic security properties.}