Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Automatic Methods for Analyzing Non-repudiation Protocols with an Active Intruder

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

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

Included in the following conference series:

Abstract

Non-repudiation protocols have an important role in many areas where secured transactions with proofs of participation are necessary. Formal methods are clever and without error, therefore using them for verifying such protocols is crucial. In this purpose, we show how to partially represent non-repudiation as a combination of authentications on the Fair Zhou-Gollmann protocol. After discussing the limitations of this method, we define a new one, based on the handling of the knowledge of protocol participants. This second method is general and of natural use, as it consists in adding simple annotations in the protocol specification. It is very easy to implement in tools able to handle participants knowledge. We have implemented it in the AVISPA Tool and analyzed the Fair Zhou-Gollmann protocol and the optimistic Cederquist-Corin-Dashti protocol, discovering attacks in each. This extension of the AVISPA Tool for handling non-repudiation opens a highway to the specification of many other properties, without any more change in the tool itself.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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.

Similar content being viewed by others

References

  1. http://www.lsv.ens-cachan.fr/~kremer/FXbib/references.php

  2. Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., 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., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: 20th IEEE Computer Security Foundations Symp., CSF, pp. 385–396. IEEE Computer Society, Los Alamitos (2007)

    Google Scholar 

  4. Bella, G., Paulson, L.C.: Mechanical Proofs about a Non-repudiation Protocol. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 91–104. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Carbonell, M., Sierra, J.M., Onieva, J.A., Lopez, J., Zhou, J.: Estimation of TTP Features in Non-repudiation Service. In: Gervasi, O., Gavrilova, M.L. (eds.) ICCSA 2007, Part II. LNCS, vol. 4706, pp. 549–558. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Cederquist, J., Corin, R., Dashti, M.T.: On the Quest for Impartiality: Design and Analysis of a Fair Non-repudiation Protocol. In: Qing, S., Mao, W., López, J., Wang, G. (eds.) ICICS 2005. LNCS, vol. 3783, pp. 27–39. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Mantovani, J., Mödersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Proc. of Work. on Specification and Automated Processing of Security Requirements, SAPS, Linz, Austria, vol. 180. Oesterreichische Computer Gesellschaft (Austrian Computer Society) (September 2004)

    Google Scholar 

  8. Compagna, L.: SAT-based Model-Checking of Security Protocols. PhD thesis, Università degli Studi di Genova and the University of Edinburgh (2005)

    Google Scholar 

  9. Gürgens, S., Rudolph, C.: Security Analysis of Efficient (Un-)fair Non-repudiation Protocols. Formal Aspects of Computing 17(3), 260–276 (2005)

    Article  MATH  Google Scholar 

  10. Gürgens, S., Rudolph, C., Vogt, H.: On the Security of Fair Non-repudiation Protocols. Int. Journal of Information Security 4, 253–262 (2005)

    Article  MATH  Google Scholar 

  11. Guttman, J.D.: Authentication tests and disjoint encryption: A design method for security protocols. Journal of Computer Security 12(3-4), 409–433 (2004)

    Article  Google Scholar 

  12. Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS, vol. 1955, pp. 131–160. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Kremer, S., Markowitch, O.: Optimistic Non-repudiable Information Exchange. In: Biemond, J. (ed.) 21st Symp. on Information Theory in the Benelux, Wassenaar, NL, pp. 139–146. Werkgemeenschap Informatieen Communicatietheorie, Enschede (2000)

    Google Scholar 

  14. Kremer, S., Markowitch, O., Zhou, J.: An Intensive Survey of Fair Non-repudiation Protocols. Computer Communications 25(17), 1606–1621 (2002)

    Article  Google Scholar 

  15. Kremer, S., Raskin, J.-F.: A Game-Based Verification of Non-repudiation and Fair Exchange Protocols. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 551–565. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Lowe, G.: A Hierarchy of Authentication Specification. In: 10th Computer Security Foundations Work., CSFW, Rockport, Massachusetts, USA, pp. 31–44. IEEE Computer Society, Los Alamitos (1997)

    Google Scholar 

  17. Markowitch, O., Kremer, S.: An Optimistic Non-repudiation Protocol with Transparent Trusted Third Party. In: Davida, G.I., Frankel, Y. (eds.) ISC 2001. LNCS, vol. 2200, pp. 363–378. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Markowitch, O., Roggeman, Y.: Probabilistic Non-Repudiation without Trusted Third Party. In: 2nd Work. on Security in Communication Networks, Amalfi, Italy (1999)

    Google Scholar 

  19. Ochsenschläger, P., Repp, J., Rieke, R., Nitsche, U.: The SH-Verification Tool - Abstraction-Based Verification of Co-operating Systems. Formal Aspects of Computing 10(4), 381–404 (1998)

    Article  MATH  Google Scholar 

  20. Pagnia, H., Gärtner, F.C.: On the Impossibility of Fair Exchange without a Trusted Third Party. Technical Report TUD-BS-1999-02, Darmstadt University of Technology, Darmstadt, Germany (1999)

    Google Scholar 

  21. Pancho-Festin, S., Gollmann, D.: On the Formal Analyses of the Zhou-Gollmann Non-repudiation Protocol. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 5–15. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Englewood Cliffs (1997)

    Google Scholar 

  23. Ryan, P., Goldsmith, M., Lowe, G., Roscoe, B., Schneider, S.: Modelling and Analysis of Security Protocols. Addison Wesley, Reading (2000)

    Google Scholar 

  24. Santiago, J., Vigneron, L.: Optimistic Non-repudiation Protocol Analysis. In: Sauveron, D., Markantonakis, K., Bilas, A., Quisquater, J.-J. (eds.) WISTP 2007. LNCS, vol. 4462, pp. 90–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Schneider, S.: Formal Analysis of a Non-Repudiation Protocol. In: Proc. of The 11th Computer Security Foundations Work, pp. 54–65. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  26. Shmatikov, V., Mitchell, J.C.: Analysis of abuse-free contract signing. In: Frankel, Y. (ed.) FC 2000. LNCS, vol. 1962, pp. 174–191. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  27. Wei, K., Heather, J.: Towards verification of timed non-repudiation protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 244–257. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  28. Wei, K., Heather, J.: A theorem-proving approach to verification of fair non-repudiation protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 202–219. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  29. Zhou, J., Deng, R.H., Bao, F.: Evolution of fair non-repudiation with TTP. In: Pieprzyk, J.P., Safavi-Naini, R., Seberry, J. (eds.) ACISP 1999. LNCS, vol. 1587, pp. 258–269. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  30. Zhou, J., Gollmann, D.: A Fair Non-repudiation Protocol. In: IEEE Symp. on Security and Privacy, Oakland, CA, USA, pp. 55–61. IEEE Computer Society, Los Alamitos (1996)

    Google Scholar 

  31. Zhou, J., Gollmann, D.: Towards verification of non-repudiation protocols. In: Proc. of Int. Refinement Work. and Formal Methods Pacific, Canberra, Australia, pp. 370–380 (September 1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. France Telecom R&D, Lannion, France

    Francis Klay

  2. LORIA, Nancy Université, Vandoeuvre-lès-Nancy, France

    Laurent Vigneron

Authors
  1. Francis Klay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laurent Vigneron
    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 Guttman

  3. Istituto di Informatica e Telematica - IIT Consiglio Nazionale delle Ricerche, C.N.R., Pisa Research Area, Via. G. Moruzzi 1, 56125, Pisa, Italy

    Fabio Martinelli

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klay, F., Vigneron, L. (2009). Automatic Methods for Analyzing Non-repudiation Protocols with an Active Intruder. In: Degano, P., Guttman, J., Martinelli, F. (eds) Formal Aspects in Security and Trust. FAST 2008. Lecture Notes in Computer Science, vol 5491. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01465-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-01465-9_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-01464-2

  • Online ISBN: 978-3-642-01465-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation