Issues in SimpleX protocol discovered via analysis with Verifpal

[nadimkobeissi]

Hi @epoberezkin, I hope you're doing well! 😄

I'm happy to report that I was able to discover and confirm three findings in SimpleX through protocol analysis with Verifpal. Here is my report.

Scope

This analysis covers simplexmq at commit 27a37387be98d9c7ec0e62373e125539675d0095, tagged 7.0.1.0. All Verifpal models and analysis reports in PDF format are available at this accompanying GitHub repository..

---

Finding 1: Ratchet renegotiation relies only on a static per-queue key

Verifpal protocol analysis report (PDF)

Summary

A double ratchet should recover after a device compromise by replacing old keys. However, SimpleX also uses a per-queue key that is created once and remains unchanged for the life of the queue. That key alone protects the message that tells the agent to discard and rebuild its ratchet.

An attacker who obtains the per-queue key, for example from a stolen backup or a compromised device, can later send a forged renegotiation with attacker-chosen key material. The agent accepts it without user approval and replaces the ratchet. The attacker can repeat this reset, preventing post-compromise recovery.

What the specification says

The agent protocol defines four client-message envelope types, and states that all four are protected by one key:

These messages are encrypted with per-queue shared secret using NaCL crypto_box and can be of 4 types — protocol/agent-protocol.md:169

One of those four is the renegotiation envelope:

agentRatchetKey = agentVersion %s"R" rcvE2EEncryptionParams ratchetKeyInfo — protocol/agent-protocol.md:190

Renegotiation was introduced as agent protocol v3, "ratchet sync - supports re-negotiating double ratchet encryption" (protocol/agent-protocol.md:52).

The parties agree the per-queue secret once, when they create the queue. It is derived from the recipient's key in the queue URI and the sender's key in the confirmation. It is neither ratcheted nor rotated during that queue's lifetime.

Two published claims rely on the double ratchet remaining secure when this key is exposed. A destination router:

cannot: compromise end-to-end encryption even with full access to the per-queue NaCl DH secret. — protocol/agent-protocol.md:702

An attacker holding a client's decrypted database:

cannot: decrypt future messages once the client application resumes communication and the double ratchet completes a new ratchet step, provided PQDR is active. — protocol/agent-protocol.md:711

protocol/security.md:115 also states that an SMP router cannot "compromise the users' end-to-end encryption with an active attack".

What the implementation does

A received SMP client message is decrypted with the per-queue secret, then dispatched by envelope type:

• src/Simplex/Messaging/Agent.hs:3195 — decryptClientMessage e2eDh clientMsg
• src/Simplex/Messaging/Agent.hs:3382 — decryptClientMessage is defined as agentCbDecrypt e2eDh cmNonce cmEncBody. The per-queue Diffie-Hellman secret is therefore the envelope's only authenticator.
• src/Simplex/Messaging/Agent.hs:3198 — the AgentRatchetKey case calls newRatchetKey directly.

newRatchetKey (src/Simplex/Messaging/Agent.hs:3638) then:

• :3649 and :3651 guard against replay with ratchetExists, a SHA-256 hash of the two offered public keys. A fresh attacker key pair passes this check.
• :3657 takes the sendReplyKey branch in the normal RSOk state.
• :3669 and :3672 generate fresh X3DH parameters and enqueue them for the peer.
• :3693 runs pqX3dhRcv or pqX3dhSnd against the parameters that just arrived.
• :3686 deletes the existing ratchet and installs the new one through recreateRatchet.

The envelope has no ratchet-level authentication, and this code path requires no user confirmation.

Two details increase the impact.

First, the renegotiated key agreement uses Diffie-Hellman only. sendReplyKey calls generateRcvE2EParams (src/Simplex/Messaging/Crypto/Ratchet.hs:446), which proposes a KEM key without a ciphertext. When both sides have only proposed, pqX3dhSnd returns Nothing for the KEM component (Ratchet.hs:485); pqX3dhRcv has the mirror case at Ratchet.hs:490. The new root key therefore has no post-quantum secret. The KEM enters at the next ratchet step.

Second, initRatchet chooses which side initializes the sending ratchet by comparing the SHA-256 hashes of the two offered key pairs. By choosing its own keys, the attacker can also choose the victim's role.

The model compresses one implementation step. notifyAgreed (src/Simplex/Messaging/Agent.hs:3679) leaves the connection in RSAgreed. Because ratchetSyncSendProhibited (src/Simplex/Messaging/Agent/Store.hs:478) covers that state, the victim cannot send yet. After a message decrypts under the new ratchet, resetRatchetSync (src/Simplex/Messaging/Agent.hs:3239) returns the connection to RSOk.

