\relax 
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\citation{rfc8446}
\citation{rfc9369}
\citation{Donenfeld_2017}
\citation{openvpn}
\citation{Dingledine_Mathewson_Syverson_2004}
\citation{Marlinspike_Perrin_X3DH}
\citation{Moxie_DoubleRatchet}
\citation{Moxie_Sesame}
\citation{Kret_Schmidt_PQXDH}
\citation{Bhargavan_PQXDH,cremers_signal,alwen_doubleratchet,VatandasDeny,bhargavan_dy}
\citation{rfc9420}
\citation{Wallez_TreeSync,Wallez_TreeKEM}
\citation{WhatsAppSecurity2024}
\citation{MetaMessengerE2EE2023}
\citation{SignalSenderKeysRust}
\citation{Jefferys2020SessionProtocol}
\citation{Albrecht_Dowling_Jones}
\@LN@col{1}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{section.1}\protected@file@percent }
\@LN@col{2}
\citation{Balbas_SK}
\citation{Albrecht_Dowling_Jones}
\citation{matrixorg_megolm_doc}
\citation{VatandasDeny,FiedlerPQXDHdeny}
\citation{SoK_CAC}
\citation{Balbas_SK,Albrecht_Dowling_Jones}
\citation{Blanchet_2016}
\citation{Balbas_SK}
\citation{Albrecht_Dowling_Jones}
\citation{Albrecht_2025}
\@LN@col{1}
\@LN@col{2}
\citation{Balbas_SK}
\citation{Albrecht_Dowling_Jones}
\citation{Albrecht_2025}
\citation{Blanchet_2012}
\citation{Kobeissi_Bhargavan_Blanchet_2017,Bhargavan_PQXDH}
\citation{rfc9420}
\citation{Alwen_Coretti_Jost_Mularczyk_2020}
\citation{rfc9420}
\citation{Wallez_TreeKEM}
\citation{Wallez_TreeSync}
\citation{VatandasDeny}
\citation{VatandasDeny}
\citation{Celi_Hoyland_Stebila_Wiggers_2022}
\citation{Lafourcade_Mahmoud_Ruhault_Taleb}
\citation{Basin_Cremers_Dreier_Sasse_2022}
\citation{ProverifManual}
\citation{Lafourcade_Mahmoud_Ruhault_Taleb}
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Overview of related works that study nested ratchet protocols, including Megolm (underpinning Matrix) and Sender Keys (underpinning WhatsApp). We include a comparison with our own work.}}{3}{table.caption.1}\protected@file@percent }
\providecommand*\caption@xref[2]{\@setref\relax\@undefined{#1}}
\newlabel{tab:symbolic-tools}{{1}{3}{Overview of related works that study nested ratchet protocols, including Megolm (underpinning Matrix) and Sender Keys (underpinning WhatsApp). We include a comparison with our own work}{table.caption.1}{}}
\@LN@col{1}
\@writefile{toc}{\contentsline {section}{\numberline {2}Related Works}{3}{section.2}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Computational Analysis}{3}{subsection.2.1}\protected@file@percent }
\newlabel{sec:section label}{{2.1}{3}{Computational Analysis}{subsection.2.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Messaging Layer Security}{3}{subsection.2.2}\protected@file@percent }
\newlabel{sec:section label}{{2.2}{3}{Messaging Layer Security}{subsection.2.2}{}}
\@LN@col{2}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Mechanized Deniability}{3}{subsection.2.3}\protected@file@percent }
\newlabel{sec:section label}{{2.3}{3}{Mechanized Deniability}{subsection.2.3}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}The Nested Ratchet Protocol}{3}{section.3}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Cryptographic Building Blocks}{3}{subsection.3.1}\protected@file@percent }
\newlabel{sec:section label}{{3.1}{3}{Cryptographic Building Blocks}{subsection.3.1}{}}
\citation{rfc5869}
\citation{auth}
\citation{matrixorg_olm_repo}
\citation{Marlinspike_Perrin_X3DH}
\citation{Kret_Schmidt_PQXDH}
\citation{Moxie_DoubleRatchet}
\@LN@col{1}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Handshakes}{4}{subsection.3.2}\protected@file@percent }
\newlabel{sec:section label}{{3.2}{4}{Handshakes}{subsection.3.2}{}}
\@LN@col{2}
\@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Notation for employed Cryptographic primitives.}}{4}{table.caption.2}\protected@file@percent }
\newlabel{tab:symbols}{{2}{4}{Notation for employed Cryptographic primitives}{table.caption.2}{}}
\@LN@col{1}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces An example workflow of asynchronous authenticated key exchange. Bob, the responder, uploads his pre-key material ({\footnotesize  \textsf  {spk\textsubscript  {B}, sig\_pk\textsubscript  {B}, pk\textsubscript  {B}}}) to the server. Alice, the initiator, fetches Bob's key material from the central server at her leasure, and initiates the authenticated key exchange and \textsf  {DH} key agreement}}{5}{figure.caption.3}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Signal, Olm, and the Double Ratchet}{5}{subsection.3.3}\protected@file@percent }
\newlabel{sec:section label}{{3.3}{5}{Signal, Olm, and the Double Ratchet}{subsection.3.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Session Sharing \& Server-Side Fan-Out}{5}{subsection.3.4}\protected@file@percent }
\newlabel{sec:section label}{{3.4}{5}{Session Sharing \& Server-Side Fan-Out}{subsection.3.4}{}}
\@LN@col{2}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Nested Ratchet Protocol Definition}{5}{subsection.3.5}\protected@file@percent }
\newlabel{sec:section label}{{3.5}{5}{Nested Ratchet Protocol Definition}{subsection.3.5}{}}
\citation{Chase_Perrin_Zaverucha_2020}
\citation{SignalSenderKeysRust}
\citation{WhatsAppSecurity2024}
\citation{matrixorg_megolm_doc}
\citation{MetaMessengerE2EE2023}
\citation{Jefferys2020SessionProtocol}
\citation{Chase_Perrin_Zaverucha_2020}
\citation{Balbas_SK}
\citation{mcmillion2025keytransparencyarchitecture}
\citation{matrixorg_megolm_doc}
\citation{Blanchet_2012,Blanchet_2016}
\citation{Dolev_1983}
\citation{ProverifManual}
\@LN@col{1}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces An example workflow of session transmission from Alice to Bob. Alice transmits her session information, including her session's symmetric key {\footnotesize  \textsf  {symkey\textsubscript  {A0}}} and public signing key {\footnotesize  \textsf  {pk\textsubscript  {A}}}. Alice generates a new message {\footnotesize  \textsf  {m1}}, hashes her session's symmetric key and uses it to encrypt {\footnotesize  \textsf  {m1}}, signs the ciphertext with {\footnotesize  \textsf  {sk\textsubscript  {A}}}, then sends the ciphertext and signature to the server for server-side fan-out. The recipient, Bob, checks the signature, hashes his copy of the symmetric key, and decrypts. }}{6}{figure.caption.4}\protected@file@percent }
\@LN@col{2}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.6}Real World Instantiations of the Nested Ratchet Protocol}{6}{subsection.3.6}\protected@file@percent }
\newlabel{sec:section label}{{3.6}{6}{Real World Instantiations of the Nested Ratchet Protocol}{subsection.3.6}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Formal Modeling}{6}{section.4}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Modeling Strategy}{6}{subsection.4.1}\protected@file@percent }
\newlabel{sec:section label}{{4.1}{6}{Modeling Strategy}{subsection.4.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces  An example instantiation of the nested ratchet protocol using 3DH as the pairwise ratcheting channel. In this example, Alice, the initiator, asynchronously establishes a shared secret with Bob, the responder, via 3DH. Alice then transmits her fan-out layer session, including her ratchet key \textsf  {symkey\textsubscript  {A0}} and session public key \textsf  {ssk\_pk\textsubscript  {A}}, using the established secure 3DH channel. Alice follows this by sending Bob her first message, encrypted and signed using her session, and fanned out by the server to all receivers, including Bob. We note the above handshake may be equivalently condensed into just a 3-way handshake; however, for the sake of example, we make explicit the transmission of the 3DH material, session material, and message material. Specified notation for cryptographic primitives, as well as their respective descriptions, are elaborated upon in Table \ref {tab:symbols}. }}{7}{figure.caption.5}\protected@file@percent }
\newlabel{fig:megolm}{{3}{7}{An example instantiation of the nested ratchet protocol using 3DH as the pairwise ratcheting channel. In this example, Alice, the initiator, asynchronously establishes a shared secret with Bob, the responder, via 3DH. Alice then transmits her fan-out layer session, including her ratchet key \textsf {symkey\ts {A0}} and session public key \textsf {ssk\_pk\ts {A}}, using the established secure 3DH channel. Alice follows this by sending Bob her first message, encrypted and signed using her session, and fanned out by the server to all receivers, including Bob. We note the above handshake may be equivalently condensed into just a 3-way handshake; however, for the sake of example, we make explicit the transmission of the 3DH material, session material, and message material. Specified notation for cryptographic primitives, as well as their respective descriptions, are elaborated upon in Table \ref {tab:symbols}}{figure.caption.5}{}}
\@LN@col{1}
\@LN@col{2}
\citation{Celi_Hoyland_Stebila_Wiggers_2022,Lafourcade_Mahmoud_Ruhault_Taleb}
\@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Comparison of Nested Ratchet Protocol Implementations}}{8}{table.caption.6}\protected@file@percent }
\newlabel{tab:crypto-summary}{{3}{8}{Comparison of Nested Ratchet Protocol Implementations}{table.caption.6}{}}
\@LN@col{1}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Claimed Security Properties}{8}{subsection.4.2}\protected@file@percent }
\newlabel{sec:section label}{{4.2}{8}{Claimed Security Properties}{subsection.4.2}{}}
\@LN@col{2}
\citation{Unger_Goldberg_2018}
\citation{VatandasDeny,Collins_Colombo_Huguenin-Dumittan_2025}
\@LN@col{1}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Additional Security Properties}{9}{subsection.4.3}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Analysis of the Nested Ratchet Protocol}{9}{section.5}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Sub-Protocol Properties}{9}{subsection.5.1}\protected@file@percent }
\newlabel{sec:section label}{{5.1}{9}{Sub-Protocol Properties}{subsection.5.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Symbolic Analysis Results}{9}{subsection.5.2}\protected@file@percent }
\newlabel{sec:section label}{{5.2}{9}{Symbolic Analysis Results}{subsection.5.2}{}}
\@LN@col{2}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Failure Case Analysis}{9}{subsection.5.3}\protected@file@percent }
\newlabel{sec:section label}{{5.3}{9}{Failure Case Analysis}{subsection.5.3}{}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.3.1}Failure Taxonomy}{9}{subsubsection.5.3.1}\protected@file@percent }
\@LN@col{1}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.3.2}Observed Patterns \& Insights}{10}{subsubsection.5.3.2}\protected@file@percent }
\@LN@col{2}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}P2P layer pre-key post-compromise message secrecy vs mutual deniability}{10}{subsection.5.4}\protected@file@percent }
\newlabel{sec:section label}{{5.4}{10}{P2P layer pre-key post-compromise message secrecy vs mutual deniability}{subsection.5.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5}Fan-out layer non-repudiation vs deniability}{10}{subsection.5.5}\protected@file@percent }
\newlabel{sec:section label}{{5.5}{10}{Fan-out layer non-repudiation vs deniability}{subsection.5.5}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Discussion}{10}{section.6}\protected@file@percent }
\citation{Itkis_Reyzin_2001}
\citation{DY}
\citation{Gancher_2023}
\citation{Kret_Schmidt_PQXDH}
\citation{pqwg}
\citation{rfc9180}
\citation{Schwabe_Stebila_Wiggers_2020}
\citation{Lafourcade_Mahmoud_Ruhault_Taleb,Bhargavan_PQXDH}
\citation{Celi_Hoyland_Stebila_Wiggers_2022}
\citation{mcMillion2025keytrans}
\@LN@col{1}
\@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Security property preservation under compromise scenarios. {\fontfamily  {pzd}\fontencoding  {U}\fontseries  {m}\fontshape  {n}\selectfont  \char 51} = property maintained, {\fontfamily  {pzd}\fontencoding  {U}\fontseries  {m}\fontshape  {n}\selectfont  \char 55} = property violated. $^*$Megolm maintains authentication in C3 due to MAC verification, unlike Sender Keys which relies solely on signatures. P2: Message Secrecy, P3: Authentication, P4: Deniability, P5: Perfect Forward Secrecy, P6: Post-Compromise Security, P7: Strong Deniability. ``P1: Reachability'' remains all true for all cases, and ``P2: Mutual Deniability'' remains false for all cases, thus both properties are not included in the table.}}{11}{table.caption.7}\protected@file@percent }
\newlabel{tab:failure-comparison}{{4}{11}{Security property preservation under compromise scenarios. \ding {51} = property maintained, \ding {55} = property violated. $^*$Megolm maintains authentication in C3 due to MAC verification, unlike Sender Keys which relies solely on signatures. P2: Message Secrecy, P3: Authentication, P4: Deniability, P5: Perfect Forward Secrecy, P6: Post-Compromise Security, P7: Strong Deniability. ``P1: Reachability'' remains all true for all cases, and ``P2: Mutual Deniability'' remains false for all cases, thus both properties are not included in the table}{table.caption.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Recommendations for protocol implementers}{11}{subsection.6.1}\protected@file@percent }
\newlabel{sec:recs}{{6.1}{11}{Recommendations for protocol implementers}{subsection.6.1}{}}
\@LN@col{2}
\@writefile{toc}{\contentsline {section}{\numberline {7}Limitations \& Future Work}{11}{section.7}\protected@file@percent }
\citation{Blanchet_2012}
\citation{Blanchet_Jacomme}
\citation{Kobeissi_Bhargavan_Blanchet_2017}
\citation{VatandasDeny}
\citation{Blanchet_Jacomme}
\bibstyle{plain}
\bibdata{refs}
\bibcite{Albrecht_Dowling_Jones}{1}
\bibcite{Albrecht_2025}{2}
\bibcite{alwen_doubleratchet}{3}
\bibcite{Alwen_Coretti_Jost_Mularczyk_2020}{4}
\bibcite{Balbas_SK}{5}
\@LN@col{1}
\@writefile{toc}{\contentsline {section}{\numberline {8}Conclusions}{12}{section.8}\protected@file@percent }
\@LN@col{2}
\@writefile{toc}{\contentsline {section}{\numberline {9}Ethical Considerations}{12}{section.9}\protected@file@percent }
\newlabel{sec:section label}{{9}{12}{Ethical Considerations}{section.9}{}}
\@writefile{toc}{\contentsline {section}{\numberline {10}Open Science}{12}{section.10}\protected@file@percent }
\newlabel{sec:section label}{{10}{12}{Open Science}{section.10}{}}
\bibcite{SoK_CAC}{6}
\bibcite{rfc9420}{7}
\bibcite{rfc9180}{8}
\bibcite{Basin_Cremers_Dreier_Sasse_2022}{9}
\bibcite{bhargavan_dy}{10}
\bibcite{DY}{11}
\bibcite{Bhargavan_PQXDH}{12}
\bibcite{Blanchet_2012}{13}
\bibcite{Blanchet_2016}{14}
\bibcite{Blanchet_Jacomme}{15}
\bibcite{ProverifManual}{16}
\bibcite{Celi_Hoyland_Stebila_Wiggers_2022}{17}
\bibcite{Chase_Perrin_Zaverucha_2020}{18}
\bibcite{cremers_signal}{19}
\bibcite{Collins_Colombo_Huguenin-Dumittan_2025}{20}
\bibcite{auth}{21}
\bibcite{Dingledine_Mathewson_Syverson_2004}{22}
\bibcite{Dolev_1983}{23}
\bibcite{Donenfeld_2017}{24}
\bibcite{rfc9369}{25}
\bibcite{FiedlerPQXDHdeny}{26}
\bibcite{Gancher_2023}{27}
\bibcite{pqwg}{28}
\bibcite{Itkis_Reyzin_2001}{29}
\@LN@col{1}
\@LN@col{2}
\bibcite{Jefferys2020SessionProtocol}{30}
\bibcite{Kobeissi_Bhargavan_Blanchet_2017}{31}
\bibcite{rfc5869}{32}
\bibcite{Kret_Schmidt_PQXDH}{33}
\bibcite{Lafourcade_Mahmoud_Ruhault_Taleb}{34}
\bibcite{Moxie_Sesame}{35}
\bibcite{Marlinspike_Perrin_X3DH}{36}
\bibcite{matrixorg_olm_repo}{37}
\bibcite{matrixorg_megolm_doc}{38}
\bibcite{mcmillion2025keytransparencyarchitecture}{39}
\bibcite{mcMillion2025keytrans}{40}
\bibcite{MetaMessengerE2EE2023}{41}
\bibcite{Moxie_DoubleRatchet}{42}
\bibcite{rfc8446}{43}
\bibcite{Schwabe_Stebila_Wiggers_2020}{44}
\bibcite{SignalSenderKeysRust}{45}
\bibcite{Unger_Goldberg_2018}{46}
\bibcite{VatandasDeny}{47}
\bibcite{Wallez_TreeKEM}{48}
\bibcite{Wallez_TreeSync}{49}
\bibcite{WhatsAppSecurity2024}{50}
\bibcite{openvpn}{51}
\@LN@col{1}
\@LN@col{2}
\gdef \@abspage@last{14}