| Full text | Click to download. |
| Citation | In Proceedings of 18th IEEE Computer Security Foundations
Workshop, pp. 94-110, June 2005
|
| Authors | Michael Backes
Anupam Datta Ante Derek John C. Mitchell Mathieu Turuani |
We develop a general method for reasoning about contract-signing protocols using a specialized protocol logic. The method is applied to prove properties of 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 sub-protocols of which each protocol is comprised. Second, the formal proofs are carried out in a "template" form, which gives us a reusable proof that may be instantiated for the ASW and GJM 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 that the specific strategy that the protocol designer had in mind works, instead of showing that one exists. Finally, our results hold even when an unbounded number of sessions are executed in parallel.