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

  • Maxime PuysEmail author
  • Marie-Laure Potet
  • Pascal Lafourcade
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9922)


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.


Transmission Control Protocol Security Property Formal Verification Message Authentication Code Stream Transmission Control Protocol 
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.



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.


  1. 1.
    Langner, R.: Stuxnet: dissecting a cyberwarfare weapon. IEEE Secur. Priv. 9(3), 49–51 (2011)CrossRefGoogle Scholar
  2. 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. 3.
    ANSSI. Managing cybersecurity for ICS, June 2012Google Scholar
  4. 4.
    Igure, V.M., Laughter, S.A., Williams, R.D.: Security issues in SCADA networks. Comput. Secur. 25(7), 498–506 (2006)CrossRefGoogle Scholar
  5. 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)CrossRefGoogle Scholar
  6. 6.
    Clarke, G.R., Reynders, D., Wright, E.: Practical modern SCADA protocols: DNP3, 60870.5 and related systems. Newnes (2004)Google Scholar
  7. 7.
    Dzung, D., Naedele, M., von Hoff, T.P., Crevatin, M.: Security for industrial communication systems. Proc. IEEE 93(6), 1152–1177 (2005)CrossRefGoogle Scholar
  8. 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. 9.
    Patel, S.C., Yu, Y.: Analysis of SCADA security models. Int. Manag. Rev. 3(2), 68 (2007)Google Scholar
  10. 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. 11.
    Hayes, G., El-Khatib, K.: Securing MODBUS transactions using hash-based message authentication codes and stream transmission control protocol. In: ICCIT 2013, June 2013Google Scholar
  12. 12.
    Graham, J.H., Patel, S.C.: Correctness proofs for SCADA communication protocols. In: WM-SCI 2005 (2005)Google Scholar
  13. 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)CrossRefGoogle Scholar
  14. 14.
    Saul, E., Hutchison, A.: SPEAR II - the security protocol engineering and analysis resource (1999)Google Scholar
  15. 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 CrossRefGoogle Scholar
  16. 16.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSF 2001 (2001)Google Scholar
  17. 17.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol, version 1.2. IETFRFC 5246, August 2008Google Scholar
  19. 19.
    Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS 1996 (1996)Google Scholar
  20. 20.
    Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6 (1996)CrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 22.
    Mahnke, W., Leitner, S., Damm, M.: OPC Unified Architecture. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  23. 23.
    OPC Unified Architecture. Part 2: Security model, April 2013Google Scholar
  24. 24.
    OPC Unified Architecture. Part 4: Services, August 2012Google Scholar
  25. 25.
    OPC Unified Architecture. Part 6: Mappings, August 2012Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Maxime Puys
    • 1
    Email author
  • Marie-Laure Potet
    • 1
  • Pascal Lafourcade
    • 1
    • 2
  1. 1.VerimagUniversity of Grenoble AlpesSaint-Martin-D’hèresFrance
  2. 2.LIMOSUniversity of Clermont AuvergneAubièreFrance

Personalised recommendations