Abstract
Computational Indistinguishability Logic (CIL) is a logic for reasoning about cryptographic primitives in computational model. It is sound for standard model, but also supports reasoning in the random oracle and other idealized models. We illustrate the benefits of CIL by formally proving the security of a Password-Based Key Exchange (PBKE) scheme, which is designed to provide entities communicating over a public network and sharing a short password, under a session key.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bellovin, S.M., Merritt, M.: Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionnary Attacks. In: Proc. IEEE Computer Society Symposium on Research in Security and Privacy, pp. 72–84 (1992)
Bellare, M., Rogaway, P.: The AuthA Protocol for Password-Based Authenticated Key Exchange. Unpublished contribution to IEEE P1363 (2000)
Bresson, E., Chevassut, O., Pointcheval, D.: Security Proofs for an Efficient Password-Based Key Exchange. In: Proceedings of CCS 2003, pp. 241–250. ACM Press (2003)
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)
Shoup, V.: Sequences of games: A Tool for Taming Complexity in Security Proofs (2004) (manuscript)
Halevi, S.: A plausible approach to computer-aid cryptographic proofs (2005) (manuscript)
Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational Indistinguishability Logic. In: Proceedings of CCS 2010, pp. 375–386. ACM Press (2010)
Daubignard, M.: Formal Methods for Concrete Security Proofs. PhD thesis (2012)
Blanchet, B.: Automatically Verified Mechanized Proof of One-Encryption Key Exchange. In: CSF 2012 (2012)
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
Ene, C., Gritti, C., Lakhnech, Y. (2013). CIL Security Proof for a Password-Based Key Exchange. In: Susilo, W., Reyhanitabar, R. (eds) Provable Security. ProvSec 2013. Lecture Notes in Computer Science, vol 8209. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41227-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-41227-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41226-4
Online ISBN: 978-3-642-41227-1
eBook Packages: Computer ScienceComputer Science (R0)