EtMDefs.lean
Declarations on this page (8)
Encrypt-then-MAC AEAD from a one-time cipher and a PRF-based MAC
Trusted in part. The theorems of Computational/ use only CipherScheme, MACScheme, PRFAdversary, PRFState, prfAdvantage, prfEval, prfGame, prfSpec from this file: read them. Everything else here is checked by Lean. See Computational/.
Defines one-time symmetric ciphers (CipherScheme, indcpaEncrypt, indcpaGame, indcpaAdvantage), deterministic MACs/PRFs (MACScheme), the Encrypt-then-MAC AEADScheme etm, the decryption-query bound MakesAtMostDecQueries, and the concrete reductions redCipher, redMACChall, and redMACForge used by etm_otcca (EtM.lean). Because the OT-CCA and IND-CPA games sample uniform ciphertexts from $ᵗ C, instantiations with AES-256-CBC fix the plaintext length (DEV-AEAD2).
@[expose] public sectionopen OracleComp OracleSpec ENNReal MeasureTheorynamespace CryptoGamesOne-time symmetric cipher (IND-CPA)
structure CipherScheme
A deterministic one-time symmetric cipher. All randomness (e.g. key and IV in Signal's AES-256-CBC-PKCS#7) comes from the one-time key Key. Decryption returns Option Message to accommodate padding validation.
structure CipherScheme (Key Message Ciphertext : Type) where
/-- `Enc(k, m)`: encrypt message `m` under key `k`. -/
enc : Key → Message → Ciphertext
/-- `Dec(k, c)`: decrypt ciphertext `c` under key `k`; `none` means rejection (e.g. bad padding). -/
dec : Key → Ciphertext → Option Message10 declarations not shown (lines 54–122): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
Deterministic MAC / PRF game
structure MACScheme
A deterministic MAC / PRF with key space Key, input space Input, and tag space Tag (in Signal: 8-byte truncated HMAC-SHA256).
structure MACScheme (Key Input Tag : Type) where
/-- `Tag(k, x)`: compute the authentication tag of `x` under key `k`. -/
tag : Key → Input → Tagnamespace MACSchemevariable {Key Input Tag : Type}abbrev prfSpec
PRF evaluation oracle Input →ₒ Tag.
abbrev prfSpec (Input Tag : Type) :=
Input →ₒ Tagstructure PRFState
PRF game state: key, hidden bit b, and the lazy table of the random function.
structure PRFState (Key Input Tag : Type) where
key : Key
b : Bool
table : List (Input × Tag) := []abbrev PRFAdversary
A PRF adversary, with its own coins (unifSpec) and the evaluation oracle Input →ₒ Tag.
abbrev PRFAdversary (Input Tag : Type) :=
OracleComp (unifSpec + prfSpec Input Tag) Bool1 declaration not shown (lines 152–154): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames.
variable [DecidableEq Input] [SampleableType Tag]def prfEval
PRF evaluation oracle: b = false returns mac.; b = true returns a lazily sampled random function on Input → Tag.
def prfEval (mac : MACScheme Key Input Tag) :
QueryImpl (prfSpec Input Tag) (StateT (PRFState Key Input Tag) ProbComp) := fun x => do
let st ← get
if st.b then
match st.table.lookup x with
| some t => return t
| none =>
let t ← liftM ($ᵗ Tag)
set { st with table := (x, t) :: st.table }
return t
else
return mac.tag st.key x1 declaration not shown (lines 173–179): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames.
def prfGame
PRF hidden-bit game.
def prfGame [SampleableType Key] (mac : MACScheme Key Input Tag)
(A : PRFAdversary Input Tag) : ProbComp Bool := do
let b ← $ᵗ Bool
let key ← $ᵗ Key
let impl := (QueryImpl.ofLift unifSpec ProbComp).liftTarget
(StateT (PRFState Key Input Tag) ProbComp) + prfEval mac
let b' ← (simulateQ impl A).run' { key, b }
return b == b'def prfAdvantage
Adv^{prf}_{mac}(A), the bias 2·|Pr[b = b'] − 1/.
noncomputable def prfAdvantage [SampleableType Key]
(mac : MACScheme Key Input Tag) (A : PRFAdversary Input Tag) : ℝ≥0∞ :=
𝒟[mac.prfGame A].boolBias1 declaration not shown (lines 196–204): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames.
end MACScheme10 declarations not shown (lines 216–342): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
end CryptoGames