112 lines
4.4 KiB
Markdown
112 lines
4.4 KiB
Markdown
# CryptoVerif Models
|
||
|
||
Computational formal verification of the Soliton cryptographic protocol using
|
||
[CryptoVerif](https://bblanche.gitlabpages.inria.fr/CryptoVerif/).
|
||
|
||
These models were authored by the protocol designers and have not undergone
|
||
independent peer review. They are published for transparency and to facilitate
|
||
third-party verification. All results are machine-checkable and reproducible.
|
||
|
||
## Requirements
|
||
|
||
- CryptoVerif 2.12+
|
||
- The `pq.cvl` library (ships with CryptoVerif)
|
||
|
||
## Usage
|
||
|
||
```bash
|
||
# All models
|
||
CV_LIB=/path/to/pq ../verify.sh cryptoverif
|
||
|
||
# Single model
|
||
cryptoverif -lib /path/to/pq LO_Auth.cv
|
||
```
|
||
|
||
## Resource Usage
|
||
|
||
All 5 models complete in under 5 seconds total with negligible RAM usage.
|
||
No special hardware required.
|
||
|
||
## Results
|
||
|
||
Verified with CryptoVerif 2.12.
|
||
|
||
### LO_Auth.cv — Theorem 6 (Key Possession)
|
||
|
||
| Query | Result | Bound |
|
||
|-------|--------|-------|
|
||
| event(ServerAccepts) ==> event(ClientResponds) | proved | Ns × P_mac + P_kem |
|
||
| inj-event(ServerAccepts) ==> inj-event(ClientResponds) | proved | Ns × P_mac + P_kem |
|
||
|
||
Primitives: IND-CCA2 KEM (X-Wing), SUF-CMA deterministic MAC (HMAC-SHA3-256).
|
||
|
||
### LO_KEX.cv — Theorem 2b (Initiator Authentication)
|
||
|
||
| Query | Result | Bound |
|
||
|-------|--------|-------|
|
||
| event(Bob_Accept) ==> event(Alice_Init) | proved | P_sig_A |
|
||
|
||
Primitives: EUF-CMA signature (HybridSig). Proof uses only Alice's signature
|
||
unforgeability. Non-injective (replay is application-layer per §7.5 A4).
|
||
|
||
### LO_KEX_Secrecy.cv — Theorem 1 (Session Key Secrecy)
|
||
|
||
| Query | Result | Bound |
|
||
|-------|--------|-------|
|
||
| secret rk_A [cv_onesession] | proved | 2·P_prf + 2·P_kem_ik + 2·P_kem_spk + 2·P_kem_opk + collision terms |
|
||
|
||
Primitives: 3× IND-CCA2 KEM, PRF (HKDF). Signatures omitted (Theorem 1 is
|
||
secrecy, not authentication). No corruption oracles (Tamarin covers corruption
|
||
cases). See header comment for full simplifications list.
|
||
|
||
### LO_Ratchet_MsgSecrecy.cv — Theorem 3 (Message Key Secrecy)
|
||
|
||
| Query | Result | Bound |
|
||
|-------|--------|-------|
|
||
| secret test_mk [cv_onesession] | proved | 2 × P_prf |
|
||
|
||
Precondition: epoch key ek is fresh (from Theorem 1 + KDF_Root output
|
||
independence). Combined with AEAD IND-CPA+INT-CTXT under random keys
|
||
(standard [BN00] composition), gives full message secrecy.
|
||
|
||
### LO_Stream_Secrecy.cv — Theorem 13, Properties 1+2 (Streaming AEAD)
|
||
|
||
| Query | Result | Bound |
|
||
|-------|--------|-------|
|
||
| secret b0 [cv_bit] (IND-CPA) | proved | 2·P_ctxt + 2·P_cpa(time, N_enc) |
|
||
| inj-event(Received) ==> inj-event(Sent) (INT-CTXT) | proved | P_ctxt |
|
||
|
||
Adapted from CryptoVerif's TLS 1.3 Record Protocol example. Nonce uniqueness
|
||
enforced via table-based game hypothesis (§9.11(f)). base_nonce is public.
|
||
|
||
Key properties of the bounds:
|
||
- **INT-CTXT has no Q-factor** — direct forgery reduction
|
||
- **IND-CPA scales as N_enc × P_cpa** — Q-step hybrid argument
|
||
|
||
## Scope and Limitations
|
||
|
||
- **X-Wing as black box**: All models treat X-Wing as a monolithic IND-CCA2
|
||
KEM. The spec (§2.1) recommends opening the combiner for CryptoVerif. The
|
||
black-box assumption is stronger; bounds are in terms of P_kem rather than
|
||
component advantages (P_mlkem + P_x25519 + P_sha3_ro).
|
||
- **No corruption oracles**: The CryptoVerif KEX models prove security for
|
||
the no-corruption case. Corruption-parameterized secrecy (partial key
|
||
compromise, RNG corruption) is verified by the Tamarin models.
|
||
- **Simplified KDF info**: LO_KEX_Secrecy.cv binds fewer values in the PRF
|
||
input than the full HKDF info field. The PRF proof holds regardless of
|
||
info content; session-binding properties are verified by Tamarin.
|
||
- **Single-epoch message secrecy**: LO_Ratchet_MsgSecrecy.cv assumes a fresh
|
||
epoch key. The composition chain (Theorem 1 → KDF_Root → fresh ek → PRF →
|
||
fresh mk → AEAD) is sound but not mechanically verified end-to-end.
|
||
- **No Theorem 2c/d**: Key confirmation requires a combined KEX+Ratchet model.
|
||
|
||
## Theorem Coverage
|
||
|
||
| Theorem | Model | What's proved |
|
||
|---------|-------|---------------|
|
||
| 1 (KEX Key Secrecy) | LO_KEX_Secrecy | rk indistinguishable from random |
|
||
| 2b (Initiator Auth) | LO_KEX | σ_SI authentication via EUF-CMA |
|
||
| 3 (Message Secrecy) | LO_Ratchet_MsgSecrecy | mk indistinguishable from random |
|
||
| 6 (Auth Key Possession) | LO_Auth | Correspondence + injective |
|
||
| 13 P1 (IND-CPA) | LO_Stream_Secrecy | Bit secrecy of challenge bit |
|
||
| 13 P2 (INT-CTXT) | LO_Stream_Secrecy | Injective correspondence |
|