Advertisement

Stateful Protocol Composition

  • Andreas V. Hess
  • Sebastian A. Mödersheim
  • Achim D. Brucker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11098)

Abstract

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.

Notes

Acknowledgments

This work was supported by the Sapere-Aude project “Composec: Secure Composition of Distributed Systems”, grant 4184-00334B of the Danish Council for Independent Research. We thank Luca Viganò for helpful comments and discussions.

References

  1. 1.
    Almousa, O., Mödersheim, S., Modesti, P., Viganò, L.: Typing and compositionality for security protocols: a generalization to the geometric fragment. In: Pernul, G., Ryan, P.Y.A., Weippl, E. (eds.) ESORICS 2015. LNCS, vol. 9327, pp. 209–229. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-24177-7_11CrossRefGoogle Scholar
  2. 2.
    Andova, S., Cremers, C.J.F., Gjøsteen, K., Mauw, S., Mjølsnes, S.F., Radomirović, S.: A framework for compositional verification of security protocols. Inf. Comput. 206(2–4), 425–459 (2008)MathSciNetCrossRefGoogle Scholar
  3. 3.
    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).  https://doi.org/10.1007/978-3-662-46666-7_17CrossRefGoogle Scholar
  4. 4.
    Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685–1720 (2007)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Butin, D.F.: Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. Ph.D. thesis, Dublin City University, November 2012Google Scholar
  6. 6.
    Cheval, V., Cortier, V., Warinschi, B.: Secure composition of PKIs with public key protocols. In: CSF, pp. 144–158, August 2017.  https://doi.org/10.1109/CSF.2017.28
  7. 7.
    Chevalier, C., Delaune, S., Kremer, S., Ryan, M.D.: Composition of password-based protocols. Formal Methods Syst. Des. 43(3), 369–413 (2013).  https://doi.org/10.1007/s10703-013-0184-6CrossRefzbMATHGoogle Scholar
  8. 8.
    Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322–336. IEEE (2010)Google Scholar
  9. 9.
    Cortier, V., Delaune, S.: Safely composing security protocols. Formal Methods Syst. Des. 34(1), 1–36 (2009).  https://doi.org/10.1007/s10703-008-0059-4CrossRefzbMATHGoogle Scholar
  10. 10.
    Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Sequential protocol composition in Maude-NPA. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 303–318. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15497-3_19CrossRefGoogle Scholar
  11. 11.
    Groß, T., Mödersheim, S.: Vertical protocol composition. In: CSF, pp. 235–250 (2011).  https://doi.org/10.1109/CSF.2011.23
  12. 12.
    Guttman, J.D.: Cryptographic protocol composition via the authentication tests. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 303–317. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00596-1_22CrossRefGoogle Scholar
  13. 13.
    Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: CSFW, pp. 24–34. IEEE (2000)Google Scholar
  14. 14.
    Heintze, N., Tygart, J.D.: A model for secure protocols and their compositions. In: Security and Privacy, pp. 2–13, May 1994.  https://doi.org/10.1109/RISP.1994.296596
  15. 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/
  16. 16.
    Hess, A.V., Mödersheim, S.: Formalizing and proving a typing result for security protocols in Isabelle/HOL. In: CSF (2017)Google Scholar
  17. 17.
    Hess, A.V., Mödersheim, S.: A typing result for stateful protocols. In: CSF (2018)Google Scholar
  18. 18.
    Küsters, R., Tuengerthal, M.: Composition theorems without pre-established session identifiers. In: CCS, pp. 41–50. ACM, New York (2011).  https://doi.org/10.1145/2046707.2046715
  19. 19.
    Mödersheim, S., Viganò, L.: Secure pseudonymous channels. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 337–354. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04444-1_21CrossRefGoogle Scholar
  20. 20.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.DTU ComputeTechnical University of DenmarkLyngbyDenmark
  2. 2.The University of SheffieldSheffieldUK

Personalised recommendations