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.
Type de document :
Communication dans un congrès
2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), Apr 2017, Paris, France. Springer, Proceedings of the 2nd IEEE European Symposium on Security and Privacy
Liste complète des métadonnées


https://hal.inria.fr/hal-01396282
Contributeur : Steve Kremer <>
Soumis le : lundi 23 janvier 2017 - 15:05:00
Dernière modification le : jeudi 15 juin 2017 - 09:09:06
Document(s) archivé(s) le : lundi 24 avril 2017 - 14:34:25

Fichier

fairexchange-long.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01396282, version 1

Collections

Citation

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. Springer, Proceedings of the 2nd IEEE European Symposium on Security and Privacy. <hal-01396282>

Partager

Métriques

Consultations de
la notice

411

Téléchargements du document

139