Proved Generation of Implementations from Computationally-Secure Protocol Specifications

Abstract : In order to obtain implementations of security protocols proved secure in the computational model, we have previously implemented a compiler that takes a specification of the protocol in the input language of the computational protocol verifier CryptoVerif and translates it into an OCaml implementation. However, until now, this compiler was not proved correct, so we did not have real guarantees on the generated implementation. In this paper, we fill this gap. We prove that this compiler preserves the security properties proved by CryptoVerif: if an adversary has probability p of breaking a security property in the generated code, then there exists an adversary that breaks the property with the same probability p in the CryptoVerif specification. Therefore, if the protocol specification is proved secure in the computational model by CryptoVerif, then the generated implementation is also secure.
Type de document :
Communication dans un congrès
David Basin and John Mitchell. 2nd Conference on Principles of Security and Trust (POST 2013), 2013, Rome, Italy. spv, 7796, pp.63--82, 2013, lncs
Liste complète des métadonnées

https://hal.inria.fr/hal-00863376
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:08
Dernière modification le : mardi 17 avril 2018 - 11:25:43

Identifiants

  • HAL Id : hal-00863376, version 1

Collections

Citation

David Cadé, Bruno Blanchet. Proved Generation of Implementations from Computationally-Secure Protocol Specifications. David Basin and John Mitchell. 2nd Conference on Principles of Security and Trust (POST 2013), 2013, Rome, Italy. spv, 7796, pp.63--82, 2013, lncs. 〈hal-00863376〉

Partager

Métriques

Consultations de la notice

87