feat(X3DH): skeleton for active-adversary message secrecy

[jinxinglim]

Summary

Introduces PQXDHLean/X3DH/X3DHActiveMessageSecrecy.lean — a structured skeleton for X3DH active-adversary (AKE-game) message secrecy, mirroring the existing passive proof in X3DHPassiveMessageSecrecy.lean.

This is the natural next step after passive secrecy: the paper's Theorem 2 (§5.2, p. 479) proves a much stronger active-adversary security result. This file lays the structural foundation for that proof — types, game state, oracle handlers, game variants, and theorem statements — so future work can fill in proof bodies one piece at a time.

What's in this PR

• One new file: PQXDHLean/X3DH/X3DHActiveMessageSecrecy.lean (~965 lines, ~60% comments/docstrings)
• Compiles with lake build (3 expected sorry warnings on placeholder bodies)
• No changes to existing files — purely additive

Status of components

Component	Status
File header (~100 lines docstring)	✓ done — covers AKE game, freshness, fixed-roles rationale, paper refs
SessionStatus, AliceSessionRecord, BobSessionRecord	✓ done — recv_* fields are Option G; each record has a transcript : List X3DHMessage
ActiveGameState + ActiveGameState.empty + Inhabited	✓ done
Party, AKEQuery, akeSpec, ActiveAdversary	✓ done
AKEStateM (state monad for handlers)	✓ done
akeQueryImpl — 5 oracle handlers	🚧 3/5 fully implemented (corrupt, revealSK, newSession); test partial; send sorry
activeGame body (two-pass simulateQ wiring)	✓ done
activeReal, activeRand	✓ done — executable end-to-end
activeSecrecyAdvantage	✓ done — executable end-to-end
X3DH_ActiveMessageSecrecy (local opaque Prop)	✓ done
x3dh_active_message_secrecy (main theorem)	🚧 statement done; proof sorry
passive_embeds_into_active (corollary sketch)	☐ statement done; proof sorry
## Follow-up work section	✓ done — 11 items with status markers and cross-refs

How to review

The file is large (~965 lines). I'd suggest reading in this order:

1. Header docstring (lines 1-101) — covers the AKE game, freshness conditions, the fixed-roles simplification (Alice always init, Bob always resp) with its symmetry-based justification, and paper references.

2. Session state section (lines ~136-340) — SessionStatus, X3DHMessage (currently Unit stub), AliceSessionRecord, BobSessionRecord, ActiveGameState. Pay attention to the recv_* field semantics (none = pending, some _ = received) and the transcript field (initialized to [] by newSession; future send will append). Notation convention block at the top of the section.

3. Active adversary section (lines ~340-430) — Party, AKEQuery, akeSpec, ActiveAdversary. The shape OracleComp (unifSpec + akeSpec + KDFOracle) Bool is the standard VCVio idiom for an interactive AKE adversary.

4. Oracle implementations section (lines ~432-625) — akeQueryImpl. Three handlers (corrupt, revealSK, newSession) are fully implemented; test is partial; send has a detailed TODO. The getTestKey callback parameterizes test for the two-game formulation. Only send will append to transcripts (when implemented).

5. Active secrecy games section (lines ~625-690) — activeGame, activeReal, activeRand. activeGame's body now does the full two-pass simulateQ: pass 1 (in AKEStateM) eliminates akeSpec; StateT.run' strips the state; pass 2 (in ProbComp) mirrors passive's execGame. activeReal and activeRand instantiate the getTestKey callback.

6. Advantage + theorem (lines ~695-755) — activeSecrecyAdvantage is fully defined; the main theorem's statement uses it indirectly via X3DH_ActiveMessageSecrecy.

7. ## Follow-up work section (lines ~775-end) — the most important section for understanding what's deferred and why. 11 numbered items with status markers and dependency notes.

Discussion items

These are design decisions worth surfacing before further work lands:

1. Fixed roles vs. flexible roles: documented in the header. The skeleton commits to Alice=init / Bob=resp throughout. By symmetry, no theorem is weakened. Open question: do we want to reconsider this for Double Ratchet later? (Section in header documents future-extension paths.)

2. X3DH_ActiveMessageSecrecy as local opaque Prop: defined here, not in SecurityDefs.lean. Should it be lifted to SecurityDefs.lean alongside MessageSecrecy and PeerAuth (small refactor, clean PR), or stay local for now? See follow-up §5.

3. SessionId := Nat vs. abstract: currently Nat; abstraction noted as a future refinement.

4. X3DHMessage = Unit stub: send is sorry partly because messages aren't concretized. Concretization would propagate type parameters (G, CT_aead, S_sig) up the stack. See follow-up §2. The transcript field currently holds List Unit — its structure (a list per session) is in place, but the contents are trivial until concretization.

5. recv_OPK ambiguity: none could mean "haven't received bundle" or "received bundle with no OPK". Documented as relying on the status field to disambiguate, but a more rigorous design might use Option (Option G). Worth a second look.

6. Long-term keys as parameters vs. game state: akeQueryImpl takes ikₐ ikᵦ spkᵦ as parameters rather than storing them in ActiveGameState. Justified because they're sampled once at game setup and never change. Alternative: include them in ActiveGameState for uniformity.

7. activeGame combined vs. split into activeGameOuter + execActiveGame: passive separates the game from its execution; we've combined them in activeGame. Could split for symmetry if proofs need access to the un-execed form.

Next steps (in order)

After this skeleton lands, the recommended order to fill in sorrys:

1. Define a partnering predicate (follow-up §1) — a concrete arePartners : AliceSessionRecord → BobSessionRecord → Prop over the new transcript fields. Needed by the partner-reveal freshness check (next).

2. Concretize Freshness predicates over ActiveGameState (follow-up §6) — small but important. Makes the Freshness hypothesis on the main theorem meaningful. Depends on partnering.

3. Lift X3DH_ActiveMessageSecrecy to SecurityDefs.lean (follow-up §5) — small refactor; arguably its own small PR.

4. Concretize X3DHMessage and implement send (follow-up §2) — biggest single chunk (~200-300 LOC). Pulls in Sig and AEAD parameters; likely propagates type parameters through AKEQuery / akeSpec / ActiveAdversary. Also wires send to maintain the transcript fields (the only handler that does).

5. Game-hop proof for the main theorem (follow-up §7) — multiple game hops using VCVio's tvDist_simulateQ_le_probEvent_bad. The largest effort.

6. passive_embeds_into_active corollary (follow-up §9) — derives passive_secrecy_le_ddh from active.

7. Expansion to other security properties (follow-up §11) — peer auth, forward secrecy, KCI, session independence, each in its own follow-up file.

[ChristianoBraga]

There is a lot here @jinxinglim.
However, this project will be further developed now by Galois.
Maybe we should talk to them first. What do you think?