feat(UAKE): UAKE security notion#476
Conversation
…one only on non-final steps
🤖 PR SummaryThis PR adds the formalization of Unilaterally Authenticated Key Exchange (UAKE) following Dodis & Fiore 2017. New definitions and structures are introduced across four files under Statistics
Lean Declarations ✏️ Added: 26 declaration(s)
📋 **Additional Analysis**The diff adds new files and imports for the UAKE module. Two minor style violations are noted: The new files lack module docstrings ( 📄 **Per-File Summaries**
Last updated: 2026-07-15 19:25 UTC. |
|
Wrong link 😅 |
alexanderlhicks
left a comment
alexanderlhicks
left a comment
There was a problem hiding this comment.
🤖 AI-generated review
This review was produced by an AI assistant (Claude Code), invoked and supervised by @alexanderlhicks. Each finding was validated before posting (methods noted per comment), but please treat it as reviewer input to verify, not authority.
Soundness vs. the reference
First, a housekeeping item: the PR description links the wrong ePrint entry — 2014/144 is Andreeva et al., How to Securely Release Unverified Plaintext in Authenticated Encryption. The docstring in Defs.lean has the right one: ePrint 2017/109 (Dodis & Fiore, Unilaterally-Authenticated Key Exchange, FC 2017). Worth fixing the description for posterity.
I cross-checked the formalization against the paper, and it holds up well:
Exp/finalizematch the Sec. 3Exp^UAKE-Secexperiment branch-for-branch:K0 = ⊥ ⟹ K1 = ⊥;K0 ≠ ⊥ ∧not ping-pong⟹adversary wins (authenticity); otherwise real-or-randomK1with the full-ping-pong coin-flip nullifier. The reveal bookkeeping (revealedpersisting into the post phase,fullPingPongchecked on post-phase state against the challenge-phase transcript snapshot) correctly captures the paper's “one additional query” formulation.Matchingrealizes Def. 3: simulating the oracle's clock/recording logic for honest relays of 2–7 rounds (both leader parities) reproduces the paper's alternation exactly; message substitution and cross-session confusion correctly fail to match; and — a nice robustness property of the snapshot design — sessions opened or extended after the challenge completes can never retroactively match, by clock monotonicity. Details in the inline comment onMatching.CorrectExpis faithful to Def. 7, including its (the paper's own) weak conditional form; the docstring is upfront about this.- The documented model deviations (early reveal, reject-and-retry, unenforced well-formedness) are all adversary-favoring, so security in this model implies security in the paper's model. The “Model simplifications” docstring is genuinely excellent — more definitions PRs should do this.
Two soundness-adjacent polish items are flagged inline (post-phase stepChallenge availability; rounds semantics being load-bearing but undocumented) — both easy to validate and cheap to address.
Main suggestions (details inline)
- Adopt
ProbCompRuntimein place of the[MonadLiftT ProbComp m]/[MonadLiftT m SPMF]constraints — this is the established pattern acrossCryptoFoundations, and it keeps UAKE composable with the reduction infrastructure already stated against it. - Connect
advantageto theSecExp.leanhelpers, or document the deliberate paper-convention choice. - Trim or wire in currently-unused definitions (
Transcript.relabel/merge/combine/prefixWith,Party.RecoveryDeterministic,Party.OutputsAtCompletion).
Minor
- Docstring gaps on the public surface:
Schemefields (especiallyrounds),PerfectlyCorrect,oracleSpec,Adversary/ChallengeResultfields,challengeSession,finalize,advantage,Session,interleave,pingPong,recordOne/recordOpt,runHonest(Loop), and theStepResult.acceptAndSenddoneflag (“this send is my final message”). A sentence on the deliberate double-OptioninParty.output(outer = “no output yet”, inner = “output ⊥”) would also help readers — it takes a while to reconstruct. - Peer files are universe-polymorphic in the ambient monad (
m : Type → Type v, cf.INDCCA.lean); consider matching. - Naming: peers use
*_Game/*_Advantage(e.g.IND_CCA_Game);AKE.UAKE.Exp/advantageare fine namespaced, but worth a consistency thought. challengeSessionreturns thetkit was handed only to thread it tofinalize; passingtktofinalizedirectly would simplify the tuple.
Suggested follow-up (not blocking)
A machine-checked sanity lemma that the honest-relay adversary is ping-pong (for a toy protocol), and/or a toy instantiation under Examples/, would lock in the trickiest machinery and validate the definition's ergonomics.
Overall: careful, well-documented work — the two-phase stateful Adversary and the HasQuery.toQueryImpl … + opImpl composition mirror the INDCCA idiom nicely, and the game logic is faithful to the paper precisely in the places that are easiest to get wrong.
| | .acceptAndSend st' w' done => | ||
| let (tr1, c1) := recordOne t.transcript w env.clock | ||
| let (tr2, c2) := recordOne tr1 w' c1 | ||
| let key ← if done then (proto.T.output st' : m _) else pure none |
There was a problem hiding this comment.
🤖 AI-generated comment
Corner case worth a note in TSession.key's docstring: if proto.T.output st' returns none on a done step, then key = none is recorded, which the rest of the oracle reads as “session not completed” — the session stays steppable through the t.key gate above, and revealT returns none. This is only reachable for protocols violating the outputs-at-completion discipline, and it errs in the adversary-favoring (safe) direction, so no code change is needed — but the docstring currently states none ⟺ “session has not yet completed”, which this corner contradicts.
| noncomputable def advantage [SampleableType K] [DecidableEq W] [Monad m] | ||
| [MonadLiftT ProbComp m] [MonadLiftT m SPMF] {proto : Scheme m K UK TK W} | ||
| (A : Adversary proto) : ℝ := | ||
| |(Pr[= true | Exp A]).toReal - 1 / 2| |
There was a problem hiding this comment.
🤖 AI-generated comment
Consider connecting this to the existing advantage API in SecExp.lean rather than introducing a new formulation: peers define e.g. IND_CCA_Advantage runtime adversary := (IND_CCA_Game runtime adversary).boolBiasAdvantage. For a total (failure-free) game the two conventions differ by exactly a factor of 2, and the bridging lemma already exists (SPMF.boolBiasAdvantage_eq_two_mul_abs_sub_half). |Pr[true] − 1/2| matches DF'17's Def. 8 directly, so keeping it is defensible — in that case a short comment noting the deliberate paper-convention choice and its relation to boolBiasAdvantage (plus routing through runtime.evalDist per the comment on PerfectlyCorrect) would keep downstream reduction algebra consistent.
| /-- True if the final output message of a party is deterministic given the | ||
| state. I.e., all non-determinism is in the init and step functions. -/ | ||
| def RecoveryDeterministic [Monad m] (P : Party m In W Out) : Prop := | ||
| ∀ st : P.State, ∃ out, P.output st = pure out | ||
|
|
||
| /-- True if a party outputs a final message only once the protocol is complete. -/ | ||
| def OutputsAtCompletion [MonadLiftT m SetM] (P : Party m In W Out) : Prop := | ||
| (∀ i r, r ∈ support (P.init i) → ∀ out ∈ support (P.output r.state), out = none) ∧ | ||
| (∀ st w st' w', StepResult.acceptAndSend st' w' false ∈ support (P.step st w) → | ||
| ∀ out ∈ support (P.output st'), out = none) |
There was a problem hiding this comment.
🤖 AI-generated comment
Both predicates are currently unused — git grep -n 'RecoveryDeterministic\|OutputsAtCompletion' shows only these definitions. Notably, OutputsAtCompletion is exactly the property that model-simplification bullet 3 in Defs.lean leans on (“we do not enforce that U outputs K0 only at completion, which DF'17 (implicitly) assumes”). Two reasonable options:
- Bundle them into a named well-formedness predicate (e.g.
Scheme.WellFormed) that future security theorems take as a hypothesis, and reference it from that docstring; or - Defer them to the PR that first needs them.
Option 1 seems more in the spirit of a foundational definitions PR — it turns the docstring's informal WLOG argument into a checkable interface.
| def relabel {A B : Type} (f : A → B) (t : Transcript A) : Transcript B := | ||
| ⟨t.entries.map fun p => (f p.1, p.2)⟩ | ||
|
|
||
| def merge {A : Type} (t1 t2 : Transcript A) : Transcript A := | ||
| ⟨(t1.entries ++ t2.entries).mergeSort fun p q => decide (p.2 ≤ q.2)⟩ | ||
|
|
||
| def combine {A B : Type} (ta : Transcript A) (tb : Transcript B) : | ||
| Transcript (A ⊕ B) := | ||
| (ta.relabel Sum.inl).merge (tb.relabel Sum.inr) | ||
|
|
||
| def prefixWith {A B : Type} (a : A) (t : ℕ) (tb : Transcript B) : | ||
| Transcript (A ⊕ B) := | ||
| ⟨(Sum.inl a, t) :: tb.entries.map fun p => (Sum.inr p.1, p.2)⟩ |
There was a problem hiding this comment.
🤖 AI-generated comment
relabel, merge, combine, and prefixWith have no consumers in this PR — they are used only by each other (validate: git grep -nE 'relabel|combine|prefixWith' -- VCVio returns only these lines). If they're groundwork for a later development (e.g. assembling the global interleaved transcript for proofs about Matching), a one-line doc comment saying so would justify keeping them; otherwise consider deferring them to the PR that uses them, keeping this foundational file minimal.
| def interleave : Bool → List (ℕ × ℕ) → List ℕ | ||
| | _, [] => [] | ||
| | ab, (a, b) :: rest => (if ab then [a, b] else [b, a]) ++ interleave (!ab) rest | ||
|
|
||
| /-- Def. 3 from DF'17. A pair of transcripts match (T ⊆ T*) if their messages | ||
| are elementwise identical and their timestamps are "interleaved" as t₁ < t₁* | ||
| < t₂* < t₂ < ... or t₁* < t₁ < t₂ < t₂* < ..., depending on which party | ||
| speaks first. -/ | ||
| def Matching (oracleLeadsFirst : Bool) (T Tstar : Transcript W) : Prop := | ||
| T.entries.map Prod.fst = Tstar.entries.map Prod.fst ∧ | ||
| List.IsChain (· < ·) | ||
| (interleave oracleLeadsFirst ((T.entries.map Prod.snd).zip (Tstar.entries.map Prod.snd))) |
There was a problem hiding this comment.
🤖 AI-generated comment
A positive one: this machinery was stress-tested externally (a faithful re-implementation of the recordOne/opImpl clock bookkeeping plus this Matching predicate), and it checks out against DF'17 Def. 3 in every case tried: honest relays for 2–7 rounds under both leader parities match exactly; single-message substitution fails to match; with two interleaved oracle sessions, only the honestly-relayed one matches; and a session opened or extended after the challenge completes can never retroactively match a challenge snapshot — its final message's timestamp violates the alternation, by clock monotonicity. That last point means the fullPingPong-on-snapshot design in Defs.lean can't be gamed from the post phase.
Suggested (non-blocking) follow-up: a machine-checked version of the first fact — e.g. a lemma that the honest-relay adversary against a toy 2-round protocol satisfies isPingPong — would lock in the parity flag and interleave bookkeeping, the easiest places for a silent regression later.
Oops! Fixed. Thanks for catching that. |
…composability with existing VCVio lemmas
… the adversary guesses; express this in the doc comment
2 participants
This PR adds a model of unilaterally authenticated key exchange, a la Dodis & Fiore 2017. I've put it into
CryptoFoundations/AKE, since it seems likely that multiple AKE definitions would be useful. This is just a simple and well accepted one.Some caveats about the model are in the doc comment at the top of
UAKE/Defs.lean.