Abstract
We present an approach to automating computationally sound proofs of key exchange protocols based on public-key encryption. We show that satisfying the property called occultness in the Dolev–Yao model guarantees the security of a related key exchange protocol in a simple computational model. Security in this simpler model has been shown to imply security in a Bellare–Rogaway-like model. Furthermore, the occultness in the Dolev–Yao model can be searched automatically by a mechanisable procedure. Thus automated proofs for key exchange protocols in the computational model can be achieved. We illustrate the method using the well-known Lowe–Needham–Schroeder protocol.
Research partially funded by the Australian Research Council through Discovery Project DP0773348.
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
Bellare, M., Boldyreva, A., Micali, S.: Public-key encryption in a multi-user setting: Security proofs and improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)
Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated key exchange secure against dictionary attacks. LNCS, pp. 139–155. Springer, Heidelberg (2000)
Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)
Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: Proceedings of IEEE Symposium on Security and Privacy, 86–100 (2004)
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing 5(4), 193–207 (2008)
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)
Canetti, R., Gajek, S.: Universally composable symbolic analysis of Diffie–Hellman based key exchange. Cryptology ePrint Archive, Report 2010/303 (2010), http://eprint.iacr.org/
Canetti, R., Krawczyk, H.: Universally composable notions of key exchange and secure channels. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 337–351. Springer, Heidelberg (2002)
Chevalier, Y., Vigneron, L.: A tool for lazy verification of security protocols. In: Proceedings of ASE, vol. 1, pp. 373–376 (2001)
Choo, K.K., Boyd, C., Hitchcock, Y.: Errors in computational complexity proofs for protocols. In: Roy, B. (ed.) ASIACRYPT 2005. LNCS, vol. 3788, pp. 624–643. Springer, Heidelberg (2005)
Choo, K.K.R., Boyd, C., Hitchcock, Y., Maitland, G.: On session identifiers in provably secure protocols. Security in Communication Networks, 351–366 (2004)
Cortier, V., Millen, J., Rueß, H.: Proving secrecy is easy enough. In: Proceedings of the 14th IEEE workshop on Computer Security Foundations, p. 97. IEEE Computer Society, Los Alamitos (2001)
Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Programming Languages and Systems, pp. 157–171
Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lakhnech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, pp. 371–380. ACM, New York (2008)
Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: 19th IEEE Computer Security Foundations Workshop, p. 14 (2006)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Gagné, M., Lafourcade, P., Lakhnech, Y., Safavi-Naini, R.: Automated security proof for symmetric encryption modes. In: Advances in Computer Science-ASIAN 2009. Information Security and Privacy, pp. 39–53 (2009)
Kudla, C., Paterson, K.: Modular security proofs for key agreement protocols. In: Roy, B. (ed.) ASIACRYPT 2005. LNCS, vol. 3788, pp. 549–565. Springer, Heidelberg (2005)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 147–166 (1996)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. Theory of Cryptography, 133–151 (2004)
Millen, J., Rueß, H.: Protocol-independent secrecy. In: 2000 IEEE Symposium on Security and Privacy, IEEE Computer Society, Los Alamitos (2000)
Okamoto, T., Pointcheval, D.: The gap-problems: A new class of problems for the security of cryptographic schemes. In: Kim, K.-c. (ed.) PKC 2001. LNCS, vol. 1992, pp. 104–118. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ngo, L., Boyd, C., Nieto, J.G. (2010). Automating Computational Proofs for Public-Key-Based Key Exchange. In: Heng, SH., Kurosawa, K. (eds) Provable Security. ProvSec 2010. Lecture Notes in Computer Science, vol 6402. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16280-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16280-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16279-4
Online ISBN: 978-3-642-16280-0
eBook Packages: Computer ScienceComputer Science (R0)