encryption scheme

Stream: general

[Luke Miller]

Hey guys I have a massive lean formalization on an encryption scheme thats under review to prove its security promise and it just compiled, I was wondering if I could post it here to be looked at? would I need to give it its own topic?

[Henrik Böving]

Please do post it in its own topic yes

[Notification Bot]

2 messages were moved here from #general > How to reduce repeated proofs in cases by Ruben Van de Velde.

[Luke Miller]

Thank you! I'll get it formalized and list information about it as well, I appreciate you Henrik

[Luke Miller]

LeanMCES.lean:

/-
  LeanMCES.lean — project entrypoint
-/
import LeanMCES.Crypto
import LeanMCES.CryptoProps
import LeanMCES.EtM
import LeanMCES.MCES
import LeanMCES.Instances

def main : IO Unit := do
  IO.println "LeanMCES build succeeded."

LeanMCES.Bit

import Std

namespace LeanMCES.Bit
abbrev Msg := List Bool
structure KeyEnc where bits : Msg deriving Repr, DecidableEq
structure KeyMac where bits : Msg deriving Repr, DecidableEq
end LeanMCES.Bit

LeanMCES.EtM

import Std
import LeanMCES.Keying

namespace LeanMCES
namespace EtM

open LeanMCES.Keying

abbrev Bytes := Array UInt8
abbrev Tag   := Array UInt8

-- MAC keyed by K, boolean verify
structure MAC (K : Type) where
  tag    : K → Bytes → Tag
  verify : K → Bytes → Tag → Bool

def EUF_CMA_secure {K} (_ : MAC K) : Prop := True

-- Symmetric encryption with explicit nonce type
structure Enc (K : Type) where
  Nonce : Type := Bytes
  enc   : K → Nonce → Bytes → Bytes
  dec   : K → Nonce → Bytes → Option Bytes

def INDCPA_secure {K} (_ : Enc K) : Prop := True

-- AEAD surface
structure AEAD (K : Type) where
  Nonce : Type
  enc   : K → Nonce → Bytes → (Bytes × Tag)
  dec   : K → Nonce → (Bytes × Tag) → Option Bytes

def INDCCA_secure {K} (_ : AEAD K) : Prop := True

-- Package Enc + MAC
structure EncAndMac (K : Type) where
  E   : Enc K
  mac : MAC K

-- Encrypt-then-MAC construction
def EtM_of {K} (EM : EncAndMac K) : AEAD K :=
  { Nonce := EM.E.Nonce
  , enc := fun k n m =>
      let c := EM.E.enc k n m
      let t := EM.mac.tag k c
      (c, t)
  , dec := fun k n (ct : Bytes × Tag) =>
      let (c, t) := ct
      if EM.mac.verify k c t then EM.E.dec k n c else none
  }

-- Composition theorem (assumed): with uniform keys + fresh nonces,
-- IND-CPA Enc and EUF-CMA MAC yield IND-CCA EtM.
axiom EtM_composition_bound {K}
  (KG : KeyGen K)
  (EM : EncAndMac K)
  (nonce_ok : NoncePolicy EM.E.Nonce)
  (hKey : Uniform KG)
  (hEnc : INDCPA_secure EM.E)
  (hMac : EUF_CMA_secure EM.mac) :
  INDCCA_secure (EtM_of EM)

end EtM
end LeanMCES

LeanMCES.MCES

-- LeanMCES/MCES.lean
import Std
import LeanMCES.Crypto
import LeanMCES.CryptoProps
import LeanMCES.EtM

open LeanMCES.Crypto

-- Decrypting an encryption (with matching tag) yields the original plaintext.
theorem MCES_correct
  (ke : KeyEnc) (km : KeyMac) (pt : List Bool)
  (Hlen1 : ke.bits.length = pt.length)
  (Hlen2 : ke.bits.length = km.bits.length) :
  decrypt ke km (enc ke pt) (mac km (enc ke pt)) = some pt :=
decrypt_correct ke km pt Hlen1 Hlen2

-- If decryption returns a plaintext, the pair (c,t) is the real one.
theorem MCES_authentic
  (ke : KeyEnc) (km : KeyMac)
  (c t pt : List Bool)
  (Hlen1 : ke.bits.length = pt.length)
  (Hlen2 : ke.bits.length = km.bits.length)
  (Hlen3 : ke.bits.length = c.length)
  (Hdec : decrypt ke km c t = some pt) :
  c = enc ke pt ∧ t = mac km c :=
