Abstract
Game-based cryptographic proofs are typically expressed using pseudocode, which lacks a formal semantics. This can lead to ambiguous specifications, hidden mistakes, and even wrong proofs. We propose a language for expressing proofs that is expressive enough to specify all constructs occurring in cryptographic games, including probabilistic behaviors, the usage of oracles, and polynomial-time programs. The language is a probabilistic higher-order lambda calculus with recursive types, references, and support for events, and is simple enough that researchers without a strong background in the theory of programming languages can understand it. The language has been implemented in the proof assistant Isabelle/HOL.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography: The computational soundness of formal encryption. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)
Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW), pp. 204–218 (2004)
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proc. 10th ACM Conference on Computer and Communications Security, pp. 220–230 (2003); Full version in IACR Cryptology ePrint Archive 2003/015 (January 2003), http://eprint.iacr.org/
Barthe, G., Gregoire, B., Janvier, R., Zanella Beguelin, S.: Formal certification of code-based cryptographic proofs. IACR ePrint Archive (August. 2007), http://eprint.iacr.org/2007/314
Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security (2004)
Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006), http://eprint.iacr.org/2004/331.ps
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proc. 27th IEEE Symposium on Security & Privacy, pp. 140–154 (2006)
Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006)
Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)
Corin, R., den Hartog, J.: A probabilistic hoare-style logic for game-based cryptographic proofs. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 252–263. Springer, Heidelberg (2006)
Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)
de Bruijn, N.G.: Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation. Indagationes Mathematicæ 34, 381–392 (1972)
Goldreich, O.: Foundations of Cryptography, May 2004. Basic Applications, vol. 2. Cambridge University Press, Cambridge (May 2004), http://www.wisdom.weizmann.ac.il/~oded/frag.html
Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005), http://eprint.iacr.org/
Halmos, P.R.: Measure Theory. Graduate Texts in Mathematics, vol. 18. Springer, Heidelberg (1974)
Kemmerer, R.: Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications 7(4), 448–457 (1989)
Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)
Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 25th IEEE Symposium on Security & Privacy, pp. 71–85 (2004)
Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 232–246. Springer, Heidelberg (2002)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Mason, I., Talcott, C.: Equivalence in Functional Languages with Effects. Journal of Functional Programming 1(3), 287–327 (1991)
Meadows, C.: Using narrowing in the analysis of key management protocols. In: Proc. 10th IEEE Symposium on Security & Privacy, pp. 138–147 (1989)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)
Millen, J.K.: The interrogator: A tool for cryptographic protocol security. In: Proc. 5th IEEE Symposium on Security & Privacy, pp. 134–141 (1984)
Müller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9(2), 191–223 (1999)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Nowak, D.: A framework for game-based security proofs. IACR Cryptology ePrint Archive 2007/199 (2007), http://eprint.iacr.org/
Paulson, L.: The inductive approach to verifying cryptographic protocols. Journal of Cryptology 6(1), 85–128 (1998)
Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)
Schwinghammer, J.: Reasoning about Denotations of Recursive Objects. PhD thesis, Department of Informatics, University of Sussex, Brighton, UK (July 2006)
Shoup, V.: Sequences of games: A tool for taming complexity in security proofs. IACR ePrint Archive (November 2004), http://eprint.iacr.org/2004/332.ps
Thayer Fabrega, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: Proc. 19th IEEE Symposium on Security & Privacy, pp. 160–171 (1998)
The Coq development team. The Coq Proof Assistant Reference Manual (2006), http://coq.inria.fr
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Berg, M., Unruh, D. (2008). A Formal Language for Cryptographic Pseudocode. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)