Behavioural specs (Allium)
Allium is a pre-formal behavioural layer used on the open signal-protocol library. It captures intended rules and invariants in a structured .allium file so gaps show up before (and beside) ProVerif models and hax extracts.
This page is not a claim that behaviour is Tested, Modeled, or Type-checked. Those words stay on the verification report and per-library pages. Allium does not discharge secrecy queries and does not type-check extracted Rust.
Where the artefacts live
| Artefact | Location |
|---|---|
| Behavioural spec | specs/signal-protocol-core.allium in the open library |
| How to use (optional CLI / skills) | specs/README.md |
| In-house library findings | security/SP-2026-library-audit.md |
| Positive regressions (former probes) | signal-protocol-core/tests/audit_probes.rs |
The juxt Allium skills and CLI are not vendored into the crypto tree. Contributors may install them locally; builds and Rust tests do not require them.
How it sits next to formal verification
| Layer | Question it answers |
|---|---|
| Allium | What should the system do? Which invariants are intended? |
| Audit probes / Rust tests | Does the production build match that intent today? |
| ProVerif | Do idealized processes satisfy secrecy / correspondence queries? |
| hax → F* / Rocq / Lean | Does the stub extract type-check under axioms? |
A green ProVerif or extract job does not imply production matches Allium. SP-2026-001–017 are mitigated in the library (and companion crates) with positive Rust regressions. ProVerif models were updated in this hardening pass (including sp2026_hardening.pv: SPK check, IK-bound AD, commit-after-AEAD, single-use OTPK). That remains research-grade symbolic modeling — not a firm audit of the messenger.
Hard break: regenerate Signal/PQXDH identities, re-sign SPK/PQ prekeys with Signal-spec XEdDSA, and re-pair sessions after upgrading. Handshake wire is v4 (binds OTPK id).
Example controls (SP-2026, mitigated in code)
Claim-bounded: the open library audit and tests document these; this page does not claim a firm audit or messenger verification.
| Theme | Allium invariant | Library status |
|---|---|---|
| Decrypt side effects | Commit ratchet / skipped-key maps only after AEAD success | Mitigated; ProVerif updated this pass |
| Previous chain | On DH ratchet, archive remaining keys using header PN | Mitigated |
| Prekey auth | Initiate verifies the signed prekey inside the library | Mitigated; ProVerif updated this pass |
| Identity | XEdDSA on a single X25519 key | Mitigated (hard break: re-sign + wire v4) |
| OTPK / wire | Handshake binds OTPK id (single-use) | Mitigated (wire v4) |
Details: the SP-2026 library audit. Protocol models: Signal Protocol formal verification.
Optional local workflow
npx skills add juxt/allium
cargo install allium-cli
allium check specs/*.allium
Agent skills such as /distill (code → spec) and /weed (reconcile spec ↔ code) are optional. allium check is structural hygiene on the .allium file — not a security proof.
Honesty
You may cite this page as documentation of a behavioural-spec practice on an open research library, and that SP-2026 items are claimed mitigated in that library’s audit/tests (not firm-audited). You may not cite it as formal verification of signal-protocol or as a messenger audit.
Next: Signal Protocol formal verification · Verification report · Security audit methodology.