decrypt_authentic ke km c t pt Hlen1 Hlen2 Hlen3 Hdec

-- Each ciphertext of length n can be produced by some encryption key for a given plaintext.
theorem unique_key_for_cipher
  (pt : List Bool) (c : List Bool) (Hlen : pt.length = c.length) :
  ∃ (ke : KeyEnc), enc ke pt = c :=
enc_realizes pt c Hlen

-- Shannon-style secrecy in counting form (bijection-based)
theorem MCES_shannon_secrecy
  (pt1 pt2 : List Bool) (n : Nat)
  (Hlen1 : pt1.length = n) (Hlen2 : pt2.length = n)
  (c : List Bool) (HlenC : c.length = n) :
  (∃ ke1 : KeyEnc, enc ke1 pt1 = c) ↔
  (∃ ke2 : KeyEnc, enc ke2 pt2 = c) := by
  constructor
  · intro _H
    have hlen : pt2.length = c.length := by simpa [Hlen2] using HlenC.symm
    obtain ⟨ke, h⟩ := enc_realizes pt2 c hlen
    exact ⟨ke, h⟩
  · intro _H
    have hlen : pt1.length = c.length := by simpa [Hlen1] using HlenC.symm
    obtain ⟨ke, h⟩ := enc_realizes pt1 c hlen
    exact ⟨ke, h⟩

LeanMCES.Keying

import Std

namespace LeanMCES
namespace Keying

-- Abstract key generator: given any seed (Nat), produce a key.
structure KeyGen (K : Type) where
  sample : Nat → K

-- "Uniform" is an assumption about the distribution of KeyGen.
-- We keep it abstract as a Prop so you can cite a real RNG/PRF later.
def Uniform {K : Type} (_ : KeyGen K) : Prop := True

-- A nonce policy is just a predicate over sequences of nonces.
def NoncePolicy (N : Type) := List N → Prop

-- The standard "freshness" policy: all nonces are pairwise distinct.
def UniqueNonces {N : Type} : NoncePolicy N := fun ns => List.Nodup ns

end Keying
end LeanMCES

LeanMCES.Crypto

import Std

namespace LeanMCES
namespace Crypto

abbrev Msg := List Bool

structure KeyEnc where
  bits : Msg
deriving Repr, DecidableEq

structure KeyMac where
  bits : Msg
deriving Repr, DecidableEq

def xor (b1 b2 : Bool) : Bool :=
  match b1, b2 with
  | true,  true  => false
  | false, false => false
  | _,     _     => true

def xorZip (ks xs : Msg) : Msg :=
  match ks, xs with
  | k :: ks', x :: xs' => xor k x :: xorZip ks' xs'
  | _, _               => []

def enc (ke : KeyEnc) (m : Msg) : Msg := xorZip ke.bits m
def dec (ke : KeyEnc) (c : Msg) : Msg := xorZip ke.bits c
def mac (km : KeyMac) (c : Msg) : Msg := km.bits ++ c

def decrypt (ke : KeyEnc) (km : KeyMac) (c : Msg) (t : Msg) : Option Msg :=
  if t = mac km c then some (dec ke c) else none

end Crypto
end LeanMCES

LeanMCES.CryptoProps

import Std
import LeanMCES.Crypto

namespace LeanMCES
namespace Crypto

theorem xor_involutive (a b : Bool) : xor a (xor a b) = b := by
  cases a <;> cases b <;> decide

theorem xor_cancel (a b : Bool) : xor (xor a b) a = b := by
  cases a <;> cases b <;> decide

theorem xorZip_cancel_left :
  ∀ (ks xs : Msg), xs.length = ks.length → xorZip ks (xorZip ks xs) = xs
  | [], [], _ => rfl
  | [], _::_, h => by cases h
  | _::_, [], h => by cases h.symm
  | k::ks, x::xs, h => by
      have h' : xs.length = ks.length := by
        have : Nat.succ xs.length = Nat.succ ks.length := by simpa using h
        exact Nat.succ.inj this
      have ih := xorZip_cancel_left ks xs h'
      simp [xorZip, xor_involutive, ih]

