AEZ v5 as a strong pseudorandom permutation

AEZ with tau = 0, no associated data, a 48-byte extracted key and a 16-byte nonce: a length-preserving SPRP with no authentication tag. Key extraction, associated-data hashing and aezPRF are omitted.

@[reducible, inline]

abbrev Cryptlib.Primitives.WideBlockCipher.AEZ.Block : Type

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.Block = Array UInt8

def Cryptlib.Primitives.WideBlockCipher.AEZ.zero16 : Block

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.zero16 = Array.replicate 16 0

def Cryptlib.Primitives.WideBlockCipher.AEZ.xor16 (a b : Block) : Block

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.xor16 a b = Array.ofFn fun (i : Fin 16) => a[↑i]! ^^^ b[↑i]!

def Cryptlib.Primitives.WideBlockCipher.AEZ.doubleBlock (p : Block) : Block

Doubling in GF(2¹²⁸) modulo x¹²⁸+x⁷+x²+x+1, big-endian.

Equations

• One or more equations did not get rendered due to their size.

The round function

AES4/AES10 whiten the input with the call-site j,i,l blocks, then apply 4 or 10 full AES rounds under a fixed schedule derived from the key.

structure Cryptlib.Primitives.WideBlockCipher.AEZ.EState : Type

• I0 : Block
• I1 : Block
• J0 : Block
• J1 : Block
• J2 : Block
• L : Array Block
• aes4Sched : List Block
• aes10Sched : List Block

def Cryptlib.Primitives.WideBlockCipher.AEZ.aes4 (e : EState) (j i l src : Block) : Block

AES4(j, i, l; src): whiten with the call-site j,i,l, then 4 fixed-schedule rounds.

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.aes4 e j i l src = Cryptlib.Primitives.WideBlockCipher.AEZ.roundsApply✝ (Cryptlib.Primitives.WideBlockCipher.AEZ.xor4✝ j i l src) e.aes4Sched

def Cryptlib.Primitives.WideBlockCipher.AEZ.aes10 (e : EState) (l src : Block) : Block

AES10(l; src): whiten with the call-site l alone, then 10 fixed-schedule rounds.

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.aes10 e l src = Cryptlib.Primitives.WideBlockCipher.AEZ.roundsApply✝ (Cryptlib.Primitives.WideBlockCipher.AEZ.xor16 src l) e.aes10Sched

@[simp]

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.aes4_size' (e : EState) (j i l src : Block) : Array.size (aes4 e j i l src) = 16

aes4 always produces a 16-byte block.

def Cryptlib.Primitives.WideBlockCipher.AEZ.initState (key48 : Block) : EState

The key schedule, from a 48-byte extracted key.

Equations

• One or more equations did not get rendered due to their size.

aezHash with tau = 0 and no associated data

def Cryptlib.Primitives.WideBlockCipher.AEZ.aezHashNoAD (e : EState) (nonce : ByteArray) : Block

Equations

• One or more equations did not get rendered due to their size.

aezTiny: inputs shorter than 32 bytes

def Cryptlib.Primitives.WideBlockCipher.AEZ.aezTinyParams (inBytes : Nat) : Nat × Nat

aezTiny's (i0, rounds) parameters. Separate so size proofs need not case-split on them.

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.aezTinyParams inBytes = if (inBytes == 1) = true then (7, 24) else if (inBytes == 2) = true then (7, 16) else if inBytes < 16 then (7, 10) else (6, 8)

def Cryptlib.Primitives.WideBlockCipher.AEZ.mkBuf (half ih2 : Nat) (mask pad : UInt8) (delta X : Block) (ctr : UInt8) : Block

The round buffer of aezTinyLR: X's first half bytes, mask/pad at ih2, XOR delta, then the counter byte XORed into the last position.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.aezTinyLR (e : EState) (delta : Block) (inArr : ByteArray) (d rounds i0 : Nat) : Block × Block

aezTiny's Feistel rounds, producing (L, R). Kept separate to keep proof terms small.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.aezTiny (e : EState) (delta : Block) (inArr : ByteArray) (d : Nat) : ByteArray

d = 0: encipher; d = 1: decipher.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.aezTiny_size (e : EState) (delta : Block) (inArr : ByteArray) (d : Nat) : (aezTiny e delta inArr d).size = inArr.size

The aezTiny Feistel ladder inverts

