Stateful Protocol Composition

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


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.



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.


  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). 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). 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.
  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). 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). 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). Scholar
  11. 11.
    Groß, T., Mödersheim, S.: Vertical protocol composition. In: CSF, pp. 235–250 (2011).
  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). 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.
  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.
  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).
  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). 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). 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