Abstract
Security proofs for cryptographic systems can be carried out in different models which reflect different kinds of security assumptions. In the symbolic model, an attacker cannot guess a secret at all and can only apply a pre-defined set of operations, whereas in the computational model, he can hope to guess secrets and apply any polynomial-time operation. Security properties in the computational model are more difficult to establish and to check.
In this paper we present a framework for certified proofs of computational indistinguishability, written using the Coq proof assistant, and based on CIL, a specialized logic for computational frames that can be applied to primitives and protocols. We demonstrate how CIL and its Coq-formalization allow proofs beyond the black-box security framework, where an attacker only uses the input/output relation of the system by executing on chosen inputs without having additional information on the state. More specifically, we use it to prove the security of a protocol against a particular kind of side-channel attack which aims at modeling leakage of information caused by an intrusion into Alice and Bob’s computers.
This work has been partially supported by the ANR SCALP project.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alwen, J., Dodis, Y., Wichs, D.: Survey: Leakage Resilience and the Bounded Retrieval Model. In: Kurosawa, K. (ed.) Information Theoretic Security. LNCS, vol. 5973, pp. 1–18. Springer, Heidelberg (2010)
Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Science of Computer Programming 74(8), 568–589 (2009)
Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational indistinguishability logic. In: Proceedings of the 17th ACM Conference on Computer and Communications Security. ACM, New York (2010)
Barthes, G., Duclos, M., Lakhnech, Y.: A computational indistinguishability logic for the bounded storage model. In: FPS 2011 (2011)
Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: Proceedings of POPL 2009, pp. 90–101 (2009)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, pp. 82–96. IEEE Computer Society (June 2001)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154 (2006)
Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 1–35 (2010)
The Coq Proof Assistant, http://coq.inria.fr/
Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: Proceedings of CSFW 2006, pp. 321–334 (2006)
Dziembowski, S., Maurer, U.: Optimal randomizer efficiency in the bounded-storage model. Journal of Cryptology 17(1), 5–26 (2004)
Dziembowski, S., Pietrzak, K.: Leakage-resilient cryptography. In: IEEE 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, pp. 293–302 (2008)
Dziembowski, S.: Intrusion-Resilience Via the Bounded-Storage Model. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 207–224. Springer, Heidelberg (2006)
Impagliazzo, R., Kapron, B.: Logics for reasoning about cryptographic constructions. Journal of Computer and Systems Sciences 72(2), 286–320 (2006)
Kocher, P.C.: Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996)
Kiltz, E., Pietrzak, K.: Leakage Resilient ElGamal Encryption. In: Abe, M. (ed.) ASIACRYPT 2010. LNCS, vol. 6477, pp. 595–612. Springer, Heidelberg (2010)
Maurer, U.M.: Conditionally-perfect secrecy and a provably-secure randomized cipher. Journal of Cryptology 5(1), 53–66 (1992)
Micali, S., Reyzin, L.: Physically Observable Cryptography. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 278–296. Springer, Heidelberg (2004)
Micali, S., Reyzin, L.: Physically Observable Cryptography (extended abstract). In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 278–296. Springer, Heidelberg (2004)
Rogaway, P., Bellare, M.: Optimal asymmetric encryption how to encrypt with rsa (1995)
Zhang, Y.: The computational SLR: a logic for reasoning about computational indistinguishability. IACR ePrint Archive 2008/434, 2008. Also in Proc. of Typed Lambda Calculi and Applications (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corbineau, P., Duclos, M., Lakhnech, Y. (2011). Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. In: Jouannaud, JP., Shao, Z. (eds) Certified Programs and Proofs. CPP 2011. Lecture Notes in Computer Science, vol 7086. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25379-9_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-25379-9_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25378-2
Online ISBN: 978-3-642-25379-9
eBook Packages: Computer ScienceComputer Science (R0)