71 lines
8.3 KiB
TeX
71 lines
8.3 KiB
TeX
We describe our approach for the analysis nested ratchet protocol, Megolm, and Sender Keys
|
||
%l, Megolm (as described by Matrix), Sender Keys (as described by Signal, Whatsapp, and Facebook Messenger), as well as the reliant sub-protocols 3DH, X3DH, Signal, and Olm,
|
||
using \textsc{ProVerif}. We also describe the claimed
|
||
security properties for these protocols.
|
||
|
||
\subsection{Modeling Strategy}
|
||
\label{sec:section label}
|
||
|
||
We do not go into the full details of the symbolic approach. One may refer to \cite{Blanchet_2012, Blanchet_2016} for a detailed presentation and comparison with alternative approaches.
|
||
|
||
\textbf{Cryptographic Primitives}. In the symbolic model, messages are represented as terms which can be either atomic (to represent fresh values or constants), or constructed through applying functional rules. For instance, \textsf{pk}(\textit{sk}), \textsf{Mac($key$, $msg$)}, \textsf{Encrypt(k, m)}, and \textsf{Decrypt(k, m)}. To model the behavior of cryptographic primitives, function symbols may be ruled by a set of equations, i.e. an \textit{equational theory}. For example, \textsf{Decrypt(k, Encrypt(k, m)) = m} will hold. Therefore, cryptography is assumed to be perfect in the symbolic model; if no equational rules are defined for a given primitive, it behaves as a perfect one-way function.
|
||
|
||
\textbf{Threat Model}. The Dolev-Yao attacker model is the standard attacker model assumed in symbolic cryptography \cite{Dolev_1983}. The Dolev-Yao attacker has full control over the network, and can observe, remove, duplicate, replay, synthesize, and subtitute messages on public channels. In \pv, the attacker may be configured to never gain access to certain terms (i.e. a private key), or have access to pre-computed values (i.e. precomputing \textsf{DH} to find additional attacker scenarios). \pv is capable of reasoning soundly, but not completely, about arbitrary protocols with respect to a Dolev-Yao attacker. That is, any attack or proof \pv is guaranteed within the model,\footnote{Though, one must look out for false attacks -- that is, where a property is violated by a trivial or unintended attack trace. Alternatively, cases where properties vacuously hold (i.e. because parts of a protocol are not reachable) should similarly be avoided.}
|
||
but \pv is not guaranteed to terminate.\footnote{And indeed, we employ a plethora of tricks and tweaks to ensure our models terminate reasonably quickly. See section \S 6.6.2 ``Settings'' and \S 6.7.5 ``Sources of incompleteness'' in the \pv manual \cite{ProverifManual}}
|
||
|
||
\textbf{Trace and Equivalence}. In the symbolic approach there exists two primary classes of security properties: \textit{trace properties} and \textit{equivalence} properties.
|
||
Trace properties are considered to be satisfied when, in all possible
|
||
traces or executions of the protocol, the property holds. Several security properties are expressable as trace properties. \textit{secrecy} is specified as a reachability property, i.e. whether an attacker can \textit{reach} a given secret term, such as a message. \textit{authentication} is specified as correspondance between two events; that is, if an event is reachable, another event is previously reachable. \textit{perfect forward securiy} and \textit{post-compromise security} relate secrecy queries with event timings, e.g. if a message can be compromised by the time an event occurs. On the other hand, equivalence properties decide if an attacker can \textit{tell apart} two processes; e.g. privacy properties such as deniability and unlinkability can be expressed as equivalence properties. In this work, we employ both trace and equivalence properties.
|
||
|
||
% Things to mention:
|
||
% - threat model
|
||
% - cryptographic primitives, how they're modeled
|
||
% - security and authentication
|
||
% - equivalence properties \& deniability
|
||
% - evaluation strategy
|
||
|
||
% claimed security properties
|
||
% - authentication of sessions, authentication of msgs sent with megolm
|
||
% - secrecy of sessions, secrecy of messages; resistant against unknown keyshare attacks
|
||
% - deniability
|
||
% - forward secrecy and post compromise security
|
||
|
||
\subsection{Claimed Security Properties}
|
||
\label{sec:section label}
|
||
|
||
We provide informal definitions for each property we claim the nested ratchet protocol to hold.
|
||
|
||
\attackerbox{\underline{\textbf{P1}}: Protocol participants are \textbf{Deadlock-Free}.} We claim an arbitrary number of peers who participate in the nested ratchet protocol \textit{do not deadlock} and complete the protocol, even in the presence of an attacker.
|
||
|
||
\attackerbox{\underline{\textbf{P2}}: Honest peers enjoy \textbf{Message Secrecy}.}
|
||
We claim only group members who hold the correct fan-out ratchet state can decrypt ciphertexts encrypted by honest peers, ruling out outsider eavesdropping and cross-group leakage.
|
||
|
||
\attackerbox{\underline{\textbf{P3}}: Honest protocol participants enjoy \textbf{Mutual Authentication} \& \textbf{Message Agreement.}.}
|
||
We claim that every plaintext accepted by an honest recipient is \textit{jointly authenticated}: if Alice outputs a message labelled as originating from Bob, then Bob must have previously emitted that exact message under the same epoch key. This guarantees resistance to replay, impersonation, and \textit{unknown-key-share} attacks.
|
||
|
||
\attackerbox{\underline{\textbf{P4}}: Honest peers enjoy \textbf{Offline Deniability}.}
|
||
|
||
We follow the form of \cite{Celi_Hoyland_Stebila_Wiggers_2022, Lafourcade_Mahmoud_Ruhault_Taleb} and claim it is impossible for an offline judge (that is, a judge that does not interfere with the protocol execution) to distinguish between a transcript generated between an honest initiator, and a transcript generated by a simulator.\footnote{No single approach to defining and demonstrating deniability guarantees has distinguished itself in the literature; see a classification here} On the other hand, it is well-known that responder deniability in authenticated key exchange, namely signal, is not ensured in the offline judge model. Thus, we also consider responder \textit{undeniability}.
|
||
|
||
%We claim that for the initiator of each Double Ratchet channel, message authorship cannot be proven to a coercer and deniability is retained. On the other hand, it is well-known that responder deniability in authenticated key exchange, namely Signal, is not ensured. Thus, we also claim all keys in the initial key exchange must remain unsigned by long-term static keys to ensure mutual deniability.
|
||
% https://eprint.iacr.org/2022/1111.pdf
|
||
|
||
\attackerbox{\underline{\textbf{P5}}: Messages sent by honest peers enjoy \textbf{Perfect Forward Secrecy}.}
|
||
We claim that the compromise of any static credential, including the identity keys and the medium-term pre-keys of the double ratchet channel, and the present fan-out ratchet key, does not reveal any earlier traffic from either the current session or any previous sessions.
|
||
|
||
\attackerbox{\underline{\textbf{P6}}: Between sessions, messages sent by honest peers enjoy \textbf{Post-Compromise Security}.}
|
||
We claim that once a compromised party executes a fresh \textsc{SessionGen} followed by \textsc{SessionShare}, full secrecy and authentication guaratnees are re-established for the subsequent traffic.
|
||
%The attacker’s influence is thus confined to the interval between the breach and the next honest ratchet refresh, matching the recovery guarantees of Signal.
|
||
|
||
\subsection{Additional Security Properties}
|
||
We additionally define exceptionally strong properties we do not expect to hold in composition with the aforementioned properties, but are desirable and relevant nonetheless.
|
||
|
||
\badpropbox{\underline{\textbf{P7}}: In the post-compromise and forward secrecy scenarios, deniability is maintained (i.e. \textbf{Strong Deniability} \cite{Unger_Goldberg_2018}). }
|
||
% https://cypherpunks.ca/~iang/pubs/dakez-popets18.pdf
|
||
Given the compromise of static or ephemeral credentials, ideally deniability of message authorship, both previous and future, is maintained.
|
||
|
||
\badpropbox{\underline{\textbf{P8}}: Deniability is maintained for all protocol participants (i.e. \textbf{Mutual Offline Deniability})}
|
||
%https://eprint.iacr.org/2021/642.pdf (or the thesis, https://academicworks.cuny.edu/cgi/viewcontent.cgi?article=6191&context=gc_etds)
|
||
%https://petsymposium.org/popets/2025/popets-2025-0018.pdf
|
||
It is well-known that responder deniability in mutually authenticated key exchange, namely Signal, is not ensured within the offline judge model \cite{VatandasDeny, Collins_Colombo_Huguenin-Dumittan_2025}.
|