Stateful protocol composition. (English) Zbl 1496.68065

Hess, Andreas V.; Mödersheim, Sebastian A.; Brucker, Achim D.

Lopez, Javier (ed.) et al., Computer security. 23rd European symposium on research in computer security, ESORICS 2018, Barcelona, Spain, September 3–7, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 11098, 427-446 (2018).

Summary: We prove a parallel compositionality result for protocols with a shared mutable state, i.e., stateful protocols. For protocols satisfying certain compositionality conditions our result shows that verifying the component protocols in isolation is sufficient to prove security of their composition. Our main contribution is an extension of the compositionality paradigm to stateful protocols where participants maintain shared databases. Because of the generality of our result we also cover many forms of sequential composition as a special case of stateful parallel composition. Moreover, we support declassification of shared secrets. As a final contribution we prove the core of our result in Isabelle/HOL, providing a strong correctness guarantee of our proofs.
For the entire collection see [Zbl 1493.68018].

MSC:

68M25	Computer security
94A60	Cryptography

Software:

Isabelle/HOL

References:

[1]	Almousa, O.; Mödersheim, S.; Modesti, P.; Viganò, L.; Pernul, G.; Ryan, PYA; Weippl, E., Typing and compositionality for security protocols: a generalization to the geometric fragment, Computer Security - ESORICS 2015, 209-229 (2015), Cham: Springer, Cham · Zbl 1499.68043 · doi:10.1007/978-3-319-24177-7_11
[2]	Andova, S.; Cremers, CJF; Gjøsteen, K.; Mauw, S.; Mjølsnes, SF; Radomirović, S., A framework for compositional verification of security protocols, Inf. Comput., 206, 2-4, 425-459 (2008) · Zbl 1147.68389 · doi:10.1016/j.ic.2007.07.002
[3]	Arapinis, M.; Cheval, V.; Delaune, S.; Focardi, R.; Myers, A., Composing security protocols: from confidentiality to privacy, Principles of Security and Trust, 324-343 (2015), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-46666-7_17
[4]	Backes, M.; Pfitzmann, B.; Waidner, M., The reactive simulatability (RSIM) framework for asynchronous systems, Inf. Comput., 205, 12, 1685-1720 (2007) · Zbl 1132.68025 · doi:10.1016/j.ic.2007.05.002
[5]	Butin, D.F.: Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. Ph.D. thesis, Dublin City University, November 2012
[6]	Cheval, V., Cortier, V., Warinschi, B.: Secure composition of PKIs with public key protocols. In: CSF, pp. 144-158, August 2017. doi:10.1109/CSF.2017.28
[7]	Chevalier, C.; Delaune, S.; Kremer, S.; Ryan, MD, Composition of password-based protocols, Formal Methods Syst. Des., 43, 3, 369-413 (2013) · Zbl 1291.68035 · doi:10.1007/s10703-013-0184-6
[8]	Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322-336. IEEE (2010)
[9]	Cortier, V.; Delaune, S., Safely composing security protocols, Formal Methods Syst. Des., 34, 1, 1-36 (2009) · Zbl 1165.68358 · doi:10.1007/s10703-008-0059-4
[10]	Escobar, S.; Meadows, C.; Meseguer, J.; Santiago, S.; Gritzalis, D.; Preneel, B.; Theoharidou, M., Sequential protocol composition in Maude-NPA, Computer Security - ESORICS 2010, 303-318 (2010), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-15497-3_19
[11]	Groß, T., Mödersheim, S.: Vertical protocol composition. In: CSF, pp. 235-250 (2011). doi:10.1109/CSF.2011.23
[12]	Guttman, JD; de Alfaro, L., Cryptographic protocol composition via the authentication tests, Foundations of Software Science and Computational Structures, 303-317 (2009), Heidelberg: Springer, Heidelberg · Zbl 1234.94045 · doi:10.1007/978-3-642-00596-1_22
[13]	Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: CSFW, pp. 24-34. IEEE (2000)
[14]	Heintze, N., Tygart, J.D.: A model for secure protocols and their compositions. In: Security and Privacy, pp. 2-13, May 1994. doi:10.1109/RISP.1994.296596
[15]	Hess, A.V., Mödersheim, S.A., Brucker, A.D.: Stateful protocol composition (extended version). Technical report, DTU Compute (2018). Technical report-2018-03. https://people.compute.dtu.dk/samo/ · Zbl 1496.68065
[16]	Hess, A.V., Mödersheim, S.: Formalizing and proving a typing result for security protocols in Isabelle/HOL. In: CSF (2017)
[17]	Hess, A.V., Mödersheim, S.: A typing result for stateful protocols. In: CSF (2018)
[18]	Küsters, R., Tuengerthal, M.: Composition theorems without pre-established session identifiers. In: CCS, pp. 41-50. ACM, New York (2011). doi:10.1145/2046707.2046715
[19]	Mödersheim, S.; Viganò, L.; Backes, M.; Ning, P., Secure pseudonymous channels, Computer Security - ESORICS 2009, 337-354 (2009), Heidelberg: Springer, Heidelberg · Zbl 1481.94077 · doi:10.1007/978-3-642-04444-1_21
[20]	Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL - A Proof Assistant for Higher-Order Logic (2002), Heidelberg: Springer, Heidelberg · Zbl 0994.68131 · doi:10.1007/3-540-45949-9