I wanted to implement the Signal protocol for a series of secure messaging apps I’m working on, so I built this project to test and use in my own work. It’s still far from finished, but I think it’s at a stage where it’s worth sharing with the community.

IMPORTANT DISCLAIMER: This project is not professionally audited and is not production-ready. I do not recommend anyone use this in their own code yet. It is provided strictly for testing, experimentation, and demo purposes. I used AI as an assistant to help build this, so double-check everything before taking it seriously.

Project Links:

• GitHub: https://github.com/positive-intentions/signal-protocol
• Live Demo: https://signal.positive-intentions.com/
• Formal Verification Docs: https://glitr.io/docs/technical/formal-verification/signal-protocol
• Security Feedback (ROS): https://www.reddit.com/r/CyberSecurityAdvice/comments/1su8lir/security_audit_feedback_from_radically_open

Current Status & Development:

• Spec Alignment: The goal is to fully align with the official Signal protocol spec.
• Testing: It includes unit tests, but due to WASM testing limitations, I also added a Storybook-like UI to run and test it directly within a browser environment.

You used LLMs, right?

How did you manage to review all this?

thats right. i used LLM's. i reviewed this thoroughly myself. there are some in-house documents published on the website. for exmples threat-models, formal-verification and security audits. they are good for internal review but fundamentally invalid because its like "trust me bro"... and you shouldnt need to.

i would like to aim for a third-party review from an org like ROS or NLNet, but open source support isnt easy to come by on project as complicated as this. im sure many orgs are overwhelmed by AI slop and i've failed to make the cut several times, so im not expecting a professiona audit any time soon.

feel free to reach out for clarity on the details if you would like to investigate it further.

I mean on code level. How did you make sure, the LLM prints out something maintainable, understandable?

the typical software development approach: unit tests, reviewing PR changes, documenting details and CI/CD (to mention a few steps). its not something i can easily enumerate because in cybersecurity there are countless nuances to consider, which is how we end up with formal verification documents and security audits. all the internal documents are useful for me, but essentially geared toward being a starting point for a third-party reviewer.

the impementation here is being used in a couple functional messaging apps (similarly unaudited and unreviewed):

• https://enkrypted.chat/ - javascript based approach
• https://glitr.io/ - rust based approach

i will also be adding it to an open source project soon as seen at: https://github.com/positive-intentions/chat to give that e2e open-source transparency in the implementation.

Did you remember this time to tell copilot to actually write stuff in the files and not just create them?

Similar Signal rust projects:

https://github.com/wnoronha/signal-cli

https://github.com/foxl-ai/signal-cli

So you needed an implementation of a e2e protocol in rust.

So why didn't you use signals libraries directly? Or the Matrix implementation of it. Or OpenMLS the probable follower of the axolotl protocol.

All of which are implemented in Rust. All of them.had at least one security audit. All of them where implemented by people probably knowing much more about cryptonthen you.

Because vibe coders would rather spend the extra 100k tokens to have Claude "write it themselves" than actually have to do work in finding and integrating a 3rd party library I think 😂

There are a few nuances to my approach, but the key detail is that I wanted it to also work in a browser so I needed the ability to build to a wasm to be used in js.

Signal doesnt offer browser based capabilities and so I created this to target web aswell as native.

I used a frontier model to generate an allium spec from your repo and it found a few bugs. I like to run apps through allium to prepare for formal verification because it tends to find a LOT of flaws in even the most robust apps. The allium spec file is too large to share here but it can be generated by any frontier model.

Defects, three of them confirmed by running probes against the crate:

• P1, a late message from the previous chain breaks the session. The decrypt code never keeps the leftover keys of the old receiving chain, and it reads the header's previous chain length only as associated data. So a delayed message from the old chain looks like a new ratchet key. The session steps the ratchet again and the tag fails. In the probe, the next good message also failed with an AES-GCM error. Signal handles exactly this case, and the crate's out-of-order test only reorders messages within one chain.
• P2, one forged message with a made-up ratchet key desyncs the session for good. The ratchet step and key skipping happen before the tag is checked, and they're never rolled back. In the probe, the next real message failed.
• P3, a forged message naming a skipped key deletes that key before the tag check. The real message then fails with "Message number mismatch".
• The signed prekey's signature is never checked. x3dh_initiate_internal doesn't call verify_signed_prekey, and the WASM API doesn't expose it. Prekey authentication depends on every application remembering to do it.
• The X3DH associated data isn't bound to the two identities. It's the constant "X3DH_Key_Exchange" rather than both identity keys, and the ratchet never uses it anyway.
• The identity key and the signing key are unrelated. It uses a separate, unbound Ed25519 signing key instead of XEdDSA on the identity key.
• The first chain gets no DH ratchet. On both sides it's derived from the X3DH secret alone.
• Smaller issues:
• • There's no cap on the total number of skipped keys.
  • Cleanup drops keys in string order, not oldest first.
  • The send counter is a u32 with no overflow check.
  • The DH output isn't checked for all-zero values from small-order keys.
  • The legacy encrypt_message helper returns the message key to JavaScript.
    Variants, not defects: the non-standard HKDF salts and info strings. Both sides agree on them, and the spec says so.

-- VIOLATED: only one decrypt's skip is capped (max_skip); nothing caps
-- the total unless the application calls cleanup, so a peer that keeps
-- skipping grows the state without limit.
invariant SkippedKeysAreBounded {
    for s in Sessions:
        s.skipped.count <= config.max_skipped_total
}

invariant OneTimePreKeysBelongToOneSession {
    for a in Handshakes:
        for b in Handshakes:
            a != b and a.one_time_prekey != null
                implies a.one_time_prekey != b.one_time_prekey
}

invariant ResponderCannotSendBeforeReceiving {
    for s in Sessions:
        s.role = responder and s.receiving_ratchet_public = null
            implies s.sending_chain_key = null
}

open question "Should x3dh_initiate_internal take the signing key and signature and verify the signed prekey itself, so a caller cannot skip it?"

open question "Should the identity key sign with XEdDSA, so there is one long-term key instead of an unbound X25519 and Ed25519 pair?"

open question "Should decrypt work on a copy of the state and commit only after the tag verifies?"

open question "Should the associated data be IK_A || IK_B and be passed into every seal and open?"

Thanks! This is very helpful! I'll take a look and fix it.

No problem. It’s a surprisingly good tool despite relying completely on hallucination machines.