A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange - Archive ouverte HAL Access content directly
Conference Papers Year :

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

(1, 2) , (3) , (3) , (2)
1
2
3

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.
Fichier principal
Vignette du fichier
fairexchange-long.pdf (620.97 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01396282 , version 1 (23-01-2017)

Identifiers

Cite

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⟩
728 View
689 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More