Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

Abstract

In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol for multiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.

References

1. M. Abadi and C. Fournet. 2001. Mobile values, new names, and secure communication. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’01). ACM, 104--115.
2. M. Abadi and P. Rogaway. 2002. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 15, 2, 103--127.
3. M. Abdalla, P.-A. Fouque, and D. Pointcheval. 2005. Password-based authenticated key exchange in the three-party setting. In Proceedings of the 8th International Conference on Theory and Practice in Public Key Cryptography (PKC’05). Springer, 65--84.
4. M. Backes, B. Pfitzmann, and M. Waidner. 2003. A composable cryptographic library with nested operations. In Proceedings of the 10th ACM Conference on Computer and Communications Security (CCS’03). ACM, 220--230.
5. G. Bana, P. Adão, and H. Sakurada. 2012. Computationally complete symbolic attacker in action. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’12) (LIPIcs). Schloss Dagstuhl, 546--560.
6. G. Bana and R. Chadha. 2016. Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability. Retrieved from http://eprint.iacr.org/2016/069.
7. G. Bana, R. Chadha, and A. K. Eeralla. 2018. Formal analysis of vote privacy using computationally complete symbolic attacker. In Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS’18). Springer, 350--372.
8. G. Bana and H. Comon-Lundh. 2012. Towards unconditional soundness: Computationally complete symbolic attacker. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST’12). Springer, 189--208.
9. G. Bana and H. Comon-Lundh. 2014. A computationally complete symbolic attacker for equivalence properties. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS’14). ACM, 609--620.
10. G. Bana, K. Hasebe, and M. Okada. 2013. Computationally complete symbolic attacker and key exchange. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS’13). ACM, 1231--1246.
11. G. Barthe, J. M. Crespo, Y. Lakhnech, and B. Schmidt. 2015. Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. Retrieved from http://eprint.iacr.org/.
12. G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-Béguelin. 2011. Computer-aided security proofs for the working cryptographer. In Proceedings of the 31st Annual Conference on Advances in Cryptology (CRYPTO’11). Springer, 71--90.
13. M. Bellare, A. Desai, D. Pointcheval, and P. Rogaway. 1998. Relations among notions of security for public-key encryption schemes. In Proceedings of the 18th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO’98). Springer, 26--45.
14. B. Blanchet. 2005. An automatic security protocol verifier based on resolution theorem proving (invited tutorial). In Proceedings of the 20th International Conference on Automated Deduction (CADE’05). Springer.
15. B. Blanchet. 2008. A computationally sound mechanized prover for security protocols. IEEE Trans. Depend. Secure Comput. 5, 4 (2008), 193--207.
16. D. Boneh. 1998. The decision diffie-hellman problem. In Proceedings of the Conference on Algorithmic Number Theory (ANTS’98). Springer, 48--63.
17. Adam Chlipala. 2013. Certified Programming with Dependent Types—A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. I--XII, 1--424 pages. Retrieved from http://mitpress.mit.edu/books/certified-programming-dependent-types.
18. H. Comon and A. Koutsos. 2017. Formal computational unlinkability proofs of RFID protocols. In Proceedings of the IEEE 30th Computer Security Foundations Symposium (CSF’17). 100--114.
19. H. Comon-Lundh and V. Cortier. 2008. Computational soundness of observational equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS’08). ACM, 109--118.
20. V. Cortier, C. C. Dragan, F. Dupressoir, B. Schmidt, P. Strub, and B. Warinschi. 2017. Machine-checked proofs of privacy for electronic voting protocols. In Proceedings of the IEEE Symposium on Security and Privacy. 993--1008.
21. C. Cremers. 2008. The scyther tool: Verification, falsification, and analysis of security protocols. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08), Vol. 5123. Springer, 414--418.
22. Ajay Kumar Eeralla. 2019. Coq formalization of Computationally Complete Symbolic Attacker. Retrieved from https://bitbucket.org/ajayeeralla/machine-checked-proofs/src/master/.
23. P. Gupta and V. Shmatikov. 2005. Towards computationally sound symbolic analysis of key exchange protocols. In Proceedings of the ACM Workshop on Formal Methods in Security Engineering (FMSE’05). ACM, 23--32.
24. J. Katz and Y. Lindell. 2007. Introduction to Modern Cryptography. Chapman 8 Hall/CRC Press.
25. R. Küsters and M. Tuengerthal. 2009. Computational soundness for key exchange protocols with symmetric encryption. In Proceedings of the ACM Conference on Computer and Communications Security (CCS’09). ACM, 91--100.
26. Guillaume Scerri. 2015. Proofs of security protocols revisited. Thèse de doctorat. Laboratoire Spécification et Vérification, ENS Cachan, France. Retrieved from http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/scerri-phd15.pdf.
27. G. Scerri and S.-O. Ryan. 2016. Analysis of key wrapping APIs: Generic policies, computational security. In Proceedings of the IEEE 29th Computer Security Foundations Symposium (CSF’16). IEEE Computer Society, 281--295.
28. B. Schmidt, S. Meier, C. J. F. Cremers, and D. A. Basin. 2012. Automated analysis of diffie-hellman protocols and advanced security properties. In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF’12). 78--94.
29. Yves Bertot and Pierre Castéran. 2004. A brief overview. In Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer Berlin Heidelberg, 1--11. https://doi.org/10.1007/978-3-662-07964-5_1

Index Terms

• Security and privacy

  • Formal methods and theory of security

    • Formal security models

    • Logic and verification