Skip to main content
SpringerLink
Log in

CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions

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

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

Included in the following conference series:

Abstract

We propose extensions to the Dolev-Yao attacker model to make it suitable for arguments about security of Cyber-Physical Systems. The Dolev-Yao attacker model uses a set of rules to define potential actions by an attacker with respect to messages (i.e. information) exchanged between parties during a protocol execution. As the traditional Dolev-Yao model considers only information (exchanged over a channel controlled by the attacker), the model cannot directly be used to argue about the security of cyber-physical systems where physical-layer interactions are possible. Our Dolev-Yao extension, called Cyber-Physical Dolev-Yao (CPDY), allows additional orthogonal interaction channels between the parties. In particular, such orthogonal channels can be used to model physical-layer mechanical, chemical, or electrical interactions between components. In addition, we discuss the inclusion of physical properties such as location or distance in the rule set. We present an example set of additional rules for the Dolev-Yao attacker, using those we are able to formally discover physical attacks that previously could only be found by empirical methods or detailed physical process models.

M. Rocchetto—The work was carried out while Marco was with iTrust at Singapore University of Technology and Design.

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. Adepu, S., Mathur, A.: An investigation into the response of a water treatment system into cyber attacks. In: IEEE Symposium on High Assurance Systems Engineering (HASE) (2015)

    Google Scholar 

  2. Antonioli, D., Tippenhauer, N.O., MiniCPS: a toolkit for security research on CPS networks. In: Proceedings of Workshop on Cyber-Physical Systems Security & Privay (SPC-CPS), co-located with CCS, October 2015

    Google Scholar 

  3. Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Armando, A., Compagna, L.: SATMC: a SAT-based model checker for security protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 730–733. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. AVANTSSAR. Deliverable 5.3: AVANTSSAR Library of validated problem cases (2010). www.avantssar.eu

  6. Basin, D., Capkun, S., Schaller, P., Schmidt, B.: Formal reasoning about physical properties of security protocols. Trans. Inf. Syst. Secur. (TISSEC) 14(2), 16 (2011)

    Google Scholar 

  7. Basin, D., Cremers, C., Meadows, C.: Model checking security protocols. In: Handbook of Model Checking (2011)

    Google Scholar 

  8. Basin, D., Mödersheim, S., Viganò, L.: OFMC: a symbolic model checker for security protocols. J. Inf. Secur. 4(3), 181–208 (2005)

    Article  Google Scholar 

  9. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundation Workshop (CSFW). IEEE (2001)

    Google Scholar 

  10. Buchler, M., Hossen, K., Mihancea, P., Minea, M., Groz, R., Oriat, C.: Model inference and security testing in the spacios project. In: IEEE Conference on Software Maintenance, Reengineering and Reverse Engineering (CSMR-WCRE) (2014)

    Google Scholar 

  11. Camenisch, J., Mödersheim, S., Sommer, D.: A formal model of identity mixer. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 198–214. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Cárdenas, A.A., Amin, S.M., Sinopoli, B., Giani, A., Perrig, A., Sastry, S.S.: Challenges for securing cyber physical systems. In: Workshop on Future Directions in Cyber-physical Systems Security. DHS, July 2009

    Google Scholar 

  13. Cárdenas, A.A., Roosta, T., Sastry, S.: Rethinking security properties, threat models, and the design space in sensor networks: a case study in scada systems. Ad Hoc Netw. 7(8), 1434–1447 (2009)

    Article  Google Scholar 

  14. Choi, Y.: From NuSMV to SPIN: experiences with model checking flight guidance systems. Formal Methods Syst. Des. 30(3), 199–216 (2007)

    Article  MATH  Google Scholar 

  15. Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006)

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  18. LeMay, E., Ford, M.D., Keefe, K., Sanders, W.H., Muehrcke, C.: Model-based security metrics using adversary view security evaluation (ADVISE). In: Proceedings of Conference on Quantitative Evaluation of Systems, QEST (2011)

    Google Scholar 

  19. Mathur, A., Tippenhauer, N.O.: A water treatment testbed for research and training on ICS security. In: Proceedings of Workshop on Cyber-Physical Systems for Smart Water Networks (CySWater), April 2016

    Google Scholar 

  20. Mo, Y., Kim, T.-H., Brancik, K., Dickinson, D., Lee, H., Perrig, A., Sinopoli, B.: Cyber-physical security of a smart grid infrastructure. Proc. IEEE 100(1), 195–209 (2012)

    Article  Google Scholar 

  21. Morris, T., Srivastava, A., Reaves, B., Gao, W., Pavurapu, K., Reddi, R.: A control system testbed to validate critical infrastructure protection concepts. J. Crit. Infrastruct. Prot. 4(2), 88–103 (2011)

    Article  Google Scholar 

  22. Reaves, B., Morris, T.: An open virtual testbed for industrial control system security research. J. Inf. Secur. 11(4), 215–229 (2012)

    Article  Google Scholar 

  23. Rocchetto, M., Ochoa, M., Torabi Dashti, M.: Model-based detection of CSRF. In: Cuppens-Boulahia, N., Cuppens, F., Jajodia, S., Abou El Kalam, A., Sans, T. (eds.) SEC 2014. IFIP AICT, vol. 428, pp. 30–43. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  24. Rocchetto, M., Tippenhauer, N.O.: CPDY (Cyber-Physical Dolev-Yao) (2016). http://research.scy-phy.net/cpdy/

  25. Rocchetto, M., Viganò, L., Volpe, M., Vedove, G.D.: Using interpolation for the verification of security protocols. In: Accorsi, R., Ranise, S. (eds.) STM 2013. LNCS, vol. 8203, pp. 99–114. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Schaller, P., Schmidt, B., Basin, D.A., Capkun, S.: Modeling and verifying physical properties of security protocols for wireless networks. In: Computer Security Foundations Symposium (CSF), pp. 109–123 (2009)

    Google Scholar 

  27. Schmidt, B., Sasse, R., Cremers, C., Basin, D.A.: Automated verification of group key agreement protocols. In: Symposium on Security and Privacy (S&P), pp. 179–194 (2014)

    Google Scholar 

  28. Schmidt, M., Lipson, H.: Distilling free-form natural laws from experimental data. Science 324(5923), 81–85 (2009)

    Article  Google Scholar 

  29. SPaCIoS. Deliverable 3.3.2: Methodology and technology forvulnerability-driven security testing (final version) (2014). http://www.spacios.eu

  30. Steinmetzer, D., Schulz, M., Hollick, M.: Lockpicking physical layer key exchange: weak adversary models invite the thief. In: Proceedings of ACM Conference Wireless Security (WiSeC) (2015)

    Google Scholar 

  31. Taormina, R., Galelli, S., Tippenhauer, N.O., Salomons, E., Ostfeld, A.: Simulation of cyber-physical attacks on water distribution systems with EPANET. In: Proceedings of Singapore Cyber Security R&D Conference (SG-CRC), January 2016

    Google Scholar 

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

  33. Urbina, D., Giraldo, J., Tippenhauer, N.O., Cardenas, A.: Attacking fieldbus communications in ICS: applications to the SWaT testbed. In: Proceedings of Singapore Cyber Security R&D Conference (SG-CRC), January 2016

    Google Scholar 

  34. Viganò, L.: The spacios project: secure provision and consumption in the internet of services. In: Software Testing, Verification and Validation (ICST), pp. 497–498. IEEE (2013)

    Google Scholar 

  35. Vigo, R.: The cyber-physical attacker. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP Workshops 2012. LNCS, vol. 7613, pp. 347–356. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  36. von Oheimb, D.: The high-level protocol specification language HLPSL developed in the EU project AVISPA. In: Proceedings of APPSEM 2005 workshop, pp. 1–17 (2005)

    Google Scholar 

  37. von Oheimb, D., Mödersheim, S.: ASLan++ — a formal security specification language for distributed systems. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 1–22. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  38. Weinberger, S.: Computer security: is this the start of cyberwarfare? Nature 174, 142–145 (2011)

    Article  Google Scholar 

Download references

Acknowledgments

This work was supported by the National Research Foundation of Singapore under grant NRF2014NCR-NCR001-40.

Author information

Authors and Affiliations

  1. SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg

    Marco Rocchetto

  2. ISTD, Singapore University of Technology and Design, Singapore, Singapore

    Nils Ole Tippenhauer

Authors
  1. Marco Rocchetto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nils Ole Tippenhauer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nils Ole Tippenhauer .

Editor information

Editors and Affiliations

  1. School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan

    Kazuhiro Ogata

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    Mark Lawford

  3. Department of Computer Science, Hosei University, Tokyo, Japan

    Shaoying Liu

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Rocchetto, M., Tippenhauer, N.O. (2016). CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions. In: Ogata, K., Lawford, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47846-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47845-6

  • Online ISBN: 978-3-319-47846-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation