Skip to main content
SpringerLink
Log in

A Verification Framework for Stateful Security Protocols

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10610))

Included in the following conference series:

  • 992 Accesses

Abstract

A long-standing research problem is how to efficiently verify security protocols with tamper-resistant global states, especially when the global states evolve unboundedly. We propose a protocol specification framework, which facilitates explicit modeling of states and state transformations. On the basis of that, we develop an algorithm for verifying security properties of protocols with unbounded state-evolving, by tracking state transformation and checking the validity of the state-evolving traces. We prove the correctness of the verification algorithm, implement both of the specification framework and the algorithm, and evaluate our implementation using a number of stateful security protocols. The experimental results show that our approach is both feasible and practically efficient. Particularly, we have found a security flaw on the digital envelope protocol, which cannot be detected with existing security protocol verifiers.

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 EPUB and 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

References

  1. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proceedings 14th IEEE Computer Security Foundations Workshop (CSFW), pp. 82–96. IEEE CS (2001)

    Google Scholar 

  2. Viganò, L.: Automated security protocol analysis with the avispa tool. Electron. Notes Theoret. Comput. Sci. (ENTCS) 155, 61–86 (2006)

    Article  Google Scholar 

  3. Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03829-7_1

    Chapter  Google Scholar 

  4. Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. In: Proceedings 24th IEEE Symposium on Security and Privacy (S & P), pp. 163–178 (2014)

    Google Scholar 

  5. Herzog, J.: Applying protocol analysis to security device interfaces. IEEE Secur. Priv. 4, 84–87 (2006)

    Article  Google Scholar 

  6. Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: verification of stateful processes. In: Proceedings 24th IEEE Computer Security Foundations Symposium (CSF), pp. 33–47. IEEE CS (2011)

    Google Scholar 

  7. Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proceedings 24th IEEE Computer Security Foundations Symposium (CSF), pp. 66–80. IEEE CS (2011)

    Google Scholar 

  8. Dong, N., Jonker, H., Pang, J.: Challenges in eHealth: from enabling to enforcing privacy. In: Liu, Z., Wassyng, A. (eds.) FHIES 2011. LNCS, vol. 7151, pp. 195–206. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32355-3_12

    Chapter  Google Scholar 

  9. Dong, N., Jonker, H., Pang, J.: Formal analysis of privacy in an ehealth protocol. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 325–342. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33167-1_19

    Chapter  Google Scholar 

  10. Dong, N., Jonker, H.L., Pang, J.: Formal modelling and analysis of receipt-free auction protocols in applied PI. Comput. Secur. 65, 405–432 (2017)

    Article  Google Scholar 

  11. Meier, S., Schmidt, B., Cremers, C., Basin, D.: The 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). doi:10.1007/978-3-642-39799-8_48

    Chapter  Google Scholar 

  12. Li, L., Dong, N., Pang, J., Sun, J., Bai, G., Liu, Y., Dong, J.S.: A verification framework for stateful security protocols - full version (2017). http://www.comp.nus.edu.sg/dongnp/sspa

  13. Ables, K., Ryan, M.D.: Escrowed data and the digital envelope. In: Acquisti, A., Smith, S.W., Sadeghi, A.-R. (eds.) Trust 2010. LNCS, vol. 6101, pp. 246–256. Springer, Heidelberg (2010). doi:10.1007/978-3-642-13869-0_16

    Chapter  Google Scholar 

  14. Microsoft: Bitlocker FAQ (2011). http://technet.microsoft.com/en-us/library/hh831507.aspx

  15. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21, 993–999 (1978)

    Article  MATH  Google Scholar 

  16. Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Inf. Process. Lett. 56, 131–133 (1995)

    Article  MATH  Google Scholar 

  17. Li, L., Dong, N., Pang, J., Sun, J., Bai, G., Liu, Y., Dong, J.S.: SSPA tool, experiment models and evaluation results (2017). http://lilissun.github.io/r/sspa.html

  18. Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29, 198–207 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  19. Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions, composed keys is np-complete. Theoret. Comput. Sci. 299, 451–475 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  20. Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12, 247–311 (2004)

    Article  Google Scholar 

  21. Meier, S.: Advancing automated security protocol verification. Ph.D. thesis, ETH (2013)

    Google Scholar 

  22. Mödersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proceedings 17th ACM Conference on Computer and Communications Security (CCS), pp. 351–360. ACM (2010)

    Google Scholar 

  23. Guttman, J.D.: Fair exchange in strand spaces. In: Proceedings 7th International Workshop on Security Issues in Concurrency (SECCO), EPTCS, vol. 7, pp. 46–60 (2009)

    Google Scholar 

  24. Guttman, J.D.: State and progress in strand spaces: Proving fair exchange. J. Autom. Reasoning 48, 159–195 (2012)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgement

This work is supported by the National Research Foundation, Prime Minister’s Office, Singapore under its National Cybersecurity R&D Program (TSUNAMi project, Award No.NRF2014NCR-NCR001-21) and administered by the National Cybersecurity R&D Directorate.

Author information

Authors and Affiliations

  1. Singapore University of Technology and Design, Singapore, Singapore

    Li Li & Jun Sun

  2. National University of Singapore, Singapore, Singapore

    Naipeng Dong, Guangdong Bai & Jin Song Dong

  3. University of Luxembourg, Luxembourg, Luxembourg

    Jun Pang

  4. Nanyang Technological University, Singapore, Singapore

    Yang Liu

  5. Griffith University, Brisbane, Australia

    Jin Song Dong

Authors
  1. Li Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naipeng Dong
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jun Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jun Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Guangdong Bai
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Jin Song Dong
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Naipeng Dong .

Editor information

Editors and Affiliations

  1. Xidian University, Xi’an, China

    Zhenhua Duan

  2. University of Oxford, Oxford, United Kingdom

    Luke Ong

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Li, L. et al. (2017). A Verification Framework for Stateful Security Protocols. In: Duan, Z., Ong, L. (eds) Formal Methods and Software Engineering. ICFEM 2017. Lecture Notes in Computer Science(), vol 10610. Springer, Cham. https://doi.org/10.1007/978-3-319-68690-5_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68690-5_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68689-9

  • Online ISBN: 978-3-319-68690-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation