Skip to main content
SpringerLink
Log in

Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties

  • Conference paper
Formal Aspects in Security and Trust (FAST 2009)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 5983))

Included in the following conference series:

Abstract

Recently Kuesters et al proposed two new methods using ProVerif for analyzing cryptographic protocols with Exclusive-Or and Diffie-Hellman properties. Some tools, for instance CL-Atse and OFMC, are able to deal with Exclusive-Or and Diffie-Hellman. In this article we compare time efficiency of these tools verifying some protocols of the litterature that are designed with such algebraic properties.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Acess Control (MAC) and Physical (PHY) Specifications (1999)

    Google Scholar 

  2. Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Michael, R., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Armando, A., Compagna, L.: An optimized intruder model for SAT-based model-checking of security protocols. In: Armando, A., Viganò, L. (eds.) ENTCS, March 2005, vol. 125, pp. 91–108. Elsevier Science Publishers, Amsterdam (2005)

    Google Scholar 

  4. Armando, A., Basin, D.A., Bouallagui, M., Chevalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The aviss security protocol analysis tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 349–353. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Ateniese, G., Steiner, M., Tsudik, G.: New multiparty authentication services and key agreement protocols. IEEE Journal of Selected Areas in Communications 18(4), 628–639 (2000)

    Article  Google Scholar 

  6. Basin, D., Mödersheim, S., Viganò, L.: An On-The-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)

    Google Scholar 

  7. 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)

    Article  Google Scholar 

  8. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. CSFW 2001, pp. 82–96. IEEE Comp. Soc. Press, Los Alamitos (2001)

    Google Scholar 

  9. Blanchet, B.: Cryptographic Protocol Verifier User Manual (2004)

    Google Scholar 

  10. Boichut, Y., Héam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proc. AVIS 2004 (April 2004)

    Google Scholar 

  11. Bozga, L., Lakhnech, Y., Perin, M.: HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. In: Computer Aided Verification (2003)

    Google Scholar 

  12. Bull, J., Otway, D.J.: The authentication protocol. Technical Report DRA/CIS3/PROJ/CORBA/SC/1/CSM/436-04/03, Defence Research Agency (1997)

    Google Scholar 

  13. Cheminod, M., Cibrario Bertolotti, I., Durante, L., Sisto, R., Valenzano, A.: Experimental comparison of automatic tools for the formal analysis of cryptographic protocols. In: DepCoS-RELCOMEX 2007, Szklarska Poreba, Poland, June 14-16, pp. 153–160. IEEE Computer Society Press, Los Alamitos (2007)

    Google Scholar 

  14. Chen, X., van Deursen, T., Pang, J.: Improving automatic verification of security protocols with xor. In: Cavalcanti, A. (ed.) ICFEM 2009. LNCS, vol. 5885, pp. 107–126. Springer, Heidelberg (2009)

    Google Scholar 

  15. Clark, J., Jacob, J.: A survey of authentication protocol literature (1997), http://www.cs.york.ac.uk/~jac/papers/drareviewps.ps

  16. Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 326–341. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)

    Google Scholar 

  18. Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)

    Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic protocol analysis. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds.) Formal to Practical Security. LNCS, vol. 5458, pp. 70–94. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information Society 22(6), 644–654 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  22. Escobar, S., Meadows, C., Meseguer, J.: Maude-npa: Cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2007)

    Google Scholar 

  23. Gong, L.: Using one-way functions for authentication. SIGCOMM Computer Communication 19(5), 8–11 (1989)

    Article  Google Scholar 

  24. Liaw, H.-T., Juang, W.-S., Lin, C.-K.: An electronic online bidding auction protocol with both security and efficiency. Applied mathematics and computation 174, 1487–1497 (2008)

    Article  MathSciNet  Google Scholar 

  25. Hussain, M., Seret, D.: A comparative study of security protocols validation tools: HERMES vs. AVISPA. In: Proc. ICACT 2006, vol. 1, pp. 303–308 (2006)

    Google Scholar 

  26. Klay, F., Vigneron, L.: Automatic methods for analyzing non-repudiation protocols with an active intruder. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 192–209. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. Küsters, R., Truderung, T.: Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In: Proceedings of the 22nd Computer Security Foundations Symposium (CSF), pp. 157–171. IEEE Computer Society, Los Alamitos (2009)

    Chapter  Google Scholar 

  28. Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the horn theory based approach. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conference on Computer and Communications Security, pp. 129–138. ACM, New York (2008)

    Google Scholar 

  29. Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the horn theory based approach. In: ACM Conference on Computer and Communications Security, pp. 129–138 (2008)

    Google Scholar 

  30. Lafourcade, P., Terrade, V., Vigier, S.: Comparison of cryptographic verification tools dealing with algebraic properties. Technical Report TR-2009-16, Verimag (October 2009)

    Google Scholar 

  31. Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1-2), 53–84 (1998)

    Google Scholar 

  32. Lowe, G., Roscoe, A.W.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering 23(10), 659–669 (1997)

    Article  Google Scholar 

  33. Meadows, C.: Language generation and verification in the NRL protocol analyzer. In: Proc. CSFW 1996, pp. 48–62. IEEE Comp. Soc. Press, Los Alamitos (1996)

    Google Scholar 

  34. Meadows, C.: Analyzing the needham-schroeder public-key protocol: A comparison of two approaches. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 351–364. Springer, Heidelberg (1996)

    Google Scholar 

  35. Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: IEEE Symposium on Security and Privacy (May 1997)

    Google Scholar 

  36. Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communication of the ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  37. Roscoe, A.W.: Model-checking CSP. Prentice-Hall, Englewood Cliffs (1994)

    Google Scholar 

  38. Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol. a cautionary tale. Inf. Process. Lett. 65(1), 7–10 (1998)

    Article  Google Scholar 

  39. Schneier, B.: Applied Cryptography, 2nd edn. Wiley, Chichester (1996)

    Google Scholar 

  40. Simmons, G.J.: Cryptoanalysis and protocol failures. Communications of the ACM 37(11), 56–65 (1994)

    Article  Google Scholar 

  41. Song, D., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9(1/2), 47–74 (2001)

    Google Scholar 

  42. Tatebayashi, M., Matsuzaki, N., Newman, D.B.: Key distribution protocol for digital mobile communication systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324–334. Springer, Heidelberg (1990)

    Google Scholar 

  43. Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  44. Viganò, L.: Automated security protocol analysis with the AVISPA tool. ENTCS 155, 61–86 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, Université Grenoble 1, Verimag, France

    Pascal Lafourcade, Vanessa Terrade & Sylvain Vigier

Authors
  1. Pascal Lafourcade
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vanessa Terrade
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sylvain Vigier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Largo Bruno Pontecorvo, 3, 56127, Pisa, Italy

    Pierpaolo Degano

  2. The MITRE Corporation, 202 Burlington Rd, MS S128, MA 01730, Bedford, USA

    Joshua D. Guttman

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lafourcade, P., Terrade, V., Vigier, S. (2010). Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties. In: Degano, P., Guttman, J.D. (eds) Formal Aspects in Security and Trust. FAST 2009. Lecture Notes in Computer Science, vol 5983. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12459-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-12459-4_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-12458-7

  • Online ISBN: 978-3-642-12459-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation