Wide-block ciphers

Encrypt and decrypt one arbitrarily long block. PRP security is computational and not stated; the laws are length preservation and round trip.

structure Cryptlib.Primitives.WideBlockCipher.WideBlockCipher : Type

• keySize : Nat
• ivSize : Nat
• encrypt : Array UInt8 → ByteArray → ByteArray → ByteArray

  Encrypts one block of any size ≥ 16 bytes.

• decrypt : Array UInt8 → ByteArray → ByteArray → ByteArray
• encrypt_size (key : Array UInt8) (iv msg : ByteArray) : (self.encrypt key iv msg).size = msg.size
• decrypt_size (key : Array UInt8) (iv msg : ByteArray) : (self.decrypt key iv msg).size = msg.size
• roundTrip (key : Array UInt8) (iv msg : ByteArray) : 16 ≤ msg.size → self.decrypt key iv (self.encrypt key iv msg) = msg

  Decryption inverts encryption for blocks of at least 16 bytes, for any key and IV.

@[instance_reducible]

instance Cryptlib.Primitives.WideBlockCipher.instInhabitedWideBlockCipher : Inhabited WideBlockCipher

The identity, showing the laws are satisfiable. Provides no security.

Equations

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