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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 metadatas
Contributor : Mathieu Turuani <>
Submitted on : Wednesday, October 4, 2006 - 6:10:00 PM
Last modification on : Wednesday, September 16, 2020 - 10:42:56 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