Skip to Main content Skip to Navigation
Conference papers

A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange

Abstract : In this paper, we provide the first methodology for reasoning about liveness properties of cryptographic protocols in a machine-assisted manner without imposing any artificial, finite bounds on the protocols and execution models. To this end, we design an extension of the SAPiC process calculus so that it supports key concepts for stating and reasoning about liveness properties, along with a corresponding translation into the formalism of multiset rewriting that the state-of-the-art theorem prover Tamarin relies upon. We prove that this translation is sound and complete and can thereby automatically generate sound Tamarin specifications and automate the protocol analysis. Second, we applied our methodology to two widely investigated fair exchange protocols -- ASW and GJM -- and to the Secure Conversation Protocol standard for industrial control systems, deployed by major players such as Siemens, SAP and ABB. For the fair exchange protocols, we not only re-discovered known attacks, but also uncovered novel attacks that previous analyses based on finite models and restricted number of sessions did not detect. We suggest fixed versions of these protocols for which we prove both fairness and timeliness, yielding the first automated proofs for fair exchange protocols that rely on a general model without restricting the number of sessions and message size. For the Secure Conversation Protocol, we prove several strong security properties that are vital for the safety of industrial systems, in particular that all messages (e.g., commands) are eventually delivered in order.
Document type :
Conference papers
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Steve Kremer Connect in order to contact the contributor
Submitted on : Monday, January 23, 2017 - 3:05:00 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:47 AM
Long-term archiving on: : Monday, April 24, 2017 - 2:34:25 PM


Files produced by the author(s)




Michael Backes, Jannik Dreier, Steve Kremer, Robert Künnemann. A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange. 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), Apr 2017, Paris, France. ⟨10.1109/EuroSP.2017.12⟩. ⟨hal-01396282⟩



Record views


Files downloads