SpringerLink
Log in

Formal Analysis of Security Properties on the OPC-UA SCADA Protocol

  • Conference paper
  • First Online:
Computer Safety, Reliability, and Security (SAFECOMP 2016)

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

Included in the following conference series:

Abstract

Industrial systems are publicly the target of cyberattacks since Stuxnet [1]. Nowadays they are increasingly communicating over insecure media such as Internet. Due to their interaction with the real world, it is crucial to prove the security of their protocols. In this paper, we formally study the security of one of the most used industrial protocols: OPC-UA. Using ProVerif, a well known cryptographic protocol verification tool, we are able to check secrecy and authentication properties. We find several attacks on the protocols and provide countermeasures.

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
EUR 32.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
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://freeopcua.github.io/.

  2. 2.

    http://indusprotoverif.forge.imag.fr/PPL16.tar.gz.

References

  1. Langner, R.: Stuxnet: dissecting a cyberwarfare weapon. IEEE Secur. Priv. 9(3), 49–51 (2011)

    Article  Google Scholar 

  2. Stouffer, K., Falco, J., Karen, S.: Guide to industrial control systems (ICS) security. NIST Spec. Publ. 800(82), 16–16 (2011)

    Google Scholar 

  3. ANSSI. Managing cybersecurity for ICS, June 2012

    Google Scholar 

  4. Igure, V.M., Laughter, S.A., Williams, R.D.: Security issues in SCADA networks. Comput. Secur. 25(7), 498–506 (2006)

    Article  Google Scholar 

  5. Patel, S.C., Bhatt, G.D., Graham, J.H.: Improving the cyber security of SCADA communication networks. Commun. ACM 52(7), 139–142 (2009)

    Article  Google Scholar 

  6. Clarke, G.R., Reynders, D., Wright, E.: Practical modern SCADA protocols: DNP3, 60870.5 and related systems. Newnes (2004)

    Google Scholar 

  7. Dzung, D., Naedele, M., von Hoff, T.P., Crevatin, M.: Security for industrial communication systems. Proc. IEEE 93(6), 1152–1177 (2005)

    Article  Google Scholar 

  8. Wanying, Q., Weimin, W., Surong, Z., Yan, Z.: The study of security issues for the industrial control systems communication protocols. In: JIMET 2015 (2015)

    Google Scholar 

  9. Patel, S.C., Yu, Y.: Analysis of SCADA security models. Int. Manag. Rev. 3(2), 68 (2007)

    Google Scholar 

  10. Fovino, I., Carcano, A., Masera, M., Trombetta, A.: Design and implementation of a secure MODBUS protocol. In: IFIP AICT 2009 (2009)

    Google Scholar 

  11. Hayes, G., El-Khatib, K.: Securing MODBUS transactions using hash-based message authentication codes and stream transmission control protocol. In: ICCIT 2013, June 2013

    Google Scholar 

  12. Graham, J.H., Patel, S.C.: Correctness proofs for SCADA communication protocols. In: WM-SCI 2005 (2005)

    Google Scholar 

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

    Chapter  Google Scholar 

  14. Saul, E., Hutchison, A.: SPEAR II - the security protocol engineering and analysis resource (1999)

    Google Scholar 

  15. Lafourcade, P., Puys, M.: Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: Garcia-Alfaro, J., et al. (eds.) FPS 2015. LNCS, vol. 9482, pp. 137–155. Springer, Heidelberg (2016). doi:10.1007/978-3-319-30303-1_9

    Chapter  Google Scholar 

  16. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSF 2001 (2001)

    Google Scholar 

  17. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  18. Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol, version 1.2. IETFRFC 5246, August 2008

    Google Scholar 

  19. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS 1996 (1996)

    Google Scholar 

  20. Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6 (1996)

    Article  Google Scholar 

  21. Focardi, R., Luccio, F.L., Steel, G.: An introduction to security api analysis. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 35–65. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Mahnke, W., Leitner, S., Damm, M.: OPC Unified Architecture. Springer, Heidelberg (2009)

    Book  Google Scholar 

  23. OPC Unified Architecture. Part 2: Security model, April 2013

    Google Scholar 

  24. OPC Unified Architecture. Part 4: Services, August 2012

    Google Scholar 

  25. OPC Unified Architecture. Part 6: Map**s, August 2012

    Google Scholar 

Download references

Acknowledgements

This work has been partially funded by the CNRS PEPS SISC ASSI 2016, the LabEx PERSYVAL-Lab (ANR-11-LABX-0025), the ARAMIS project (PIA P3342-146798) and “Digital trust” Chair from the University of Auvergne Foundation.

Author information

Authors and Affiliations

  1. Verimag, University of Grenoble Alpes, Saint-Martin-D’hères, France

    Maxime Puys, Marie-Laure Potet & Pascal Lafourcade

  2. LIMOS, University of Clermont Auvergne, Campus des Cézeaux, Aubière, France

    Pascal Lafourcade

Authors
  1. Maxime Puys
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marie-Laure Potet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pascal Lafourcade
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maxime Puys .

Editor information

Editors and Affiliations

  1. Norwegian University of Science and Technology , Trondheim, Norway

    Amund Skavhaug

  2. University of Toulouse , Toulouse, France

    Jérémie Guiochet

  3. Thales Transportation Systems GmbH , Ditzingen, Germany

    Friedemann Bitsch

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Puys, M., Potet, ML., Lafourcade, P. (2016). Formal Analysis of Security Properties on the OPC-UA SCADA Protocol. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2016. Lecture Notes in Computer Science(), vol 9922. Springer, Cham. https://doi.org/10.1007/978-3-319-45477-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45477-1_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45476-4

  • Online ISBN: 978-3-319-45477-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation