15 lines
3.9 KiB
TeX
15 lines
3.9 KiB
TeX
We identify the limitations of our work, and discuss the respective potential lines of future work to address the limitations.
|
|
|
|
\noindent\textbf{Abstracted model}. Models in \pv generally abstract away implementation details of cryptographic protocols. Therefore, our models are not executable, and are not drop-in replacements for an already in-place implementation. Our models abstract away details required to actually implement the protocol, including low-level message formatting, key lifetimes, resource constraints, error handling, interfacing with other networking protocols, and caching. Thus, in order to further close the gap between the nested ratchet protocol specification and the real-world implementation, constructing a more detailed model in a more expressive cryptographic modeling tool is necessary. Frameworks such as DY* \cite{DY} and OwlC \cite{Gancher_2023} have shown great promise here, allowing for executable, compilable specifications whilst maintaining semi-automatic cryptanalysis capabilities.
|
|
|
|
\noindent\textbf{No post-quantum analysis}. Protocols supporting post-quantum encryption have increasingly seen real-world deployment in recent years, including PQXDH \cite{Kret_Schmidt_PQXDH}, PQ-Wireguard \cite{pqwg}, HPKE \cite{rfc9180}, and KEMTLS \cite{Schwabe_Stebila_Wiggers_2020}. The rollout of the aforementioned protocols was notably supported by formal methods tooling, most prominently \pv \cite{Lafourcade_Mahmoud_Ruhault_Taleb, Bhargavan_PQXDH} and \textsc{Tamarin} \cite{Celi_Hoyland_Stebila_Wiggers_2022}. In this work we do not support post-quantum primitives. While at the moment only Signal is the only implementor of a nested ratchet protocol that employs a post-quantum-secure P2P layer (using PQXDH), we expect the other implementors of the nested ratchet protocol to follow suit soon.
|
|
|
|
\noindent\textbf{No Key Transparency model}. Key Transparency provides a mechanism to allow communicating parties to verify each other's public identity keys via each party uploading key material to an append-only log on a central server \cite{mcMillion2025keytrans}.
|
|
Key Transparency has seen increasing popularity and deployment, being recently adopted by both Signal\footnote{Although Signal has yet to publicly document their usage of Key Transparency, the implementation is publicly available: \href{https://github.com/signalapp/key-transparency-server}{github.com/signalapp/key-transparency-server}} and Whatsapp.\footnote{WhatsApp is not open source; however, the implementation of the Key Transparency server is open source and available here: \href{https://github.com/facebook/akd}{github.com/facebook/akd}}
|
|
However, it is currently unclear how the incorporation of Key Transparency affects WhatsApp and Signal's existing deniability guarantees. Future work may seek to formalize Key Transparency and its guarantees, then fold the resulting model into existing models of Signal and WhatsApp.
|
|
|
|
\noindent\textbf{No mechanized computational analysis}. Computational reasoning about cryptographic protocols is fundamentally different from the symbolic model. As opposed to modeling cryptographic protocols with equational reasoning and specifying properties in terms of traces, the computational model is closer to hand-written cryptographic proofs in the random oracle model, proving protocols reduce to fundamental computational hardness assumptions through a sequence of computational games. The adversary in the computational model is slightly stronger than in the symbolic model \cite{Blanchet_2012}. Formal methods tooling exists for both the computational model and the symbolic model \cite{Blanchet_Jacomme}; in recent years, analysis of important protocols such as Signal have included mechanized proofs within both models \cite{Kobeissi_Bhargavan_Blanchet_2017} \cite{VatandasDeny}. Thus, future work could involve mechanizing the nested ratchet protocol, Sender Keys, or Megolm inside a computational verifier such as \textsc{CryptoVerif} \cite{Blanchet_Jacomme}
|
|
|
|
|
|
|