Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
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.
KeywordsProvable Cryptography Formal Verification Computational Model Security Protocol Intrusion Resilience
Unable to display preview. Download preview PDF.
- [BDKL10]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)Google Scholar
- [BDL11]Barthes, G., Duclos, M., Lakhnech, Y.: A computational indistinguishability logic for the bounded storage model. In: FPS 2011 (2011)Google Scholar
- [BGZ09]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)Google Scholar
- [Bla01]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)Google Scholar
- [Bla06]Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154 (2006)Google Scholar
- [CKW10]Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 1–35 (2010)Google Scholar
- [Coq]The Coq Proof Assistant, http://coq.inria.fr/
- [DDMW06]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)Google Scholar
- [DP08]Dziembowski, S., Pietrzak, K.: Leakage-resilient cryptography. In: IEEE 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, pp. 293–302 (2008)Google Scholar
- [Koc96]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)Google Scholar
- [RB95]Rogaway, P., Bellare, M.: Optimal asymmetric encryption how to encrypt with rsa (1995)Google Scholar
- [Zha08]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)Google Scholar