Abstract
The large cyberphysical systems that are currently being developed such as Car2X come with sophisticated security architectures that involve a complex interplay of security protocols and security APIs. Although formal methods for security protocols have achieved a mature stage there are still many challenges left. One is to improve the verification of equivalence-based security properties. A second challenge is the compositionality problem: how can the security of a composition of security protocols and APIs be derived from the security of its components. It seems intuitively clear that foundational results on causal equivalences and process calculi could help in this situation. In this talk we first identify four ways to exploit causality in security verification. In particular, this will lead us to review results on causal equivalences. Finally, we discuss how such results could help us to tackle the two challenges.
This work is partially supported by the Niedersächsisches Vorab of the Volkswagen Foundation and the Ministry of Science and Culture of Lower Saxony as part of the Interdisciplinary Research Center on Critical Systems Engineering for Socio-Technical Systems.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Composition Operator
- Security Protocol
- Parallel Composition
- Security Architecture
- Behavioural Equivalence
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.
References
Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6–15 (1996)
Arapinis, M., Cheval, V., Delaune, S.: Composing security protocols: from confidentiality to privacy. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 324–343. Springer, Heidelberg (2015)
Bednarczyk, M.: Hereditary history preserving bisimulation or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdańsk (1991)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming 75(1), 3–51 (2008)
Blanchet, B., Podelski, A.: Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science 333(1–2), 67–90 (2005). Special issue FoSSaCS 2003
Chréetien, R., Cortier, V., Delaune, S.: Typing messages for free in security protocols: the case of equivalence properties. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 372–386. Springer, Heidelberg (2014)
Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), Edinburgh, Scotland, UK, pp. 322–336. IEEE Computer Society Press, Edinburgh, July 2010
Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
Cremers, C.: Key exchange in ipsec revisited: formal analysis of IKEv1 and IKEv2. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 315–334. Springer, Heidelberg (2011)
Darondeau, P., Degano, P.: Causal trees. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) ICALP 1989. LNCS, vol. 372, pp. 234–348. Springer, Heidelberg (1989)
ETSI. TS 102 731 V1.1.1: ITS; security; security services and architecture, 09 2010
ETSI. TS 102 940 V1.1.1: ITS; security; ITS communications security architecture and security management, 06 2012
Fábrega, F.J.T., Herzog, J.C., Guttman, J.D.:. Strand spaces: Why is a security protocol correct? In: Symposium on Security and Privacy. IEEE Computer Society (1998)
Fröschle, S.: Decidability and Coincidence of Equivalences for Concurrency. PhD thesis, University of Edinburgh (2004)
Fröschle, S.: Composition and decomposition in true-concurrency. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 333–347. Springer, Heidelberg (2005)
Fröschle, S.: The decidability border of hereditary history preserving bisimilarity. Information Processing Letters 93(6), 289–293 (2005)
Fröschle, S.: The insecurity problem: tackling unbounded data. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 370–384 (2007)
Fröschle, S.: Causality in Security Protocols and Security APIs: Foundations and Practical Verification, Habilitation thesis, Universität Oldenburg (2012)
Fröschle, S.: Leakiness is decidable for well-founded protocols. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 176–195. Springer, Heidelberg (2015)
Fröschle, S., Jančar, P., Lasota, S., Sawa, Z.: Non-interleaving bisimulation equivalences on basic parallel processes. Information and Computation 208(1), 42–62 (2010)
Fröschle, S., Lasota, S.: Decomposition and complexity of hereditary history preserving bisimulation on BPP. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 263–277. Springer, Heidelberg (2005)
Fröschle, S., Lasota, S.: Normed processes, unique decomposition, and complexity of bisimulation equivalences. In: Proceedings of INFINITY 2006-2009, vol. 239, pp. 17–42. Elsevier (2009)
Fröschle, S., Sommer, N.: Reasoning with past to prove PKCS#11 keys secure. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 96–110. Springer, Heidelberg (2011)
Hack, M.: The equality problem for vector addition systems is undecidable. Theoret. Comput. Sci. 2(1), 77–95 (1976)
Hirshfeld, Y.: Petri nets and the equivalence problem. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol. 832, pp. 165–174. Springer, Heidelberg (1994)
Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. Mathematical Structures in Computer Science 6, 251–259 (1996)
Hirshfeld, Y., Jerrum, M.: Bisimulation equivalence is decidable for normed process algebra (Extended abstract). In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 412–421. Springer, Heidelberg (1999)
Jančar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science 148(2), 281–301 (1995). STACS 1994
Jančar, P.: Bisimilarity of basic parallel processes is PSPACE-complete. In: Proc. LICS 2003, pp. 218–227. IEEE Computer Society (2003)
Jategaonkar, L., Meyer, A.R.: Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science 154(1), 107–143 (1996)
Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127(2), 164–185 (1996)
Jurdziński, M., Nielsen, M., Srba, J.: Undecidability of domino games and hhp-bisimilarity. Inform. and Comput. 184, 343–368 (2003)
Kamil, A., Lowe, G.: Analysing tls in the strand spaced model. Journal of Computer Security 19(5), 975–1025 (2011)
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), 43–68 (1990)
Künnemann, R.: Automated backward analysis of PKCS#11 v2.20. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 219–238. Springer, Heidelberg (2015)
Lasota, S.: A polynomial-time algorithm for deciding true concurrency equivalences of basic parallel processes. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 521–530. Springer, Heidelberg (2003)
Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security 7(1), 89–146 (1999)
Madhusudan, P., Thiagarajan, P.S.: Controllers for discrete event systems via morphisms. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 18–33. Springer, Heidelberg (1998)
Milner, R. (ed.): A calculus of communicating systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part i. Theor. Comput. Sci. 13, 85–108 (1981)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Ramanujam, R., Suresh, S.P.: A decidable subclass of unbounded security protocols. In: WITS 2003, pp. 11–20 (2003)
Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 363–374. Springer, Heidelberg (2003)
Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. Journal of Computer Security 13(1), 135–165 (2005)
Schmidt, B., Sasse, R., Cremers, C., Basin, D.: Automated verification of group key agreement protocols. In: Proceedings of the 2014 IEEE Symposium on Security and Privacy SP 2014, DC, USA, Washington, pp. 179–194 (2014)
Song, D.X.: Athena: A new efficient automatic checker for security protocol analysis. In: CSFW 1999, pp. 192–202. IEEE Computer Society (1999)
Srba, J.: Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 535–546. Springer, Heidelberg (2002)
Sunesen, K., Nielsen, N.: Behavioural equivalence for infinite systems—partially decidable!. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 460–479. Springer, Heidelberg (1996)
van Glabbeek, R., Goltz, U.: Equivalence notions for concurrent systems and refinement of actions. In: Kreczmar, A., Mirkowska, G. (eds.) MFCS 1989. LNCS, vol. 379, pp. 237–248. Springer, Heidelberg (1989)
Vogler, W.: Deciding history preserving bisimilarity. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 495–505. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Fröschle, S. (2015). Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems. In: Meyer, R., Platzer, A., Wehrheim, H. (eds) Correct System Design. Lecture Notes in Computer Science(), vol 9360. Springer, Cham. https://doi.org/10.1007/978-3-319-23506-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-23506-6_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23505-9
Online ISBN: 978-3-319-23506-6
eBook Packages: Computer ScienceComputer Science (R0)