Automated Analysis of Security Protocols with Global State

Steve Kremer 1 Robert Künnemann 2, 3
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (MSR) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process.We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to MSR rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol.
Type de document :
Communication dans un congrès
IEEE Computer Society. 35th IEEE Symposium on Security and Privacy (S&P'14), May 2014, San Jose, United States. pp.163-178, Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P'14). 〈10.1109/SP.2014.18〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01091241
Contributeur : Steve Kremer <>
Soumis le : jeudi 8 octobre 2015 - 20:37:00
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26
Document(s) archivé(s) le : samedi 9 janvier 2016 - 10:41:54

Fichier

KK-sp14.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Steve Kremer, Robert Künnemann. Automated Analysis of Security Protocols with Global State. IEEE Computer Society. 35th IEEE Symposium on Security and Privacy (S&P'14), May 2014, San Jose, United States. pp.163-178, Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P'14). 〈10.1109/SP.2014.18〉. 〈hal-01091241〉

Partager

Métriques

Consultations de la notice

256

Téléchargements de fichiers

45