A Computationally Complete Symbolic Attacker for Equivalence Properties

ABSTRACT

We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.

References

1. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In POPL'01, pages 104--115. ACM, 2001.
2. M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2):103--127, 2002.
3. Martın Abadi and Cédric Fournet. Private authentication. Theor. Comput. Sci., 322(3):427--476, September 2004.
4. M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In CCS'03, pages 220--230. ACM, 2003.
5. G. Bana, P. Adao, and H. Sakurada. Computationally Comlete Symbolic Attacker in Action. In FSTTCS'12, LIPIcs, pages 546--560. Schloss Dagstuhl, 2012.
6. G. Bana and H. Comon-Lundh. Towards unconditional soundness: Computationally complete symbolic attacker. In POST'12, LNCS, pages 189--208. Springer, 2012.
7. G. Bana, K. Hasebe, and M. Okada. Computationally complete symbolic attacker and key exchange. In CCS '13, pages 1231--1246. ACM, 2013.
8. G. Bana, P. Mohassel, and T. Stegers. Computational soundness of formal indistinguishability and static equivalence. In ASIAN'06, volume 4435 of LNCS, pages 182--196. Springer, 2007.
9. G. Barthe, M. Daubignard, B. M. Kapron, and Y. Lakhnech. Computational indistinguishability logic. In CCS'10, pages 375--386. ACM, 2010.
10. G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-Béguelin. Computer-aided security proofs for the working cryptographer. In CRYPTO 2011, volume 6841 of LNCS, pages 71--90. Springer, 2011.
11. M. Bellare, A. Boldyreva, A. Desai, and D. Pointcheval. Key-privacy in public-key encryption. In ASIACRYPT 2001, volume 2248 of LNCS, pages 566--582. Springer, 2001.
12. M. Bellare, A. Desai, D. Pointcheval, and Ph. Rogaway. Relations among notions of security for public-key encryption schemes. In CRYPTO'98, LNCS. Springer, 1998.
13. B. Blanchet. An automatic security protocol verifier based on resolution theorem proving (invited tutorial). In CADE'05, Tallinn, Estonia, July 2005.
14. B. Blanchet. A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193--207, 2008.
15. B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. J. of Logic and Algebraic Programming, 75(1):3--51, 2008.
16. V. Cheval and B. Blanchet. Proving more observational equivalences with proverif. In POST'13, Lecture Notes in Computer Science, pages 226--246. Springer, 2013.
17. Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Trace equivalence decision: Negative tests and non-determinism. In CCS'11, pages 321--330. ACM, 2011.
18. H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. In CCS'08, pages 109--118. ACM, 2008.
19. H. Comon-Lundh, V. Cortier, and G. Scerri. Security proof with dishonest keys. In POST'12, LNCS, pages 149--168. Springer, 2012.
20. H. Comon-Lundh, V. Cortier, and G. Scerri. Tractable inference systems: an extension with a deducibility predicate. In CADE'13, LNAI. Springer, 2013.
21. Hubert Comon-Lundh, Masami Hagiya, Yusuke Kawamoto, and Hideki Sakurada. Computational soundness of indistinguishability properties without computable parsing. In ISPEC'12, pages 63--79. Springer, 2012.
22. C. Cremers. The scyther tool: Verification, falsification, and analysis of security protocols. In CAV'08, volume 5123 of LNCS, pages 414--418. Springer, 2008.
23. C. Ene, Y. Lakhnech, and V. C. Ng. Formal indistinguishability extended to the random oracle model. In ESORICS'09, volume 5789 of LNCS, pages 555--570. Springer, 2009.
24. A. Armando et al. The AVISPA Tool for the automated validation of internet security protocols and applications. In CAV'05, volume 3576 of LNCS, pages 281--285, 2005.
25. Bogdan Warinschi. A computational analysis of the needham-schroeder protocol. In 16th Computer security foundation workshop (CSFW), pages 248--262. IEEE, 2003.

Index Terms

• Networks

  • Network protocols

    • Protocol correctness

      • Protocol testing and verification