Sage Journals: Discover world-class research

Abstract

In order to obtain implementations of security protocols proved secure in the computational model, we previously proposed the following approach: we write a specification of the protocol in the input language of the computational protocol verifier CryptoVerif, prove it secure using CryptoVerif, then generate an OCaml implementation of the protocol from the CryptoVerif specification using a specific compiler that we have implemented. 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.

Keywords

Cryptographic protocol computational model implementation compiler CryptoVerif OCaml verification

Get full access to this article

View all access options for this article.

References

[1]http://research.microsoft.com/en-us/projects/cvk/.

[2]

Aizatulin,

A.D.

Gordon and

Jürjens, Extracting and verifying cryptographic models from C protocol code by symbolic execution, in: CCS’11, ACM, New York, 2011, pp. 331–340.

[3]

Aizatulin,

A.D.

Gordon and

Jürjens, Computational verification of C protocol implementations by symbolic execution, in: CCS’12, ACM, New York, 2012, pp. 712–723.

[4]

J.B.

Almeida,

Barbosa,

Barthe and

Dupressoir, Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations, in: ACM SIGSAC Conference on Computer and Communications Security (CCS’13), Berlin, Germany, November 2013, ACM, 2013, pp. 1217–1230.

[5]

Bengtson,

Bhargavan,

Fournet,

Gordon and

Maffeis, Refinement types for secure implementations, ACM TOPLAS 33(2) (2011), Article No. 8.

[6]

Bhargavan,

Fournet,

Gordon and

Tse, Verified interoperable implementations of security protocols, ACM TOPLAS 31(1) (2008), Article No. 5.

[7]

Blanchet, A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing 5(4) (2008), 193–207.

[8]

Blanchet, Automatically verified mechanized proof of one-encryption key exchange, in: CSF’12, IEEE, Los Alamitos, 2012, pp. 325–339.

[9]

Blanchet and

Pointcheval, Automated security proofs with sequences of games, in: CRYPTO’06, LNCS, Vol. 4117, Springer, 2006, pp. 537–554.

10.

[10]

Cadé and

Blanchet, From computationally-proved protocol specifications to implementations and application to SSH, Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA) 4(1) (2013), 4–31.

11.

[11]

Cadé and

Blanchet, Proved generation of implementations from computationally-secure protocol specifications, in: 2nd Conference on Principles of Security and Trust (POST 2013), Rome, Italy, March 2013,

Basin and

Mitchell, eds, LNCS, Vol. 7796, Springer, 2013, pp. 63–82.

12.

[12]

Chaki and

Datta, ASPIER: An automated framework for verifying security protocol implementations, in: CSF’09, IEEE, Los Alamitos, 2009, pp. 172–185.

13.

[13]

Corin and

F.A.

Manzano, Efficient symbolic execution for analysing cryptographic protocol implementations, in: Engineering Secure Software and Systems (ESSoS’11), Madrid, Spain, February 2011,

Ú.

Erlingsson,

Wieringa and

Zannone, eds, LNCS, Vol. 6542, Springer, 2011, pp. 58–72.

14.

[14]

Dupressoir,

A.D.

Gordon,

Jürjens and

D.A.

Naumann, Guiding a general-purpose C verifier to prove cryptographic protocols, in: CSF’11, IEEE, Los Alamitos, 2011, pp. 3–17.

15.

[15]

Fournet,

Kohlweiss and

P.-Y.

Strub, Modular code-based cryptographic verification, in: CCS’11, ACM, New York, 2011, pp. 341–350.

16.

[16]

Milicia, χ-spaces: Programming security protocols, in: NWPT’02, 2002.

17.

[17]

Owens, A sound semantics for OCaml light, in: ESOP’08,

Drossopoulou, ed., LNCS, Vol. 4960, Springer, Heidelberg, 2008, pp. 1–15.

18.

[18]

Owens,

Peskine and

Sewell, A formal specification for OCaml: The core language, 2008, available at: http://www.cl.cam.ac.uk/~so294/ocaml/caml_typedef.pdf.

19.

[19]

Pironti and

Sisto, Provably correct Java implementations of Spi Calculus security protocols specifications, Computers and Security 29(3) (2010), 302–314.

20.

[20]

Swamy,

Chen,

Fournet,

P.-Y.

Strub,

Bharagavan and

Yang, Secure distributed programming with value-dependent types, in: ICFP’11, ACM, New York, 2011, pp. 266–278.

Proved generation of implementations from computationally secure protocol specifications 1

Abstract

Keywords

Get full access to this article

References