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 libraries don't offer browser based capabilities and so I created this to target web aswell as native.

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.

The impementation here is being used in a few experimental messaging apps (similarly unaudited and unreviewed):

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

I am also working towards adding it to an open source project soon as seen at: https://github.com/positive-intentions/chat for e2e open-source transparency in the implementation.

HQC is NIST's code-based backup to ML-KEM. Its reference implementation relies heavily on binary polynomial multiplication mod xⁿ − 1, with n up to 57,637.

I've proved the unmodified HQC v5.0.0 C implementation correct for hqc-1, hqc-3 and hqc-5.

• SAW proves vect_mul equivalent to a Cryptol model, using compositional Karatsuba proofs without expanding the full product. Scratch-buffer bounds are also verified.
• Isabelle/HOL proves the model implements the intended polynomial arithmetic. No sorry, smt or eval; oracle dependencies are checked.
• Also verified GF(2⁸) operations and the Reed–Solomon encoder's algebraic properties.
• All 63 SAW mutation tests fail as expected.

An interesting solver finding: the schoolbook leaf and Karatsuba model produce very different XOR/AND circuits. ABC, Z3, Yices and cvc5 couldn't finish in 10 minutes. SAW's Reed–Muller (rme) backend completed the proof in 6 seconds.

For GF(2) arithmetic, solver representation can make the difference between a practical proof and an intractable one.

Scope: This proves specific reference arithmetic, not HQC security. Decoders, sampling, hashing, KEM and constant-time behaviour are not covered. The GF(2⁸) results apply to v5.0.0, before the October specification change.

Reproducible with make hqc (~20 min) and make hqc-isabelle (~20 sec).

https://github.com/amarshat/pqc-assay

Criticism welcome, particularly on the property specifications.

Next: the AVX2 multiplier (PCLMULQDQ + Toom-3), which is closer to what actually runs in production.

Sophie made this post in response to the eMudhra Incident

https://infosec.exchange/@sophieschmieg/117474908437371419

She suggested randomness testing on keys

They are tuned aggressively to detect non-randomness only up to 10 standard deviations

However, she also added

The tests are not constant time, so you cannot run them over your actual keys as is

In other words, they aren't going to be run on actual production keys before the corresponding certs are going to be published

So these would be tests to test the randomness of your CSPRNG. However, eMudhra production keys are typically generated by a HSM, I am sure HSM CSPRNGs are pretty well tested before they are used in HSMs

So I don't understand how this is relevant to the current incident.

eMudhra case was because they generated some very small test keys outside of the HSM & then imported it into the HSM & accidently used it in production certificates

Post the eMudhra fiasco, it now seems like everyone is going to do checks to make sure certificates don't have private keys of size less than 32 significant bits - by running Paranoid Crypto or some other such testsuites

I was wondering why not set MSB = 1 like it's set for RSA primes - make it the standard - it will totally avoid the small key problem & the loss of security because of minor reduction in number of bits of security is also not significant.

I didn't realise this was a thing, looks like a very small initiative.

Anyways here's a youtube playlist of interviews with illuminaries in cryptography: https://www.youtube.com/playlist?list=PLqhpVxkBo1dOmNr6w2nF70W3_f43Qc5hE

I'm not a cryptographer or a cybersecurity expert. I'm a JavaScript dev. I'm interested in cryptography enough for it to become a side project.

Things like unit tests have always been a good idea for professional-grade work and ai has made it easier than ever.

For that extra bit, I want to use AI to create formal verification. Before I get too far, I'd like to ask about your experience with AI in formal-verification. The following is what I got so far.

https://glitr.io/docs/technical/formal-verification

As I learn how it works, I have a few questions about the approach.

- is it invalid because it's vibecoded?

- is the formal verification tooling enough?

- what am i overlooking?

I'm aware cybersecurity has countless nuances and formal verification is a small fraction of what it takes to create something secure and reliable.

IMPORTANT DISCLAIMER: While the project is aiming to provide a secure experience, it's far from finished. It cannot be audited or reviewed because it's close-source. I'm sharing here for feedback and demo purposes only. Feel free to reach out for clarity on any of the details instead of diving into the documentation. Pease use responsibly.

