Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties

Abstract : There exist several automatic verification tools of cryptographic protocols, but only few of them are able to check protocols in presence of algebraic properties. Most of these tools are dealing either with Exclusive-Or (XOR) and exponentiation properties, so-called Diffie-Hellman (DH). In the last few years, the number of these tools increased and some existing tools have been updated. Our aim is to compare their performances by analysing a selection of cryptographic protocols using XOR and DH. We compare execution time and memory consumption for different versions of the following tools OFMC, CL-Atse, Scyther, Tamarin, TA4SP, and extensions of ProVerif (XOR-ProVerif and DH-ProVerif). Our evaluation shows that in most of the cases the new versions of the tools are faster but consume more memory. We also show how the new tools: Tamarin, Scyther and TA4SP, can be compared to previous ones. We also discover and understand for the protocol IKEv2-DS a difference of modelling by the authors of different tools, which leads to different security results. Finally, for Exclusive-Or and Diffie-Hellman properties, we construct two families of protocols P xori and P dhi that allow us to clearly see for the first time the impact of the number of operators and variables in the tools' performances.
Type de document :
Communication dans un congrès
8th International Symposium on Foundations and Practice of Security 8th International Symposium, FPS 2015, Oct 2015, Clermont-Ferrand, France. Springer, 8th International Symposium, FPS 2015 pp.137-155, 2016, Foundations nd Practice of Security 8th International Symposium, FPS 2015, Clermont-Ferrand, France, October 26-28, 2015, Revised Selected Papers. 〈http://confiance-numerique.clermont-universite.fr/fps2015/〉. 〈10.1007/978-3-319-30303-1_9〉
Liste complète des métadonnées

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

http://hal.univ-grenoble-alpes.fr/hal-01306395
Contributeur : Maxime Puys <>
Soumis le : lundi 25 avril 2016 - 09:29:23
Dernière modification le : jeudi 11 janvier 2018 - 06:16:31
Document(s) archivé(s) le : mardi 15 novembre 2016 - 10:39:58

Fichier

main-fps.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Pascal Lafourcade, Maxime Puys. Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties. 8th International Symposium on Foundations and Practice of Security 8th International Symposium, FPS 2015, Oct 2015, Clermont-Ferrand, France. Springer, 8th International Symposium, FPS 2015 pp.137-155, 2016, Foundations nd Practice of Security 8th International Symposium, FPS 2015, Clermont-Ferrand, France, October 26-28, 2015, Revised Selected Papers. 〈http://confiance-numerique.clermont-universite.fr/fps2015/〉. 〈10.1007/978-3-319-30303-1_9〉. 〈hal-01306395〉

Partager

Métriques

Consultations de la notice

271

Téléchargements de fichiers

158