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

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.
doi:10.1109/EuroSP.2017.12

Download

[PDF] [HTML]

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},
  doi =		 {10.1109/EuroSP.2017.12},
  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/},
}