Migrate PublicKeyEncryption.lean to Lean 4

Author: str4d

Cryptolib/PublicKeyEncryption.lean

@@ -1,61 +1,70 @@
 /-
- -----------------------------------------------------------
-  Security games as pmfs
- -----------------------------------------------------------
+Copyright (c) 2021 Joey Lupo. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joey Lupo
 -/
+import Cryptolib.ToMathlib
+import Cryptolib.Uniform
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Probability.Distributions.Uniform
 
-import data.zmod.basic
-import probability.probability_mass_function.basic
-import to_mathlib
-import uniform
+/-!
+# Security games as PMFs
 
-noncomputable theory
+This file provides formal definitions for correctness and semantic security of a public
+key encryption scheme.
+-/
+
+noncomputable section
 
 /-
-  G1 = public key space, G2 = private key space,
-  M = message space, C = ciphertext space
-  A_state = type for state A1 passes to A2
+G1 = public key space, G2 = private key space,
+M = message space, C = ciphertext space
+A_state = type for state A1 passes to A2
 -/
-variables {G1 G2 M C A_state: Type} [decidable_eq M]
-          (keygen : pmf (G1 × G2))
-          (encrypt : G1 → M → pmf C)
-          (decrypt : G2 → C → M)
-          (A1 : G1 → pmf (M × M × A_state))
-          (A2 : C → A_state → pmf (zmod 2)) -- Should have G1 else how can A2 do further encryptions? Any general result about encryptions before getting challenge ciphertext...?
+variable {G1 G2 M C A_state: Type} [DecidableEq M]
+         (keygen : PMF (G1 × G2))
+         (encrypt : G1 → M → PMF C)
+         (decrypt : G2 → C → M)
+         (A1 : G1 → PMF (M × M × A_state))
+         (A2 : C → A_state → PMF (ZMod 2)) -- Should have G1 else how can A2 do further encryptions? Any general result about encryptions before getting challenge ciphertext...?
 
 /-
-  Executes the a public-key protocol defined by keygen,
-  encrypt, and decrypt
+Executes a public-key protocol defined by keygen,
+encrypt, and decrypt
 -/
 -- Simulates running the program and returns 1 with prob 1 if:
 -- `Pr[D(sk, E(pk, m)) = m] = 1` holds
-def enc_dec  (m : M) : pmf (zmod 2) :=  -- given a message m
+def enc_dec (m : M) : PMF (ZMod 2) :=  -- given a message m
 do
-  k ← keygen, -- produces a public / secret key pair
-  c ← encrypt k.1 m, -- encrypts m using pk
+  let k ← keygen -- produces a public / secret key pair
+  let c ← encrypt k.1 m -- encrypts m using pk
   pure (if decrypt k.2 c = m then 1 else 0) -- decrypts using sk and checks for equality with m
 
 /-
-  A public-key encryption protocol is correct if decryption undoes
-  encryption with probability 1
+A public-key encryption protocol is correct if decryption undoes
+encryption with probability 1
 -/
 
-def pke_correctness : Prop := ∀ (m : M), enc_dec keygen encrypt decrypt m = pure 1 -- This chain of encryption/decryption matches the monadic actions in the `enc_dec` function
+/-
+This chain of encryption/decryption matches the monadic actions in the `enc_dec` function
+-/
+def PkeCorrectness : Prop := ∀ (m : M), enc_dec keygen encrypt decrypt m = pure 1
 
 /-
-  The semantic security game.
-  Returns 1 if the attacker A2 guesses the correct bit
+The semantic security game.
+Returns 1 if the attacker A2 guesses the correct bit
 -/
-def SSG : pmf (zmod 2):=
+def SSG : PMF (ZMod 2) :=
 do
-  k ← keygen,
-  m ← A1 k.1,
-  b ← uniform_2,
-  c ← encrypt k.1 (if b = 0 then m.1 else m.2.1),
-  b' ← A2 c m.2.2,
+  let k ← keygen
+  let m ← A1 k.1
+  let b ← uniform_2
+  let c ← encrypt k.1 (if b = 0 then m.1 else m.2.1)
+  let b' ← A2 c m.2.2
   pure (1 + b + b')
 
 -- SSG(A) denotes the event that A wins the semantic security game
-local notation `Pr[SSG(A)]` := (SSG keygen encrypt A1 A2 1)
+local notation "Pr[SSG(A)]" => (SSG keygen encrypt A1 A2 1)
 
-def pke_semantic_security (ε : nnreal) : Prop := abs (Pr[SSG(A)] - 1/2) ≤ ε
+def PkeSemanticSecurity (ε : NNReal) : Prop := abs (Pr[SSG(A)].toReal - 1/2) ≤ ε

README.md

@@ -18,8 +18,6 @@ This library is a work-in-progress merge, port, and refactor of several forks of
 
 - `negligible.lean` - defines negligible functions and provides several useful lemmas regarding negligible functions
 
-- [pke.lean](src/pke.lean) - provides formal definitions for correctness and semantic security of a public key encryption scheme
-
 - [tactics.lean](src/tactics.lean) - provides the `bindskip` and `bindconst` tactics to help prove equivalences between pmfs
 
 - [rsa.lean](src/rsa.lean) - contains proof of correctness of the RSA public key encryption protocol