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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aizatulin, M., Gordon, A.D., Jürjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: CCS 2011, pp. 331–340. ACM, New York (2011)
Aizatulin, M., Gordon, A.D., Jürjens, J.: Computational verification of C protocol implementations by symbolic execution. In: CCS 2012, pp. 712–723. ACM, New York (2012)
Bhargavan, K., Fournet, C., Gordon, A., Tse, S.: Verified interoperable implementations of security protocols. ACM TOPLAS 31(1) (2008)
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing 5(4), 193–207 (2008)
Blanchet, B.: Automatically verified mechanized proof of one-encryption key exchange. In: CSF 2012, pp. 325–339. IEEE, Los Alamitos (2012)
Cadé, D., Blanchet, B.: Proved generation of implementations from computationally secure protocol specifications, http://prosecco.gforge.inria.fr/personal/dcade/post2013full.pdf
Cadé, D., Blanchet, B.: From computationally-proved protocol specifications to implementations. In: ARES 2012, pp. 65–74. IEEE, Los Alamitos (2012)
Chaki, S., Datta, A.: ASPIER: An automated framework for verifying security protocol implementations. In: CSF 2009, pp. 172–185. IEEE, Los Alamitos (2009)
Dupressoir, F., Gordon, A.D., Jürjens, J., Naumann, D.A.: Guiding a general-purpose C verifier to prove cryptographic protocols. In: CSF 2011, pp. 3–17. IEEE, Los Alamitos (2011)
Fournet, C., Kohlweiss, M., Strub, P.Y.: Modular code-based cryptographic verification. In: CCS 2011, pp. 341–350. ACM, New York (2011)
Milicia, G.: χ-spaces: Programming security protocols. In: NWPT 2002 (2002)
Owens, S.: A Sound Semantics for OCaml light . In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 1–15. Springer, Heidelberg (2008)
Pironti, A., Sisto, R.: Provably correct Java implementations of spi calculus security protocols specifications. Computers and Security 29(3), 302–314 (2010)
Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bharagavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ICFP 2011, pp. 266–278. ACM, New York (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cadé, D., Blanchet, B. (2013). Proved Generation of Implementations from Computationally Secure Protocol Specifications. In: Basin, D., Mitchell, J.C. (eds) Principles of Security and Trust. POST 2013. Lecture Notes in Computer Science, vol 7796. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36830-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-36830-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36829-5
Online ISBN: 978-3-642-36830-1
eBook Packages: Computer ScienceComputer Science (R0)