Formal Analysis of the Nested Ratchet Protocol, and Symbolic Formal Verification of Sender Keys, Signal, Megolm, Olm, 3DH, and X3DH. The main models are written in ProVerif; additional supplementary models (extra from the main results described in the paper) are provided in VerifPal

Environment Setup

1. Install the nix package manager
2. Navigate to the current directory, and run nix develop. You will get dropped into a devshell with the correct versions of ProVerif and VerifPal. Feel free to execute another shell (i.e. zsh) if you have something against bash.

Model Descriptions

• 3dh.pv: a complete model of the Triple Diffie-Hellman handshake. Proving authentication and secrecy.
• x3dh.pv: a complete model of the Extended Triple Diffie-Hellman handshake. Proving authentication and secrecy.
• olm.pv: a complete model of the Olm protocol, as described here. Informally, this is 3DH composed with double ratchet. Secrecy, authentication, reachability, PCS, and PFS are formalized.
• olm-unsigned.pv: the same model as olm.pv, but pre-keys are unsigned. Demonstrates compromise of the pre-key messages.
• signal.pv: a complete model of the Signal protocol. Informally, this is X3DH composed with double ratchet. Secrecy, authentication, reachability, PCS, and PFS are formalized.
• megolm.pv: a composition of Megolm and Olm.
• megolm-olm-unsigned.pv: a composition of Megolm and Olm, where Olm pre-keys are unsigned. Demonstrates the first Megolm session.
• sender-keys.pv: a composition of fan-out layer session sharing and Signal. Includes secrecy, authentication, reachability, PCS, and PFS properties.

The deniability folder includes both initiator deniability and responder undeniability results for 3dh, x3dh, olm, signal, and megolm.

Notes on Proverif reachability

In each model, there exists several queries designed to ensure reachability and no deadlocks. First, each model has an event "start" that is positioned before the PeerA/PeerB processes begin. We simply check query event(start()), which asks ProVerif if it is the case NOT event(start). This query will always return false because in every possible execution of the protocol, event start() is triggered. Thus, broadly, testing reachability involves ensuring query event(event-name()) always resolves to false.

This flavor of query is present in each model and highly necessary, as it ensures other properties are never trivially violated or trivially satisfied.

Notes on optimizations

A common complaint among ProVerif users is optimizing ProVerif code is hard and un-intuitive. The manual isn't very helpful here. Thus, we list out the optimizations and tricks we employ:

• Phases. In ProVerif, phases are synchronization facilities that ensure every peer must stop together at phase n before proceeding to phase n+1. Placing phases right not only allows us to capture perfect forward secrecy and post-compromise security, but allows us to massively cut down on unnecessary intertwinings of operations between peers.
• Channels. Across models we create three channels: c, the channel peers use to communicate; p, a private channel to ensure the distribution of public keys with integrity and authenticity; a, a channel dedicated to publishing material to the attacker.
• Correct checksign and checkmac reduction rules. One fatal flaw in reduction rule design present in the principal ProVerif examples available on the main ProVerif website is that a term reduction of a function reduces to an argument of that function. An example is checksign(sign(m,k), pk(k)) = m (ripped directly from the ProVerif examples). The critical problem here is that, chained with other rewrite rules (i.e. concat(m1,m2) -> m), this can lead to non-termination and many headaches. So, the correct reduction strategy for checksign and checkmac is checksign(pk(sk), m, sign(sk, m)):bool where bool is strictly not a term in the input of the function. We follow in the lead of Deepsec and A Tale of Two Worlds, a Formal Story of WireGuard Hybridization and design our reduction rules for checksign and checkmac like checksign(pk(sk), m, sign(sk, m)) = okay.
• Event orderings. Events denoting sending a message always are activated after the message is sent onto the channel.
• Minimizing rules. We do our absolute best to minimize the number of functions, reduction rules, and equations defined. Our definitions of key derivation and concatonation, and the way we design our models around these functions, are minimized to the best degree possible. Furthermore, the [data] tag is instantiated for each concatonation function, indicating reversibility to ProVerif.
• Strong reduction rules. We generally define Diffie-Hellman as an equational rule, a la equation forall a: skey, b: skey; dh(pk(a), b) = dh(pk(b), a). However, ProVerif hates this, and may cause non-termination. In such cases, we provide more general equational rules that relate the Diffie-Hellman equational operation with other operations in the associated protocol.
• Tagging. Although we do not currently implement tagging in our models, one trick that we employed to speed up analysis for certain test scenarios involves "tagging" each message sent on a channel with a "tag" bitstring marked as private (i.e. free tag_oe1: bitstring [private]). This way, two similarly structured messages on the same channel are not explored in parallel, and only the correct message is processed. Indeed, there some theoretical work proving that tagged protocols always terminate. See section 6.7.2 in the ProVerif manual for more details.
• Options. We tuned the options ProVerif provides in order to ensure each model terminates in a reasonable amount of time. We tuned the selection function primarily. One thing to note is that options never sacrifice completeness. More information on ProVerif settings can be found in the manual, section 6.6.2.