Abstract
Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. This paper presents an automated procedure for analyzing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC’2000 and REACT.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barthe, G., Cederquist, J., Tarento, S.: A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 385–399. Springer, Heidelberg (2004)
Barthe, G., Grégoire, B., Janvier, R., Zanella Béguelin, S.: A framework for language-based cryptographic proofs. In: ACM SIGPLAN Workshop on Mechanizing Metatheory (2007)
Barthe, G., Tarento, S.: A machine-checked formalization of the random oracle model. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 33–49. Springer, Heidelberg (2006)
Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among notions of security for public-key encryption schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 26–45. Springer, Heidelberg (1998)
Bellare, M., Rogaway, P.: Optimal asymmetric encryption. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 92–111. Springer, Heidelberg (1995)
Bellare, M., Rogaway, P.: Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331 (2004)
Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: CCS 1993, pp. 62–73 (1993)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: S&P 2006, 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)
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)
Damgard, I.: Towards practical public key systems secure against chosen ciphertext attacks. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 445–456. Springer, Heidelberg (1992)
Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: CSFW 2006, pp. 321–334 (2006)
Feige, U., Fiat, A., Shamir, A.: Zero-knowledge proofs of identity. J. Cryptol. 1(2), 77–94 (1988)
Fujisaki, E., Okamoto, T.: How to enhance the security of public-key encryption at minimum cost. In: Imai, H., Zheng, Y. (eds.) PKC 1999. LNCS, vol. 1560, pp. 53–68. Springer, Heidelberg (1999)
Halevi, S.: A plausible approach to computer-aided cryptographic proofs. ePrint archive report 2005 (2005)
Nowak, D.: A framework for game-based security proofs. In: Qing, S., Imai, H., Wang, G. (eds.) ICICS 2007. LNCS, vol. 4861, pp. 319–333. Springer, Heidelberg (2007)
Okamoto, T., Pointcheval, D.: REACT: Rapid enhanced-security asymmetric cryptosystem transform. In: Naccache, D. (ed.) CT-RSA 2001. LNCS, vol. 2020, pp. 159–175. Springer, Heidelberg (2001)
Pointcheval, D.: Chosen-ciphertext security for any one-way cryptosystem. In: Imai, H., Zheng, Y. (eds.) PKC 2000. LNCS, vol. 1751, pp. 129–146. Springer, Heidelberg (2000)
Shoup, V.: Oaep reconsidered. J. Cryptology 15(4), 223–249 (2002)
Shoup, V.: Sequences of games: a tool for taming complexity in security proofs (2004), http://eprint.iacr.org/2004/332
Soldera, D., Seberry, J., Qu, C.: The analysis of zheng-seberry scheme. In: Batten, L.M., Seberry, J. (eds.) ACISP 2002. LNCS, vol. 2384, pp. 159–168. Springer, Heidelberg (2002)
Tarento, S.: Machine-checked security proofs of cryptographic signature schemes. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 140–158. Springer, Heidelberg (2005)
Zheng, Y., Seberry, J.: Immunizing public key cryptosystems against chosen ciphertext attacks. J. on Selected Areas in Communications 11(5), 715–724 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lakhnech, Y. (2010). Automated Proofs for Asymmetric Encryption. In: Dams, D., Hannemann, U., Steffen, M. (eds) Concurrency, Compositionality, and Correctness. Lecture Notes in Computer Science, vol 5930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11512-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-11512-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11511-0
Online ISBN: 978-3-642-11512-7
eBook Packages: Computer ScienceComputer Science (R0)