Skip to content

Prove PeerAuthPQ_implies_PeerAuth via definitional refactor #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ChristianoBraga merged 1 commit into from
May 3, 2026
Merged

Prove PeerAuthPQ_implies_PeerAuth via definitional refactor #2

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 24 additions & 5 deletions PQXDHLean/SecurityDefs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -382,15 +382,34 @@ opaque PeerAuth (G : Type _) [AddCommGroup G]
(PK SK_kem CT SS : Type _) (kem : KEM PK SK_kem CT SS)
(I K : Type _) (kdf : KDF I K) : Prop

/-- §5.3.2 p. 480: Agreement over the post-quantum signed prekey (PQSPK /
KEM public key) — the extra conjunct that distinguishes `PeerAuthPQ`
(Theorem 6) from `PeerAuth` (Theorem 2). Without this property a
malicious server could substitute PQSPK without detection (the
re-encapsulation attack). Established under the SH-CR assumption on
the KEM (Theorem 6).

Like the other security properties in this file, kept opaque: the
internal structure documents the game but truth is axiomatically
assumed when the corresponding theorem is discharged externally. -/
opaque PQSPKAgreement (G : Type _) [AddCommGroup G]
(PK SK_kem CT SS : Type _) (kem : KEM PK SK_kem CT SS)
(I K : Type _) (kdf : KDF I K) : Prop

/-- Theorem 6, §5.3.2 p. 480: Extended peer authentication — `PeerAuth` plus
agreement over the post-quantum signed prekey (PQSPK / KEM public key).
Standard `PeerAuth` (Theorem 2) does NOT guarantee PQSPK agreement.
A malicious server could substitute PQSPK without detection (the
re-encapsulation attack). This stronger property requires the
additional SH-CR assumption on the KEM (Theorem 6). -/
opaque PeerAuthPQ (G : Type _) [AddCommGroup G]
additional SH-CR assumption on the KEM (Theorem 6).

Definitionally the conjunction of `PeerAuth` and `PQSPKAgreement`, so
`PeerAuthPQ_implies_PeerAuth` falls out as `And.left`. -/
def PeerAuthPQ (G : Type _) [AddCommGroup G]
(PK SK_kem CT SS : Type _) (kem : KEM PK SK_kem CT SS)
(I K : Type _) (kdf : KDF I K) : Prop
(I K : Type _) (kdf : KDF I K) : Prop :=
PeerAuth G PK SK_kem CT SS kem I K kdf ∧
PQSPKAgreement G PK SK_kem CT SS kem I K kdf

/-- `PeerAuthPQ` implies `PeerAuth`: PQSPK agreement is strictly
stronger, adding one more agreed parameter. -/
Expand All @@ -399,8 +418,8 @@ theorem PeerAuthPQ_implies_PeerAuth
(PK SK_kem CT SS : Type _) (kem : KEM PK SK_kem CT SS)
(I K : Type _) (kdf : KDF I K) :
PeerAuthPQ G PK SK_kem CT SS kem I K kdf →
PeerAuth G PK SK_kem CT SS kem I K kdf := by
sorry
PeerAuth G PK SK_kem CT SS kem I K kdf :=
And.left

/-- §2.4, p. 472 "Forward secrecy" and Theorem 1, §5.2 p. 479:
Forward secrecy — even if all long-term identity keys (IKₐ, IKᵦ)
Expand Down