Implementing a Constraint Solving Algorithm for Checking Game-Theoretic Security Requirements
One of the central results in the area of automatic analysis of cryptographic protocols is that the security of cryptographic protocols is decidable when analyzed w.r.t. a finite number of sessions, without a bound on the message size, and in presence of the so-called Dolev-Yao intruder. Contract-signing and related protocols have to satisfy game-theoretic security properties. Based on an algorithm proposed by the researchers for checking such security properties, in this paper, the authors report on the implementation of this algorithm and its performance.