CIL security proof for a password-based key exchange

Authors

Cristian Ene, Universite GrenobleFollow
Clementine Gritti, University of WollongongFollow
Yassine Lakhnech, Universite GrenobleFollow

RIS ID

86100

Publication Details

Ene, C., Gritti, C. & Lakhnech, Y. (2013). CIL security proof for a password-based key exchange. Lecture Notes in Computer Science, 8209 59-85.

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.