I maintain SMRFORGE, an open-source (MIT) tool that seals simulation results into evidence bundles and ships a standalone offline verifier. The verifier re-implements RFC 8032 Ed25519 verification in the Python standard library with its own field arithmetic. I know the advice against rolling your own. That is why I am asking people who do this for a living to try to break it.

Each bundle section (inputs, result, provenance) is canonicalized and hashed with SHA-256. The section digests roll up into bundle_sha256, which is SHA-256 of the canonical digest list. The signature is over the ASCII string "sha256:<hex>" rather than the raw 32 bytes. The verifier first checks the signature under the public key embedded in the bundle. That is the integrity verdict. It then compares the embedded key to a pinned key as a separate origin verdict. So the verifier does process arbitrary keys, which is why the input rules below matter.

Decisions I want reviewed

1. Cofactorless and strict. It checks [s]B == R + [k]A exactly, with k = SHA-512(R || A || M) read little-endian. There is no cofactor multiply.
   
2. It rejects a point encoding with y >= p, a scalar s >= L, and any point not on the curve.
   
3. It rejects small-order points where [8]A or [8]R is the identity. It also rejects a recovered x == 0 with the sign bit set, per RFC 8032 section 5.1.3 step 4.

This intentionally differs from libsodium, which is cofactored, and from original ref10, which is permissive, on small-order and mixed-order inputs. The right reference is a cofactorless strict verifier such as ed25519-dalek verify_strict, or the strict profile in Chalkias, Garillot, and Nikolaenko, "Taming the Many EdDSAs." The challenge is to find a (public key, message, signature) where my accept/reject disagrees with that profile.

About testing. There are 24 in-tree vectors, but the verifier itself produced their expected outcomes. They are regression and self-consistency checks, not independent known-answer tests. The independent checks were cross-validation against OpenSSL on random keys and messages in both directions, and the Chalkias et al. speccheck vectors. Every copy was run against those during development, but they are not vendored in the repo. There are five copies of the verifier, four in Python that largely mirror each other and one separate JavaScript implementation in the browser checker.

Known weaknesses. The RFC 3161 timestamp token is only shape-checked offline (valid base64 and a leading DER SEQUENCE tag). A separate openssl tool verifies it against a pinned TSA CA. And this is hand-rolled Ed25519 in pure Python.

My questions. Is rolling section digests into one signed bundle_sha256 sound? Should the trust-critical path use a vetted library, with the stdlib code kept only as a cross-check? Is shape-checking the timestamp offline and deferring crypto verification to openssl an acceptable split?

AI disclosure. I used Claude to write most of the verifier and to check this post against the source. I used Grok to draft and tidy the post. The prompts are in a comment below.

Sources

- Verifier: https://gitlab.com/smrforge/smrforge/-/blob/23ce423/smrf_verify/verify.py#L450
- Vectors: https://gitlab.com/smrforge/smrforge/-/blob/23ce423/conformance/ed25519/small_order_vectors.json
- Generator: https://gitlab.com/smrforge/smrforge/-/blob/23ce423/tools/gen_ed25519_kat.py
- RFC 8032: https://www.rfc-editor.org/rfc/rfc8032#section-5.1.7
- Taming the Many EdDSAs: https://eprint.iacr.org/2020/1244
- ed25519-dalek verify_strict: https://docs.rs/ed25519-dalek/latest/ed25519_dalek/struct.VerifyingKey.html#method.verify_strict

Not the first, will not be the last

A lovely & broad lay-person discussion of the OpenAI Navier-Stokes story and LLMs in mathematics.

We'd hopefully by now all know that hosted LLMs companies train upon their customers uploads and sessions (). It's clear this *"surveillance plagiarism" is a threat to cryptographers and security researchers who do really original work, as well as to any corporation using AI, but open weights models address this threat.

Vi Hart touches upon a broader array of topics: LLM psychosis. Modern mathematics was always a machine to be applied, ala the phrase "tenure machine", so AI doing so makes some sense. LLM proofs could retard the development of important abstractions, like how Aschbacher's announcement of the CFSG slowed research on the CFSG.

It stays solidly focused upon mathematics research however, without much direct discussion of applied topics like cryptography. Yet, there are fairly obvious impacts upon cryptography.