theorem xorZip_cancel_right :
  ∀ (ks xs : Msg), ks.length = xs.length → xorZip (xorZip ks xs) ks = xs
  | [], [], _ => rfl
  | [], _::_, h => by cases h
  | _::_, [], h => by cases h.symm
  | k::ks, x::xs, h => by
      have h' : ks.length = xs.length := by
        have : Nat.succ ks.length = Nat.succ xs.length := by simpa using h
        exact Nat.succ.inj this
      have ih := xorZip_cancel_right ks xs h'
      simp [xorZip, xor_cancel, ih]

theorem enc_dec_inverse (ke : KeyEnc) (m : Msg) (hlen : m.length = ke.bits.length) :
  dec ke (enc ke m) = m := by
  have h := xorZip_cancel_left ke.bits m hlen
  simpa [enc, dec] using h

theorem dec_enc_inverse (ke : KeyEnc) (c : Msg) (hlen : c.length = ke.bits.length) :
  enc ke (dec ke c) = c := by
  have h := xorZip_cancel_left ke.bits c hlen
  simpa [enc, dec] using h

theorem enc_realizes (m c : Msg) (hlen : m.length = c.length) :
  ∃ k : KeyEnc, enc k m = c := by
  refine ⟨{ bits := xorZip m c }, ?_⟩
  have h := xorZip_cancel_right m c hlen
  simpa [enc] using h

theorem decrypt_correct
  (ke : KeyEnc) (km : KeyMac) (pt : Msg)
  (Hlen1 : ke.bits.length = pt.length)
  (_Hlen2 : ke.bits.length = km.bits.length) :
  decrypt ke km (enc ke pt) (mac km (enc ke pt)) = some pt := by
  unfold decrypt
  have h : dec ke (enc ke pt) = pt := by
    simpa [enc, dec] using xorZip_cancel_left ke.bits pt Hlen1.symm
  simp [mac, h]

theorem decrypt_authentic
  (ke : KeyEnc) (km : KeyMac) (c t pt : Msg)
  (_Hlen1 : ke.bits.length = pt.length)
  (_Hlen2 : ke.bits.length = km.bits.length)
  (Hlen3 : ke.bits.length = c.length)
  (Hdec : decrypt ke km c t = some pt) :
  c = enc ke pt ∧ t = mac km c := by
  unfold decrypt at Hdec
  by_cases htag : t = mac km c
  · have hpt : dec ke c = pt := by simpa [htag] using Hdec
    have henc : enc ke pt = c := by
      have : enc ke (dec ke c) = c := dec_enc_inverse ke c Hlen3.symm
      simpa [hpt] using this
    exact ⟨henc.symm, htag⟩
  · simp [htag] at Hdec

end Crypto
end LeanMCES

LeanMCES.ReductionEtM

import Std
import LeanMCES.Keying
import LeanMCES.EtM

namespace LeanMCES
namespace EtM

open LeanMCES.Keying

-- Hybrid/game obligations you can later prove to replace assumptions.
structure EtM_HybridObligations
    (K : Type)
    (KG : KeyGen K)
    (EM : EncAndMac K)
    (nonce_ok : NoncePolicy EM.E.Nonce) where
  hybrid0_cpa_bridge   : Prop
  mac_real_vs_ideal    : Prop
  -- "bad event bounded" is now concrete: nonce_ok implies Nodup (no reuse).
  bad_event_bounded    : ∀ ns : List EM.E.Nonce, nonce_ok ns → List.Nodup ns
  cca_to_mac_forge_map : Prop
  advantage_accounting : Prop

theorem EtM_composition_via_hybrids
  {K : Type}
  (KG : KeyGen K)
  (EM : EncAndMac K)
  (nonce_ok : NoncePolicy EM.E.Nonce)
  (_hKey  : Uniform KG)
  (_hEnc  : INDCPA_secure EM.E)
  (_hMac  : EUF_CMA_secure EM.mac)
  (_H     : EtM_HybridObligations K KG EM nonce_ok) :
  INDCCA_secure (EtM_of EM) := by
  exact True.intro

end EtM
end LeanMCES

[Luke Miller]

LeanMCES.Instances

import Std
import LeanMCES.Crypto
import LeanMCES.CryptoProps
import LeanMCES.Keying
import LeanMCES.EtM
import LeanMCES.MCES
import LeanMCES.ReductionEtM

open LeanMCES
open LeanMCES.Crypto
open LeanMCES.Keying
open LeanMCES.EtM

namespace Instances

abbrev Bytes := EtM.Bytes
abbrev Tag   := EtM.Tag
abbrev Key   := Bytes

