Abstract
This paper introduces Expi2Java, a new code generator for cryptographic protocols that translates models written in an extensible variant of the Spi calculus into executable code in a substantial fragment of Java, featuring concurrency, synchronization between threads, exception handling and a sophisticated type system with generics and wildcards. Our code generator is highly extensible and customizable, which allows it to generate interoperable implementations of complex real life protocols from detailed verified specifications. As a case study, we have generated an interoperable implementation of TLS v1.0 client and server from a protocol model verified with ProVerif. Furthermore, we have formalized the translation algorithm of Expi2Java using the Coq proof assistant, and proved that the generated programs are well-typed if the original models are well-typed. This constitutes an important step towards the first machine-checked correctness proof of a code generator for cryptographic protocols.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
CVE-2009-3555. Man-in-the-Middle Vulnerability in TLS via Session Renegotiation (2009)
The Coq proof assistant, Version 8.3, Home page (2010), http://coq.inria.fr/
Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. Information and Computation 148(1), 1–70 (1999)
Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL 2008, pp. 3–15 (2008)
Backes, M., Hriţcu, C., Maffei, M.: Type-checking zero-knowledge. In: CCS 2008, pp. 357–370. ACM Press (October 2008)
Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. ACM Transactions on Programming Languages and Systems 31(1) (2008)
Blake-Wilson, S., Nystrom, M., Hopwood, D., Mikkelsen, J., Wright, T.: Transport Layer Security (TLS) Extensions RFC 4366 (April 2006)
Blanchet, B.: ProVerif v1.14pl4 (Automatic Cryptographic Protocol Verifier) User Manual (February 2008), http://www.proverif.ens.fr/
Chown, P.: Advanced Encryption Standard (AES) Ciphersuites for Transport Layer Security (TLS) RFC 3268 (Informational) (June 2002)
Curien, P.-L., Ghelli, G.: Coherence of subsumption, minimum typing and type-checking in F ≤ . Mathematical Structures in Computer Science 2(1), 55–91 (1992)
Dierks, T., Allen, C.: The TLS Protocol Version 1.0 RFC 2246 (January 1999)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM TOPLAS 23(3), 396–450 (2001)
Igarashi, A., Viroli, M.: Variant parametric types: A flexible subtyping scheme for generics. ACM TOPLAS 28, 795–847 (2006)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS 28(4), 619–695 (2006)
Lochbihler, A.: Type safe nondeterminism - a formal semantics of Java threads. In: FOOL (2008)
Lochbihler, A.: Verifying a Compiler for Java Threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427–447. Springer, Heidelberg (2010)
Lukell, S., Veldman, C., Hutchison, A.: Automated attack analysis and code generation in a multi-dimensional security protocol engineering framework. In: Southern African Telecommunications Networks and Applications Conference (2003)
McCarthy, J.A., Krishnamurthi, S., Guttman, J.D., Ramsdell, J.D.: Compiling cryptographic protocols for deployment on the web. In: WWW 2007, pp. 687–696 (2007)
Millen, J., Muller, F.: Cryptographic protocol generation from CAPSL. Technical Report SRI-CSL-01-07, SRI International (December 2001)
Song, D., Perrig, A., Phan, D.: AGVI - Automatic Generation, Verification, and Implementation of Security Protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 241–245. Springer, Heidelberg (2001)
Pironti, A., Sisto, R.: An experiment in interoperable cryptographic protocol implementation using automatic code generation. In: ISCC (2007)
Pozza, D., Sisto, R., Durante, L.: Spi2Java: Automatic cryptographic protocol Java code generation from spi calculus. In: AINA, pp. 400–405. IEEE Computer Society Press (2004)
Song, D.X., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9(1/2), 47–74 (2001)
Tobler, B., Hutchison, A.: Generating network security protocol implementations from formal specifications. In: CSES (2004)
Torgersen, M., Hansen, C.P., Ernst, E., von der Ahé, P., Bracha, G., Gafter, N.M.: Adding wildcards to the Java programming language. In: SAC 2004, pp. 1289–1296 (2004)
Wischik, L.: Old names for nu. Presented at Dagstuhl Seminar 04241 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Busenius, A., Hriţcu, C. (2012). On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)