feat(Protocols): Key exchange protocols and Diffie-Hellman#473
feat(Protocols): Key exchange protocols and Diffie-Hellman#473ChristianoBraga wants to merge 1 commit intoleanprover:mainfrom
Conversation
Add KeyExchangeProtocol class with agreement property and Diffie-Hellman as an instance over commutative groups.
| @@ -0,0 +1,99 @@ | |||
| /- | |||
There was a problem hiding this comment.
This file doesn't build because Diffie-Hellman.lean isn't a valid module name.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Overall, it appears the author did not build this to ensure it worked locally, so there are several issues. I tried to give a thorough review despite this.
| Let G := {gᵃ : a = 0, …, q − 1}, so that G is a subset of ℤₚ* of cardinality q. It is not hard | ||
| to see that G is closed under multiplication and inversion; that is, for all u, v ∈ G, | ||
| we have u·v ∈ G and u⁻¹ ∈ G. Indeed, gᵃ · gᵇ = gᵃ⁺ᵇ = gᶜ with c := (a + b) mod q, and (gᵃ)⁻¹ = gᵈ | ||
| with d := (−a) mod q. In the language of algebra, G is called a subgroup of the group ℤₚ*. |
There was a problem hiding this comment.
The module documentation describes a specific cryptographic setup with primes p, q, and a subgroup of ℤₚ*, but this instance is for any CommGroup G, any g : G, and any q : ℕ. The documentation should say the formalization only models the agreement equation, not the full DH setup/security assumptions. It should also be as general as the definition.
| agreement := by | ||
| intro α β | ||
| show (g ^ β.val) ^ α.val = (g ^ α.val) ^ β.val | ||
| rw [← pow_mul, ← pow_mul, mul_comm] |
There was a problem hiding this comment.
This proves the algebraic agreement equation for exponentiation in a commutative group, but it is
more general and weaker than the Diffie-Hellman setup described in the module documentation. The
instance does not encode that G is a cyclic subgroup of order q, that g has order q, that q is
prime, or that public values live in the subgroup generated by g. If this is intended as a
formalization of Diffie-Hellman, those parameters and invariants should be represented explicitly.
Otherwise, the documentation should describe this as the exponentiation-based key-agreement
skeleton rather than the Diffie-Hellman protocol.
| Reference: | ||
|
|
||
| * [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*, One-time pad][BonehShoup], | ||
| Section 10.4. |
There was a problem hiding this comment.
This is incorrect, referencing the one-time pad not DH.
|
|
||
| Reference: | ||
|
|
||
| * [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*][BonehShoup], |
There was a problem hiding this comment.
This citation is missing from the references.bib.
| Section 10.4. | ||
| -/ | ||
|
|
||
| instance DiffieHellmanKE {G : Type u} [CommGroup G] (g : G) (q : ℕ) : |
There was a problem hiding this comment.
This should not be an instance. The instance is not actually synthesizable after I renamed it on my end. Just make it a struct and a def.
There was a problem hiding this comment.
This should also be in a namespace.
|
|
||
| universe u v w | ||
|
|
||
| class KeyExchangeProtocol |
There was a problem hiding this comment.
We should define this in a namespace, not in the root. This is true across the whole file.
| omit [Fact q.Prime] in | ||
| theorem secret_eq (α β : ZMod q) : | ||
| (g ^ β.val) ^ α.val = g ^ (α * β).val := by | ||
| rw [← pow_mul, ZMod.val_mul, mul_comm β.val α.val, pow_mod_q hG] |
There was a problem hiding this comment.
Fact q.Prime appears to be dead code.
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Hi @ChristianoBraga, thanks for your interest in contributing! Can I ask that you disclose any AI usage in the PR description? There seem to be some patterns of AI usage based on the review that was just left.
3 participants
Summary
KeyExchangeProtocolclass capturing the structure of key exchange withpub,sharedSecret, and anagreementproperty ensuring both parties compute the same shared secret.pow_mod_qandsecret_eq.New files
Cslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Basic.lean— Key exchange classCslib/Systems/Distributed/Protocols/Cryptographic/KeyExchange/Diffie-Hellman.lean— Diffie-Hellman instanceReferences
Test plan
lake buildpasses with no errors