The attacker must therefore send the first message under the new ratchet. It can do so because it chose its own parameters and receives the victim's parameters in the reply. The agent also emits an RSYNC event in RSAgreed, so the event is visible through the agent API. This review did not check whether a simplex-chat client displays or gates on that event.

The Verifpal model

Verifpal protocol analysis report (PDF)

examples/messaging/simplex_ratchet_sync.vp returns c0c0c1a1 with both one and two sessions.

The model establishes a connection with the full post-quantum X3DH exchange. It guards Bob's confirmation, so setup is assumed to be secure. Phase one leaks only Alice's per-queue key, ek. It leaks no ratchet state, X3DH key, or KEM key.

query	verdict	what it establishes
confidentiality? m1	holds	Bob's message on the original ratchet is safe
confidentiality? m2	holds	a message sent after the leak, on the original ratchet, is still safe
confidentiality? m3	fails	the message after the forged renegotiation is not
authentication? Bob -> Alice: rkey	fails	Alice acts on a renegotiation Bob never sent

The second query isolates the cause of the third result. The leaked per-queue key alone does not expose a message on the original ratchet. m3 becomes readable only after renegotiation.

Consequence

An attacker who obtains the per-queue secret can prevent post-compromise recovery. Possible sources include a stolen backup, a compromised device, and the confirmation race documented and accepted by the specification. The attack breaks no cryptographic primitive; it replaces the ratchet through a supported code path.

Queue rotation does refresh the secret, but it does not repair an earlier ratchet reset. qAddMsg creates a fresh sender Diffie-Hellman key, and qKeyMsg derives a fresh per-queue secret. Both messages travel inside the ratchet, so an attacker with only the old secret cannot forge them. If the attacker resets the ratchet first, however, it also controls those messages. Rotation helps only if it occurs before the attacker uses the old secret.

Suggested remedy

Before recreateRatchet runs, require either confirmation through the existing ratchet or explicit user approval. Possession of the per-queue secret must not be sufficient.

How to confirm

In a simplexmq test, inject an AgentRatchetKey envelope sealed with a captured per-queue secret into an established duplex connection. Follow it with a message under the resulting ratchet. Check that the victim decrypts the message and then sends under the same ratchet.

---

Finding 2: The proxy-to-router layer uses unauthenticated Diffie-Hellman

Verifpal protocol analysis report (PDF)

Summary

A SimpleX client can send through a chosen proxy so the destination router does not learn the client's address. Traffic from that proxy to the destination router has an extra encryption layer intended to prevent ciphertext correlation.

The destination router does not authenticate the proxy's key when establishing this layer. An active attacker on that hop can complete the handshake as the proxy, remove the extra layer, and read and replay its contents.

What the specification says

The layer and its purpose:

Proxy additionally encrypts the body to prevent correlation by ciphertext (in case TLS is compromised) and forwards it to the destination router in RFWD command. — protocol/simplex-messaging.md:1065

p2r - additional encryption between proxy and SMP router with the shared secret agreed in the handshake, to mitigate traffic correlation inside TLS. — protocol/simplex-messaging.md:1073

The handshake is asymmetric. The router's key is signed by its certificate:

signedRouterKey = originalLength x509encoded ; X25519 key signed by router certificate — protocol/simplex-messaging.md:1632

The proxy's key is unsigned:

clientHello = smpVersion keyHash [clientKey] proxyRouter optClientService ignoredPart — protocol/simplex-messaging.md:1635

clientKey is used only by SMP proxy router when it connects to the destination router to agree shared secret for the additional encryption layer — protocol/simplex-messaging.md:1656

What the implementation does

• src/Simplex/Messaging/Transport.hs:562 defines SMPClientHandshake. Its authPubKey :: Maybe C.PublicKeyX25519 field (:568) has no signature. A certificate can appear only in the optional clientService field.
• src/Simplex/Messaging/Transport.hs:603 confirms that the key is encoded without a signature.
• src/Simplex/Messaging/Transport.hs:777 accepts the client key and uses it to build the server handle.
• src/Simplex/Messaging/Transport.hs:857 and :873 derive the proxy-layer session secret by applying C.dh' to the two handshake keys.

The destination router therefore agrees this secret with an unauthenticated party. That is normal for a channel that relies on TLS, but it limits a layer described as protection when TLS is compromised.

The Verifpal model

Verifpal protocol analysis report (PDF)

examples/messaging/simplex_proxy.vp returns c0a0a1 with both one and two sessions.

query	verdict	what it establishes
confidentiality? mbody	holds	the message body stays hidden from the proxy
authentication? Proxy -> Client: gssk	holds	certificate pinning against MITM-by-proxy works
authentication? Proxy -> Router: rfwd	fails	the router accepts a forwarded transmission the proxy did not send

