HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Compositional Analysis of Contract Signing Protocols

Michael Backes 1 Anupam Datta 2 Ante Derek 2 John C. Mitchell 2 Mathieu Turuani 3
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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 subprotocols 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 \emph{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.
Document type :
Conference papers
Complete list of metadata

Contributor : Mathieu Turuani Connect in order to contact the contributor
Submitted on : Wednesday, October 4, 2006 - 6:10:00 PM
Last modification on : Friday, January 21, 2022 - 3:08:33 AM


  • HAL Id : inria-00103647, version 1


Michael Backes, Anupam Datta, Ante Derek, John C. Mitchell, Mathieu Turuani. Compositional Analysis of Contract Signing Protocols. 18th IEEE Computer Security Foundations Workshop - CSFW 2005, Jun 2005, Aix-en-Provence/France, pp.94-110. ⟨inria-00103647⟩



Record views