Compositional analysis of contract-signing protocols

We develop a general method for proving properties of contract-signing protocols using a specialized protocol logic. The method is applied to the Asokan–Shoup–Waidner and the Garay–Jacobson–MacKenzie protocols. Our method offers certain advantages over previous analysis techniques. First, it is compositional: the security guarantees are proved by combining the independent proofs for the three subprotocols of each protocol. Second, the formal proofs are carried out in a “template” form, which gives us a reusable proof that may be instantiated for the two example protocols, as well as for other protocols with the same arrangement of messages. Third, the proofs follow the design intuition. In particular, in proving game-theoretic properties like fairness, we demonstrate success for the specific strategy that the protocol designer had in mind, instead of non-constructively proving that a strategy exists. Finally, our logical proofs demonstrate security when an unbounded number of sessions are executed in parallel.