In the trace, the attacker substitutes the proxy's handshake key and derives the shared secret from the router's signed public key. It then unwraps the forwarded block, obtains the correlation identifier, the client's per-command key, and the encrypted transmission, and rewraps them in a block that the router accepts.

Consequence and limits

This attack requires an active man-in-the-middle on the proxy-to-router hop. The attacker obtains the secret by completing the handshake as the proxy. This is stronger than the observing adversary considered at protocol/security.md:83, which says correlation gains no efficiency "even in case of a compromised transport protocol". The finding does not refute that claim.

The narrower result is that a layer described as protection "in case TLS is compromised" offers no protection against an active attacker on that hop. Command and destination-queue confidentiality still hold because the client-to-router layer above it authenticates the router through its certificate.

protocol/security.md:133 already states that a proxy can "replay messages to a destination router within a single session". This finding extends that ability to an active attacker on the hop.

Suggested remedy

Sign the proxy's handshake key, or require the service certificate introduced through optClientService in v16. The router should derive the secret only with an authenticated party.

How to confirm

Run a proxy and destination router, substitute the proxy's authPubKey during the handshake, and test whether the forwarded blocks can be decrypted and reinjected.

---

Finding 3: Short-link user data has no rollback protection

Verifpal protocol analysis report (PDF)

Summary

A SimpleX short link contains fixed data and editable user data. The fixed data, which includes the address and keys, is bound to a hash in the link. Changing it breaks that commitment.

The editable data contains the profile and, for a group, the owners authorized to update the link. It is signed but has no version or timestamp. Every signed version therefore remains valid, with no way to distinguish the current version from an older one.

What the specification says

The link commits to the fixed data by hash. Both the link identifier and encryption key derive from that hash:

linkKey = SHA3-256(fixedLinkData) — protocol/agent-protocol.md:441

(linkId, encryptionKey) = HKDF(info="SimpleXContactLink", key=linkKey, outputLen=56) — protocol/agent-protocol.md:453

The signed structure adds no freshness field:

signedUserData = signature userData — protocol/agent-protocol.md:473

It includes the authorization list:

userContactData = direct ownersList relaysList userLinkData — protocol/agent-protocol.md:489

The protocol allows this data to be overwritten:

LSET - Set or update the link data associated with a queue. This is used when creating a short link or updating the user data (e.g., profile changes). — protocol/agent-protocol.md:553

The signed user data contains no version, counter, or timestamp.

What the implementation does

In src/Simplex/Messaging/Crypto/ShortLink.hs:

• :47: contactShortLinkKdf derives the link identifier and secret_box key from the link key.
• :61: encodeSignFixedData returns the SHA3-256 hash of the fixed data as the link key.
• :66: encodeSignUserData signs only the user data.
• :100: decryptLinkData performs three checks:
  • :108: the fixed data must hash to the link key.
  • :109: the fixed-data signature must verify under the root key.
  • :106 and :113: the user-data signature must verify under either the root key or an owner key accepted by validateLinkOwners.

None checks freshness. Any user-data blob that an owner signed continues to satisfy the signature check.

An honest server stores only the current blob (src/Simplex/Messaging/Server/QueueStore.hs:43, queueData :: Maybe (LinkId, QueueLinkData)). Exploitation therefore requires control over the LGET response, such as a malicious or compromised router allowed by the threat model, or an active network attacker.

The Verifpal model

Verifpal protocol analysis report (PDF)

examples/messaging/simplex_shortlink.vp returns a1e0e1 with both one and two sessions.

The model first publishes user data with two authorized owners. It then publishes a second version with one owner removed, representing revocation.

query	verdict	what it establishes
authentication? Router -> Joiner: sig_ud2	fails	the joiner verifies a signature the router did not send in this exchange
equivalence? connreq, connreq_j	holds	the hash commitment does protect the fixed data
equivalence? current_owners, seen_owners	fails	the owners list the joiner trusts is not the current one

The first query targets the signature rather than the encrypted blob. An invalid signature fails verification, and a value used only inside a failed check does not count as accepted. The result must therefore come from a genuine signature over an older version. The trace confirms this: the attacker substitutes the old nonce, ciphertext, and signature together, and every check passes.

The second query confirms that the fixed half remains protected, isolating the rollback to the editable data.

Consequence

Any previously published user-data blob can replace the current one. Most notably, serving an old owners list can reverse the removal of a group-link owner. That former owner can then sign new user data. The same rollback can restore an old direct flag or relay list.

Suggested remedy

Add a monotonic version to the signed user data. A resolving client should reject any version lower than the highest version it has seen for that link. The fixed-data commitment can remain unchanged.

How to confirm

Capture an LGET response, publish new user data with LSET, then replay the captured response to a fresh resolver. Check whether the resolver accepts it.

---

Please confirm these findings at your earliest convenience. Thanks!