A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange
Michael Backes, Jannik Dreier, Steve Kremer, and Robert Künnemann. A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange. In Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pp. 76–91, IEEE Computer Society, Paris, France, April 2017.
Download
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.
BibTeX
@inproceedings{BDKK-eurosp17,
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. \par 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.},
address = {Paris, France},
author = {Backes, Michael and Dreier, Jannik and Kremer, Steve
and K{\"u}nnemann, Robert},
booktitle = {{P}roceedings of the 2nd IEEE European Symposium on
Security and Privacy (EuroS\&P'17)},
pages = {76--91},
month = apr,
publisher = {IEEE Computer Society},
title = {A Novel Approach for Reasoning about Liveness in
Cryptographic Protocols and its Application to Fair
Exchange},
year = 2017,
acronym = {{EuroSP}'17},
nmonth = 4,
url = {https://hal.inria.fr/hal-01396282/},
}