\input{diagrams/related}

We briefly review the relevant related works, 
including the previous computational analysis of Megolm and Sender Keys,
the line of work on Messaging Layer Security, and relevant work on 
cryptographic deniability.

\subsection{Computational Analysis}
\label{sec:section label}
The only existing work on Megolm and Sender Keys is computational.
Balbás et al. provided the first formal description and 
analysis of the Sender Keys protocol, as employed by WhatsApp,
within the computational model \cite{Balbas_SK}. 
Albrecht et al. introduced the 
\textit{Device-Oriented Group Messaging}
model to capture the security guarantees of Matrix's Megolm protocol \cite{Albrecht_Dowling_Jones},
and later WhatsApp's Sender Keys protocol in great detail, also within
the computational model \cite{Albrecht_2025}.

We differ from the existing body of work in that our analysis is 
in the \textit{symbolic} model of cryptography as opposed to the random oracle 
``computational'' model. The symbolic and computational modeling approaches are
generally regarding to have complimentary benefits 
\cite{Blanchet_2012}, and cryptographic analysis of 
modern protocols generally involves both approaches 
\cite{Kobeissi_Bhargavan_Blanchet_2017,Bhargavan_PQXDH}. In general,
symbolic analysis allows for simpler mechanization, explicit failure traces,
and greater ease in evaluating attack scenarios. 
We take advantage of these benefits and provide the first 
mechanization of Sender Keys \& Megolm, as well as a 
cryptographic failure case analysis much more detailed than in previous works. 
We also cover the same high-level properties as previous works; We provide 
a complete comparison of the analyzed cryptographic properties
between the related works and our work in Table \ref{tab:symbolic-tools}.


% We differ from the existing body of work in three ways: (1) 
% we \textit{mechanize} our results in a symbolic protocol analysis tool 
% as opposed to hand-written analysis in the random 
% oracle ``computational'' model,
% (2) we provide the first cryptographic \textit{deniability} analysis of 
% Megolm and Sender Keys, and (3) 
% our analysis is unified and general, covering both Megolm and Sender Keys,s
% within our \textit{nested ratchet protocol} primitive. 

\subsection{Messaging Layer Security}
\label{sec:section label}

There exists a long and fruitful line of work studying the Messaging
Layer Security (MLS) protocol standardized by the IETF \cite{rfc9420}, 
and the underlying Continuous Group Key Agreement (CGKA) primitive \cite{Alwen_Coretti_Jost_Mularczyk_2020}. In 
comparison with Sender Keys and Megolm, MLS boasts key updates that are 
logarithmic (as opposed to linear) in the number of members \cite{rfc9420}; however, 
MLS is relatively new and thus much less widely deployed. TreeKEM, the CGKA primitive used by MLS, has enjoyed a string of 
mechanized cryptanalysis work using the symbolic protocol analysis 
framework DY* \cite{Wallez_TreeKEM}. The group management scheme employed by MLS has 
also seen verification using DY* \cite{Wallez_TreeSync}.

\subsection{Mechanized Deniability}
\label{sec:section label}

Cryptographic deniability, particularly of authenticated key exchanges, 
has a long history in the literature. See the related works section of \cite{VatandasDeny}
for additional background. However, relatively few works have considered mechanizing
\textit{offline deniability} guarantees -- that is, 
the ability to deny having participated in a communication session
\textit{after} it has taken place. One technique for proving offline 
deniability with respect to a peer involves proving any execution of a session may be 
\textit{simulated} with only access to the aforementioned peer's public key material \cite{VatandasDeny}.
In recent years there has
surfaced a technique for mechanizing offline deniability through the 
\textit{observational equivalence} feature of symbolic cryptographic provers. 
This technique has been employed to reason about the deniability of 
KEMTLS \cite{Celi_Hoyland_Stebila_Wiggers_2022} and Wireguard \cite{Lafourcade_Mahmoud_Ruhault_Taleb} using \textsc{Tamarin} \cite{Basin_Cremers_Dreier_Sasse_2022} and \textsc{ProVerif} \cite{ProverifManual} respectively. We employ this technique to provide the first comprehensive, mechanized deniability analysis of Sender Key and Megolm. Furthermore, we evaluate deniability across different compromise scenarios, as is done in \cite{Lafourcade_Mahmoud_Ruhault_Taleb}.