Formal verification of protocols based on short authenticated strings (extended version)

Stéphanie Delaune 1 Steve Kremer 2 Ludovic Robin 2
1 EMSEC - EMbedded SEcurity and Cryptography
IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Modern security protocols may involve humans in order to compare or copy short strings between different devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-secure are typical examples of such protocols. However, such short strings may be subject to brute force attacks. In this paper we propose a symbolic model which includes attacker capabilities for both guessing short strings, and producing collisions when short strings result from an application of weak hash functions. We propose a new decision procedure for analysing (a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in the AKISS tool and tested on protocols from the ISO/IEC 9798-6:2010 standard.
Type de document :
Rapport
[Research Report] Inria Nancy - Grand Est. 2017
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01528603
Contributeur : Steve Kremer <>
Soumis le : lundi 29 mai 2017 - 12:59:11
Dernière modification le : mardi 16 janvier 2018 - 15:54:26
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 10:51:23

Fichier

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

Identifiants

  • HAL Id : hal-01528603, version 1

Citation

Stéphanie Delaune, Steve Kremer, Ludovic Robin. Formal verification of protocols based on short authenticated strings (extended version). [Research Report] Inria Nancy - Grand Est. 2017. 〈hal-01528603〉

Partager

Métriques

Consultations de la notice

234

Téléchargements de fichiers

50