Cryptographic Verification by Typing for a Sample Protocol Implementation

Abstract : Type systems are effective tools for verifying the security of cryptographic protocols and implementations. They provide automation, modularity and scalability, and have been applied to large protocols. In this tutorial, we illustrate the use of types for verifying authenticity properties, first using a symbolic model of cryptography, then relying on a concrete computational assumption. (1) We introduce refinement types (that is, types carrying formulas to record invariants) for programs written in F# and verified by F7, an SMT-based type checker. (2) We describe a sample authenticated RPC protocol, we implement it in F#, and we specify its security against active adversaries. (3) We develop a sample symbolic library, we present its main cryptographic invariants, and we show that our RPC implementation is perfectly secure when linked to this symbolic library. (4) We implement the same library using concrete cryptographic primitives, we make a standard computational assumption, and we show that our RPC implementation is also secure with overwhelming probability when linked to this concrete library.
Type de document :
Chapitre d'ouvrage
Alessandro Aldini; Roberto Gorrieri Cryptographic Verification by Typing for a Sample Protocol Implementation, 6858, Springer, 2011, LNCS - Lecture Notes in Computer Science, 978-3-642-23081-3. 〈10.1007/978-3-642-23082-0_3〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01295013
Contributeur : Bhargavan Karthikeyan <>
Soumis le : lundi 4 avril 2016 - 14:24:55
Dernière modification le : jeudi 26 octobre 2017 - 16:34:02
Document(s) archivé(s) le : mardi 5 juillet 2016 - 13:50:10

Fichier

cryptographic_verification_fos...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Cédric Fournet, Karthikeyan Bhargavan, Andrew Gordon. Cryptographic Verification by Typing for a Sample Protocol Implementation. Alessandro Aldini; Roberto Gorrieri Cryptographic Verification by Typing for a Sample Protocol Implementation, 6858, Springer, 2011, LNCS - Lecture Notes in Computer Science, 978-3-642-23081-3. 〈10.1007/978-3-642-23082-0_3〉. 〈hal-01295013〉

Partager

Métriques

Consultations de la notice

71

Téléchargements de fichiers

33