feat(Protocols): Key exchange protocols and Diffie-Hellman#473

Closed

ChristianoBraga wants to merge 12 commits into

leanprover:mainfrom

Beneficial-AI-Foundation:key_exchange_pr

Commits on Apr 22, 2026

Commits on May 22, 2026

Merge branch 'main' of https://github.com/leanprover/cslib into key_exchange_pr
ChristianoBraga
committed
refactor(KeyExchange): relocate to Crypto/Protocols and trim imports

ChristianoBraga
and
claude
committed
refactor(DiffieHellman): drop KEP, rebase DH on `Module F G`

ChristianoBraga
and
claude
committed
refactor(DiffieHellman): move to its own directory, rename file to Basic

ChristianoBraga
and
claude
committed
feat(DiffieHellman): add `shared_eq_mul` canonical form, drop redundant linearity

ChristianoBraga
and
claude
committed
docs(DiffieHellman): drop Boneh–Shoup, link the two formulation references

ChristianoBraga
and
claude
committed
docs(DiffieHellman): drop References section

ChristianoBraga
and
claude
committed
docs(references): drop orphan BonehShoup entry

ChristianoBraga
and
claude
committed
feat(DiffieHellman): add `IsHonestGenerator` typeclass; gate `dh` on it

ChristianoBraga
and
claude
committed
feat(DiffieHellman): enforce primality gate; cite VCVio26

ChristianoBraga
and
claude
committed