Abstract
The TreeKEM protocol is the preeminent implementation candidate for the Message Layer Security standard. Prior work analyzed TreeKEM by defining the Continuous Group Key Agreement security game, which facilitated proof of some security guarantees and also identified protocol deficiencies which were subsequently remedied. This work extends such applications by formalizing the Continuous Group Key Agreement security game through multiple soundness preserving abstractions. The model is parameterized by N, representing an unbounded protocol duration among N distinct participants. Once formalized, the game is encoded within Promela and essential security guarantees are verified for \(N \le 16\) via the model checker Spin. This represents a notable achievement, both in practical security terms for the TreeKEM protocol, as well as demonstrating scalability techniques for non-trivial parameter bounds when modeling a complex, concurrent protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Performed on the American Museum of Natural History scientific computing cluster.
References
Alwen, J., Coretti, S., Dodis, Y.: The double ratchet: security notions, proofs, and modularization for the signal protocol. In: Ishai, Y., Rijmen, V. (eds.) EUROCRYPT 2019. LNCS, vol. 11476, pp. 129–158. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17653-2_5
Alwen, J., Coretti, S., Dodis, Y., Tselekounis, Y.: Security analysis and improvements for the IETF MLS standard for group messaging. In: Micciancio, D., Ristenpart, T. (eds.) CRYPTO 2020. LNCS, vol. 12170, pp. 248–277. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-56784-2_9
Bærentzen, J.A.: On left-balancing binary trees. Technical report, Technical University of Denmark, Technical report (2003)
Barnes, R., Beurdouche, B., Robert, R., Millican, J., Omara, E., Cohn-Gordon, K.: The messaging layer security (MLS) protocol. Internet-Draft draft-ietf-mls-protocol-14, Internet Engineering Task Force (2022). https://datatracker.ietf.org/doc/html/draft-ietf-mls-protocol-14, work in Progress
Bhargavan, K., Barnes, R., Rescorla, E.: TreeKEM: asynchronous decentralized key management for large dynamic groups a protocol proposal for messaging layer security (MLS). Research report, Inria Paris (2018). https://hal.inria.fr/hal-02425247
Boyd, C., Gellert, K.: A modern view on forward security. Comput. J. 64(4), 639–652 (2021)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981). https://doi.org/10.1007/bfb0025774
Cohn-Gordon, K., Cremers, C., Garratt, L.: On post-compromise security. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 164–178. IEEE (2016)
Cohn-Gordon, K., Cremers, C., Garratt, L.: On post-compromise security. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 164–178 (2016). https://doi.org/10.1109/CSF.2016.19
Cohn-Gordon, K., Cremers, C., Garratt, L., Millican, J., Milner, K.: On ends-to-ends encryption: asynchronous group messaging with strong security guarantees. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 1802–1819 (2018)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, hardcover edn. (2003)
Jahn, M.A., Porter, B.W., Patel, H., Zillich, A.J., Simon, S.R., Russ, A.L.: Usability assessment of secure messaging for clinical document sharing between health care providers and patients. Appl. Clin. Inform. 9(02), 467–477 (2018)
Omara, B., Rescorla, I., Kwon, D.: The messaging layer security (MLS) architecture. In: Proceedings of Network Working Group. Internet Engineering Task Force (2020)
Omara, E., Beurdouche, B., Rescorla, E., Inguva, S., Kwon, A., Duric, A.: The messaging layer security (MLS) architecture. Internet-Draft draft-ietf-mls-architecture-03, Internet Engineering Task Force (2019). https://datatracker.ietf.org/doc/draft-ietf-mls-architecture/03/. work in Progress
Perlman, R.: An overview of PKI trust models. IEEE Netw. 13(6), 38–43 (1999)
Perrin, T., Marlinspike, M.: Axolotl ratchet, p. 16 (2013). https://github.com/trevp/axolotl/wiki (visited on 2014-11-02)
Perrin, T., Marlinspike, M.: The double ratchet algorithm. GitHub wiki 112 (2016), M. Marlinspike and T. Perrin. The double ratchet algorithm (2016)
Rescorla, E., Korver, B.: RFC3552: Guidelines for Writing RFC Text on Security Considerations (2003)
Rudin, H., West, C., et al.: On limits and possibilities of automated protocol analysis. In: Protocol Specification, Testing, and Verification, VII: Proceedings of the IFIP WG 6.1 Seventh International Conference on Protocol Specification, Testing, and Verification, vol. 7, p. 339. North Holland (1987)
Schröder, S., Huber, M., Wind, D., Rottermanner, C.: When SIGNAL hits the fan: on the usability and security of state-of-the-art secure mobile messaging. In: European Workshop on Usable Security, pp. 1–7. IEEE (2016)
Shirey, R.W.: Internet Security Glossary, Version 2. RFC 4949 (2007). https://doi.org/10.17487/RFC4949. https://www.rfc-editor.org/info/rfc4949
Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. cryptology eprint archive (2004)
Unger, N., et al.: SoK: secure messaging. In: 2015 IEEE Symposium on Security and Privacy, pp. 232–249. IEEE (2015)
Vaziripour, E., et al.: Is that you, alice? A usability study of the authentication ceremony of secure messaging applications. In: Thirteenth Symposium on Usable Privacy and Security (SOUPS 2017), pp. 29–47 (2017)
Washburn, A.J.: Formal Verification Applications for the TreeKEM Continuous Group Key Agreement Protocol. Master’s thesis (2022)
Washburn, A.J., Shankar, S.: SPIN Model of TreeKEM: FSU & PCS (2024). https://doi.org/10.5281/zenodo.13893828
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Washburn, A.J., Shankar, S. (2025). Formal Verification of Forward Secrecy and Post-Compromise Security for TreeKEM. In: C. Nogueira, S., Teodorov, C. (eds) Formal Methods: Foundations and Applications. SBMF 2024. Lecture Notes in Computer Science, vol 15403. Springer, Cham. https://doi.org/10.1007/978-3-031-78116-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-031-78116-2_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-78115-5
Online ISBN: 978-3-031-78116-2
eBook Packages: Computer ScienceComputer Science (R0)