Top

Published in:

2025 | OriginalPaper | Chapter

Formal Verification of Forward Secrecy and Post-Compromise Security for TreeKEM

Authors : Alex J. Washburn, Subash Shankar

Published in: Formal Methods: Foundations and Applications

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm

next chapter Formal Privacy Analyses for Open Banking

Performed on the American Museum of Natural History scientific computing cluster.

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_5CrossRef

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_9CrossRef

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)MathSciNetCrossRef

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)CrossRef

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/bfb0025774CrossRef

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)

10.

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

11.

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)

12.

Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, hardcover edn. (2003)

13.

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)CrossRef

14.

Omara, B., Rescorla, I., Kwon, D.: The messaging layer security (MLS) architecture. In: Proceedings of Network Working Group. Internet Engineering Task Force (2020)

15.

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

16.

Perlman, R.: An overview of PKI trust models. IEEE Netw. 13(6), 38–43 (1999)CrossRef

17.

Perrin, T., Marlinspike, M.: Axolotl ratchet, p. 16 (2013). https://github.com/trevp/axolotl/wiki (visited on 2014-11-02)

18.

Perrin, T., Marlinspike, M.: The double ratchet algorithm. GitHub wiki 112 (2016), M. Marlinspike and T. Perrin. The double ratchet algorithm (2016)

19.

Rescorla, E., Korver, B.: RFC3552: Guidelines for Writing RFC Text on Security Considerations (2003)

20.

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)

21.

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)

22.

Shirey, R.W.: Internet Security Glossary, Version 2. RFC 4949 (2007). https://doi.org/10.17487/RFC4949. https://www.rfc-editor.org/info/rfc4949

23.

Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. cryptology eprint archive (2004)

24.

Unger, N., et al.: SoK: secure messaging. In: 2015 IEEE Symposium on Security and Privacy, pp. 232–249. IEEE (2015)

25.

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)

26.

Washburn, A.J.: Formal Verification Applications for the TreeKEM Continuous Group Key Agreement Protocol. Master’s thesis (2022)

27.

Washburn, A.J., Shankar, S.: SPIN Model of TreeKEM: FSU & PCS (2024). https://doi.org/10.5281/zenodo.13893828

Title: Formal Verification of Forward Secrecy and Post-Compromise Security for TreeKEM
Authors: Alex J. Washburn
Subash Shankar
Publisher: Springer Nature Switzerland
Book: Formal Methods: Foundations and Applications
Print ISBN: 978-3-031-78115-5

Electronic ISBN: 978-3-031-78116-2

Copyright Year: 2025
DOI: https://doi.org/10.1007/978-3-031-78116-2_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"