Formal Analysis of Combinations of Secure Protocols

Elliott Blot 1 Jannik Dreier 2 Pascal Lafourcade 1
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : When trying to prove the security of a protocol, one usually analyzes the protocol in isolation, i.e., in a network with no other protocols. But in reality, there will be many protocols operating on the same network, maybe even sharing data including keys, and an intruder may use messages of one protocol to break another. We call that a multi-protocol attack. In this paper, we try to find such attacks using the Tamarin prover. We analyze both examples that were previously analyzed by hand or using other tools, and find novel attacks.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-01558552
Contributeur : Jannik Dreier <>
Soumis le : samedi 11 novembre 2017 - 21:27:33
Dernière modification le : mardi 14 novembre 2017 - 01:11:12

Fichier

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

Identifiants

  • HAL Id : hal-01558552, version 5

Collections

Citation

Elliott Blot, Jannik Dreier, Pascal Lafourcade. Formal Analysis of Combinations of Secure Protocols . 2017. 〈hal-01558552v5〉

Partager

Métriques

Consultations de la notice

28

Téléchargements de fichiers

6