Bounding messages for free in security protocols – extension to various security properties

Myrto Arapinis 1 Marie Duflot 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : While the verification of security protocols has been proved to be undecidable in general, several approaches use simplifying hypotheses in order to obtain decidability for interesting subclasses. Amongst the most common is type abstraction, i.e. considering only well-typed runs of the protocol, therefore bounding message length. In this paper, we show how to get message boundedness “for free” under a reasonable (syntactic) assumption on protocols, in order to verify a variety of interesting security properties including secrecy and several authentication properties. This enables us to improve existing decidability results by restricting the search space for attacks.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2014, pp.34. 〈10.1016/j.ic.2014.09.003〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01083657
Contributeur : Marie Duflot <>
Soumis le : mercredi 28 octobre 2015 - 15:51:36
Dernière modification le : jeudi 22 septembre 2016 - 14:32:05
Document(s) archivé(s) le : vendredi 28 avril 2017 - 06:15:57

Fichier

versionjournal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Myrto Arapinis, Marie Duflot. Bounding messages for free in security protocols – extension to various security properties. Information and Computation, Elsevier, 2014, pp.34. 〈10.1016/j.ic.2014.09.003〉. 〈hal-01083657〉

Partager

Métriques

Consultations de la notice

202

Téléchargements de fichiers

43