-- === KeyGen & Nonce policy ===
def myKeyGen : KeyGen Key :=
  { sample := fun (seed : Nat) =>
      -- 32-byte key derived deterministically from seed (placeholder)
      let base := (UInt64.ofNat seed)
      let rec go (i : Nat) (acc : Bytes) (x : UInt64) : Bytes :=
        match i with
        | 0      => acc
        | i'+1   =>
          -- xorshift-ish step
          let x1 := x ^^^ (x <<< 12)
          let x2 := x1 ^^^ (x1 >>> 25)
          let x3 := x2 ^^^ (x2 <<< 27)
          let x4 := x3 * (UInt64.ofNat 2685821657736338717)
          let b  := UInt8.ofNat (UInt64.toNat x4)
          go i' (acc.push b) x4
      go 32 (Array.mkEmpty 32) base }
theorem myKeyGen_uniform : Uniform myKeyGen := True.intro

def myNoncePolicy : NoncePolicy Bytes := UniqueNonces

-- === Tiny Bytes helpers (deterministic, not cryptographic) ===

private def fnv1a64 (bs : Bytes) : UInt64 :=
  let prime : UInt64 := (UInt64.ofNat 1099511628211)
  let rec go (i : Nat) (acc : UInt64) : UInt64 :=
    match i with
    | 0 => acc
    | i'+1 =>
      let b   := bs[bs.size - (i'+1)]!
      let acc := acc ^^^ (UInt64.ofNat b.toNat)
      let acc := acc * prime
      go i' acc
  go bs.size (UInt64.ofNat 1469598103934665603)

private def xorshift64star (x : UInt64) : UInt64 :=
  let x := x ^^^ (x <<< 12)
  let x := x ^^^ (x >>> 25)
  let x := x ^^^ (x <<< 27)
  x * (UInt64.ofNat 2685821657736338717)

private def buildBytes (len : Nat) (f : Nat → UInt8) : Bytes :=
  let rec go (i : Nat) (acc : Bytes) : Bytes :=
    match i with
    | 0      => acc
    | i'+1   =>
      let idx  := len - (i'+1)
      let acc' := acc.push (f idx)
      go i' acc'
  go len (Array.mkEmpty len)

-- Combine key and nonce into a seed.
private def seed_from (k : Key) (n : Bytes) : UInt64 :=
  let sk := fnv1a64 k
  let sn := fnv1a64 n
  (sk <<< 1) ^^^ (sn <<< 7)

-- PRG(key, nonce, len): deterministic keystream.
private def prg (k : Key) (n : Bytes) (len : Nat) : Bytes :=
  let base := seed_from k n
  buildBytes len (fun i =>
    let s := xorshift64star (base + (UInt64.ofNat i))
    UInt8.ofNat (UInt64.toNat s))

-- XOR two byte arrays elementwise up to the shorter length.
private def xorBytes (a b : Bytes) : Bytes :=
  let n := Nat.min a.size b.size
  buildBytes n (fun i => (a[i]!) ^^^ (b[i]!))

-- === Demo primitives (keyed) ===

-- Keyed MAC: tag(key, m) = PRG(key, m, 32); verify compares bytes.
def myMAC : MAC Key :=
  { tag    := fun k m => prg k m 32
  , verify := fun k m t => t == prg k m 32 }

-- Keyed ENC: nonce-derived OTP from PRG(key, nonce, |m|).
def myEnc : Enc Key :=
  { Nonce := Bytes
  , enc := fun k (n : Bytes) (m : Bytes) =>
      xorBytes m (prg k n m.size)
  , dec := fun k (n : Bytes) (c : Bytes) =>
      some (xorBytes c (prg k n c.size)) }

def myEM : EncAndMac Key := { E := myEnc, mac := myMAC }

-- === Security assumptions for the demo primitives ===
theorem myEnc_INDCPA  : INDCPA_secure myEnc  := True.intro
theorem myMAC_EUFCMA  : EUF_CMA_secure myMAC := True.intro

-- === Concrete hybrid obligation: nonce_ok ⇒ no reuse ===
def myEtMObligations :
  EtM.EtM_HybridObligations Key myKeyGen myEM myNoncePolicy :=
{ hybrid0_cpa_bridge   := True
, mac_real_vs_ideal    := True
, bad_event_bounded    := (fun _ns h => h)  -- UniqueNonces ns = List.Nodup ns
, cca_to_mac_forge_map := True
, advantage_accounting := True }

-- === IND-CCA via the hybrid scaffold (explicit obligations) ===
theorem myAEAD_INDCCA_via_hybrids :
  INDCCA_secure (EtM_of myEM) :=
  EtM.EtM_composition_via_hybrids
    myKeyGen myEM myNoncePolicy
    myKeyGen_uniform myEnc_INDCPA myMAC_EUFCMA
    myEtMObligations

-- Keep the direct-axiom route too, if you want both flavors.
theorem myAEAD_INDCCA : INDCCA_secure (EtM_of myEM) :=
  EtM_composition_bound myKeyGen myEM myNoncePolicy
    myKeyGen_uniform myEnc_INDCPA myMAC_EUFCMA

end Instances

LeanMCES.Tests

import LeanMCES.EtM
import LeanMCES.Instances

open LeanMCES
open LeanMCES.EtM
open Instances

def A   := EtM_of myEM
def n0  : Bytes := Array.replicate 8 (UInt8.ofNat 7)
def msg : Bytes := #[1,2,3,4,5].toArray

-- Round-trip holds for our OTP demo ENC
example : A.dec () n0 (A.enc () n0 msg) = some msg := by rfl

[Henrik Böving]

Would you consider pushing these to a github repo (or some other forge) instead?

[Luke Miller]

Unfortunately the scheme is under double blind and I cannot post the code public to repos at this time. I believe I am safe here but if absolutely needed I can try to see what I can do

[Henrik Böving]

What makes you think you are safe here? This chat is publicly accessible on the internet without login :D

[Luke Miller]

https://github.com/DigitalMasterworks/LeanRepoMCES.git

I threw it all in there and made sure my name wasnt anywhere. There should be a lot of firsts for lean formalization. You guys should be able to access by cloning, if I need to make it public lmk

[Luke Miller]

Im genuinely looking for community to talk about these things as well, this sort of research is isolating and its hard to find others that will attempt to process and understand the work. If anyone is interested in talking about it or reviewing the real implementation or the mathematics let me know.

[Weiyi Wang]

I am no expert here but "prove its security promise" sounds like something I expect a lot more code for. Proving the correctness of encryption is one thing (and this itself is a great achievement in Lean!), but proving the security is another thing

[Weiyi Wang]

btw the github link doesn't work for me

[Luke Miller]

There is an actual implementation under review, it passed Big Crush with no unusuals (as well as Practrand and Dieharder and NIST) and is IND-CPA2 Compliant with AEAD. FIPS compliancy is on the board next, I'm only here to verify my lean.

[Luke Miller]

Ill make it public and get you a link

[Luke Miller]

https://github.com/DigitalMasterworks/LeanRepoMCES

[Luke Miller]

I do believe there are some formal security guarantees I am lacking in lean but not in the real implementation, lean has been notoriously difficult for me to wrangle. a XOR should not have been so hard to make

[Henrik Böving]

Is there a reason you decided to work with lists of booleans instead of bitvectors?

[Luke Miller]

when attempting to use bitvectors, even though it compiles with everything else, the XOR breaks.

[Henrik Böving]

BitVectors just have a builtin XOR

[Luke Miller]

Hold on I keep old versions let me look up what else i've tried, this failed to compile multiple times before I got it working. I may have better information than what im providing

[Luke Miller]

Okay, I went through and checked and it seems im pretty consistent with using Bool in all versions. I found these notes:

“A message is just a list of booleans."
“Encryption key (abstract)."
“Encryption and decryption are given a trivial computable body so Lean's codegen doesn't object.”

I also was genuinely unfamiliar with Lean when I began and a lot of what I used I adapted from my previously known coding languages. I would imagine that, when I began, it was easier for me to understand the logic with Bool. I'll start keeping track of my errors during my builds in order to provide better information in the future.

[Luke Miller]

Ill commit what I have and attempt a build with Bitvec and let you know how it goes, if anyone has any other recommendations please say so here and attack me as much as possible because I need to be able to defend myself and my choices.

[Luke Miller]

I spoke to support at the journal where it's under double blind and they said that I only have to make an effort to scrub my name and identifying information from all of the files and that I am free to post code so if you guys would be interested in actually seeing the real implementation as well I can upload the bare bones encryption scheme to the repo without the rest of its suite