Stream ciphers, generically

Pseudorandomness is computational and not stated. The one law is that a request for len bytes of keystream produces exactly len bytes. keySize/ivSize are informational.

structure Cryptlib.Primitives.StreamCipher.StreamCipher : Type

• keySize : Nat
• ivSize : Nat
• keystream : ByteArray → ByteArray → (len : Nat) → ByteArray

  len bytes of keystream from a key and IV. len need not be a block multiple.

• keystream_size (key iv : ByteArray) (len : Nat) : (self.keystream key iv len).size = len

@[instance_reducible]

instance Cryptlib.Primitives.StreamCipher.instInhabitedStreamCipher : Inhabited StreamCipher

An all-zero keystream, showing the law is satisfiable. Provides no security.

Equations

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