n forward double-rounds followed by n backward double-rounds on the swapped pair is the identity, for any round function.

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.xor16_get! {i : Nat} (hi : i < 16) (a b : Block) : (xor16 a b)[i]! = a[i]! ^^^ b[i]!

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.xor16_cancel {a : Block} (b : Block) (ha : Array.size a = 16) : xor16 (xor16 a b) b = a

XORing the same block twice is the identity.

def Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdStep (F : Nat → Block → Block) (k : Nat) (LR : Block × Block) : Block × Block

One forward double-round at iteration k, under counters 2k and 2k+1.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdStep (F : Nat → Block → Block) (s : Nat) (LR : Block × Block) : Block × Block

One backward double-round under counters s and s-1.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdN (F : Nat → Block → Block) : Nat → Block × Block → Block × Block

n forward double-rounds, counters ascending from 0.

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdN F 0 x✝ = x✝
• Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdN F n.succ x✝ = Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdStep F n (Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdN F n x✝)

def Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdN (F : Nat → Block → Block) : Nat → Block × Block → Block × Block

n backward double-rounds, counters descending from 2n-1.

Equations

• Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdN F 0 x✝ = x✝
• Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdN F n.succ x✝ = Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdN F n (Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdStep F (2 * n + 1) x✝)

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdN_size1 (F : Nat → Block → Block) (n : Nat) (L R : Block) (hL : Array.size L = 16) : Array.size (ladderFwdN F n (L, R)).fst = 16

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.ladderFwdN_size2 (F : Nat → Block → Block) (n : Nat) (L R : Block) (hR : Array.size R = 16) : Array.size (ladderFwdN F n (L, R)).snd = 16

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.ladderBwdN_ladderFwdN_swap (F : Nat → Block → Block) (n : Nat) (L R : Block) (hL : Array.size L = 16) (hR : Array.size R = 16) : ladderBwdN F n (ladderFwdN F n (L, R)).swap = (R, L)

n forward double-rounds, a swap, then n backward double-rounds return the swapped input, for any F.

aezCore: inputs of 32 bytes or more

The two passes process all 32-byte chunks except the final chunk and any shorter fragment, which are finished separately.

def Cryptlib.Primitives.WideBlockCipher.AEZ.aezCore (e : EState) (delta : Block) (inArr : ByteArray) (d : Nat) : ByteArray

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.aezCore_size (e : EState) (delta : Block) (inArr : ByteArray) (d : Nat) (h : 32 ≤ inArr.size) : (aezCore e delta inArr d).size = inArr.size

Top-level dispatch

def Cryptlib.Primitives.WideBlockCipher.AEZ.encipher (e : EState) (delta : Block) (inArr : ByteArray) : ByteArray

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.decipher (e : EState) (delta : Block) (inArr : ByteArray) : ByteArray

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.sprpEncrypt (key : Array UInt8) (iv msg : ByteArray) : ByteArray

SPRP encryption: 48-byte key, 16-byte IV.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.WideBlockCipher.AEZ.sprpDecrypt (key : Array UInt8) (iv msg : ByteArray) : ByteArray

SPRP decryption. With tau = 0 there is no tag to check.

Equations

• One or more equations did not get rendered due to their size.

Length preservation

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.encipher_size (e : EState) (delta : Block) (inArr : ByteArray) : (encipher e delta inArr).size = inArr.size

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.decipher_size (e : EState) (delta : Block) (inArr : ByteArray) : (decipher e delta inArr).size = inArr.size

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.sprpEncrypt_size (key : Array UInt8) (iv msg : ByteArray) : (sprpEncrypt key iv msg).size = msg.size

theorem Cryptlib.Primitives.WideBlockCipher.AEZ.sprpDecrypt_size (key : Array UInt8) (iv msg : ByteArray) : (sprpDecrypt key iv msg).size = msg.size

AEZ, as a WideBlockCipher

axiom Cryptlib.Primitives.WideBlockCipher.AEZ.aez_roundTrip (key : Array UInt8) (iv msg : ByteArray) (h16 : 16 ≤ msg.size) : sprpDecrypt key iv (sprpEncrypt key iv msg) = msg

AEZ round trip. An unproven axiom: only the aezTiny ladder is proved above; checked against sprp_aez.json.

def Cryptlib.Primitives.WideBlockCipher.AEZ.aez : WideBlockCipher

AEZ as a WideBlockCipher.

Equations

• One or more equations did not get rendered due to their size.