SymEnc.lean🔗

Tier 2 · definitions used by the symbolic proof 13 headline theorems depend on it 38 of 82 lines trusted source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Declarations on this page (11)

Symmetric Encryption Equational Theory

DyLean term algebra and attacker deduction rules for AES-256-CBC with PKCS#7 padding (symEnc and symDec).

namespace DY.SymEnc

class CanSymEncL26–29 ↗#

public
class CanSymEnc (Bytes: Type u) where
  symEnc: (key: Bytes) → (iv: Bytes) → (msg: Bytes) → Bytes
  symDec: (key: Bytes) → (iv: Bytes) → (ct: Bytes) → Err Bytes

export CanSymEnc (symEnc symDec)

namespace Enc

structure SubFL35–39 ↗#

public
structure SubF (Bytes: Type) where
  key: Bytes
  iv: Bytes
  msg: Bytes

instanceL41 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .ternary SubF.key SubF.iv SubF.msg

instanceL42 ↗#

public instance: SubBytesFunctor SubF := .ternary SubF.key SubF.iv SubF.msg SubF.mk

def SubF.lengthL44–48 ↗#

PKCS#7 padded ciphertext length 16 * (|msg| / 16 + 1).

@[expose] public
def SubF.length [BytesFunctor]: Bytes.PartialLength SubF :=
  fun { msg, .. } rec =>
    16 * (rec msg / 16 + 1)

end Enc

#combineL52–53 ↗#

#combine into BytesFunctor, BytesLength from
  Enc,

variable [BytesFunctor] [BytesFunctor.Has SubF]

abbrev Enc.SubF.packL57–58 ↗#

public
abbrev Enc.SubF.pack (x: Enc.SubF Bytes) := BytesView.pack x

instanceL60–68 ↗#

public
instance: CanSymEnc Bytes where
  symEnc key iv msg := ({key, iv, msg}: Enc.SubF Bytes).pack

  symDec key iv ct :=
    match ct.view? Enc.SubF with
    | some {key := key', iv := iv', msg} =>
      if key = key' ∧ iv = iv' then some msg else none
    | none => none

def symEnc.attackerKnowledgeL70–72 ↗#

@[expose] public
def symEnc.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ key iv msg, out = symEnc key iv msg ∧ p key ∧ p iv ∧ p msg

def symDec.attackerKnowledgeL74–76 ↗#

@[expose] public
def symDec.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ key iv ct, some out = symDec key iv ct ∧ p key ∧ p iv ∧ p ct

#combineL78–83 ↗#

#combine [BytesFunctor.Has SubF] into attackerKnowledge' from
  symEnc,
  symDec,

end DY.SymEnc