We correctly assume LLMs should overall raise our confidence in cryptographic software, because of auto-formalisation, eventually someone should figure out how to make LLMs write SE Linux profiles, etc and these are by far the lions share of the attack vectors.

Yet conversely, if LLM proofs cause mathematical subfields to be abandoned, then overall our confidence in problems being hard could decline, because organisations like IDA-CCR or China's version might not abandon some subtly relevant subfield. In other words, hybrid PQC+ECC protocols should become more important because of LLMs, not less.

Scott Aaronson also has an excellent post about LLM usage in mathematics too, somewhat more targeted towards mathematicians and computer scientists. It's slightly weakened towards the end by giving credence to AI doomer drama, but that's easily ignored.

Around (*), you should expect hosted LLM compajies would train upon data they promise not to train upon, either now or in future. In particular, there is a rich literature of non-cryptographic privacy preserving machine learning techniques, so similar work would buys them plausible deniability when training upon restricted data, but such techniques typically wind up being broken eventually.

Aside: Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs 

I'm the developer of SMS Import / Export, an Android Kotlin app that sequentially writes and reads large (multi GiB) files. A few months ago, I decided to add encryption to the app. I assumed that this would be a simple matter of finding an appropriate library / API that implemented the recommended modern standards, something in the AES or ChaCha20 families, and wiring it up.

Then I realized that I really should use authenticated encryption, and that's where the headaches began. Java / Kotlin offers CryptoOutputStream and CryptoInputStream, which can be used with AES-GCM or ChaChaPoly20-Poly1305 for authenticated encryption, so I initially tried them - but soon realized that they don't do streaming authenticated encryption and only authenticate the input stream after reading all of it, which means that I need to either buffer multiple GiBs of decrypted data in memory - not feasible on Android devices; store the decrypted data somewhere on disk - obviously insecure, or have my app process not-yet-authenticated data - obviously a bad idea.

I looked around for a ready-made streaming authenticated encryption solution, but the only one I could find was Google Tink's Streaming AEAD primitive. I tried using it, but I found Tink frustrating to work with, in large part due to its highly opinionated insistence on the use of its key management abstractions and its push toward the use of centralized key management systems.

So I wound up writing my own high level streaming authenticated wrapper around the libsodium SecretStream API, which I eventually split off into its own library, SecretStream For Kotlin:

Internally, SecretStreamOutputStream accumulates data passed in write() calls in a fixed size buffer; whenever this buffer fills up, the data is passed to the SecretStream API for encryption and the result is then written to the underlying OutputStream. (When the stream is closed, any remaining data is written in a final chunk, which may be smaller than the standard chunk size.) SecretStreamInputStream reads data in fixed size chunks, each of which is passed to the SecretStream API for decryption and authentication and the result stored in a fixed size buffer, from where it is provided to read() calls. No data is returned until it has been authenticated.

I'm not a cryptographer, and I was really hoping to find a ready-made solution and avoid reinventing any wheels or rolling my own crypto.

Questions: Is my approach sensible? Is there a better approach? Did I miss any useful facilities or libraries that I should have been using?

and part 3 !

previously:
part 2 https://00f.net/2026/10/06/zeroization-2/

part 1 https://00f.net/2026/10/06/zeroization-1/

Internxt is a post-quantum secure encrypted cloud storage provider which is open-source and has passed multiple independent audits.

I reviewed their code and found that post-quantum security should have been the least of their problems. Clicking a link in your browser could trigger remote code execution on the desktop app or leak your long-term encryption keys to an attacker-chosen URL. Their cryptographic architecture stands on shaky grounds with public keys never being verified, in some cases man-in-the-middled by design, a flat key hierarchy and a KDF with just 3 iterations of MD5.

We need PQC and we need it now, but adding a (self-rolled) PQC hybrid on top of a weak protocol does not make it more secure.

> LLM Disclosure: I used an LLM to help me write this post along with many hours of work, some of the findings (i.e. the RCE) were found with a local Qwen 3.5 27B model inside opencode (thanks r/LocalLLaMA ). It is impossible to share a single prompt since it was an iterative process, but I'm happy to elaborate on my methods if anyone cares.