Advertisement

Abstractions for Security Protocol Verification

  • Binh Thanh Nguyen
  • Christoph Sprenger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9036)

Abstract

We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We propose typed abstractions, which transform a term’s structure based on its type, and untyped abstractions, which remove atomic messages, variables, and redundant terms. Our theory improves on previous work by supporting a useful subclass of shallow subterm-convergent rewrite theories, user-defined types, and untyped variables to cover type flaw attacks. We prove soundness results for an expressive property language that includes secrecy and authentication. Applying our abstractions to realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers.

Keywords

Equational Theory Security Protocol Extensible Authentication Protocol Cryptographic Operation Ground Substitution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cuéllar, J., Erzse, G., Frau, S., Minea, M., Mödersheim, S., von Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Viganò, L.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Arapinis, M., Duflot, M.: Bounding messages for free in security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 376–387. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Arkko, J., Haverinen, H.: RFC 4187: Extensible authentication protocol method for 3rd generation authentication and key agreement (EAP-AKA) (2006), http://www.ietf.org/rfc/rfc4187
  4. 4.
    Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. International Journal of Information Security 7(1), 3–32 (2008)CrossRefGoogle Scholar
  5. 5.
    Basin, D.A., Mödersheim, S., Viganó, L.: OFMC: A symbolic model checker for security protocols. Int. J. Inf. Sec. 4(3), 181–208 (2005)CrossRefGoogle Scholar
  6. 6.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001)Google Scholar
  7. 7.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL, pp. 238–252. ACM (1977)Google Scholar
  8. 8.
    Cremers, C.: IKEv1 and IKEv2 protocol suites (2011), https://github.com/cascremers/scyther/tree/master/gui/Protocols/IKE
  9. 9.
    Cremers, C.: ISO/IEC 9798 authentication protocols (2012), https://github.com/cascremers/scyther/tree/master/gui/Protocols/ISO-9798
  10. 10.
    Cremers, C.J.F.: The Scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Cremers, C.: Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 315–334. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  12. 12.
    Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW) (2004)Google Scholar
  13. 13.
    Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13, 423–482 (2005)Google Scholar
  14. 14.
    Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)Google Scholar
  15. 15.
    Guttman, J.D.: Transformations between cryptographic protocols. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 107–123. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Guttman, J.D.: Security goals and protocol transformations. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 130–147. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  17. 17.
    Harkins, D., Carrel, D.: The Internet Key Exchange (IKE) IETF RFC 2409 (Proposed Standard) (November 1998), http://www.ietf.org/rfc/rfc2409.txt
  18. 18.
    Hui, M.L., Lowe, G.: Fault-preserving simplifying transformations for security protocols. Journal of Computer Security 9(1/2), 3–46 (2001)Google Scholar
  19. 19.
    Jouannaud, J., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Kaufman, C., Hoffman, P., Nir, Y., Eronen, P.: Internet Key Exchange Protocol Version 2 (IKEv2). IETF RFC 5996 (September 2010), http://tools.ietf.org/html/rfc5996
  21. 21.
    Meier, S., Schmidt, B., Cremers, C., Basin, D.: TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  22. 22.
    Nguyen, B.T., Sprenger, C.: Sound security protocol transformations. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 83–104. Springer, Heidelberg (2013)Google Scholar
  23. 23.
    Nguyen, B.T., Sprenger, C.: Abstractions for security protocol verification. Tech. rep. Department of Computer Science, ETH Zurich (January 2015), http://dx.doi.org/10.3929/ethz-a-010347780
  24. 24.
    Paulson, L.: The inductive approach to verifying cryptographic protocols. J. Computer Security 6, 85–128 (1998)Google Scholar
  25. 25.
    Pavlovic, D., Meadows, C.: Deriving secrecy in key establishment protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 384–403. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  26. 26.
    Turuani, M.: The CL-atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Binh Thanh Nguyen
    • 1
  • Christoph Sprenger
    • 1
  1. 1.Institute of Information Security Department of Computer ScienceETH ZurichZürichSwitzerland

Personalised recommendations