law cbc_round_trip

bend-osdev-cipher-modes@0.1.0.0 · LAWS.bend:30

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/cbc.bend as C

30# CBC on bytes: for every 16-byte IV and every message of whole blocks,
31# encryption succeeds and decryption gives the message back
32law cbc_round_trip:
33  for ~K: Data
34  for ~enc: K -> M.CmBlock -> M.CmBlock
35  for ~dec: K -> M.CmBlock -> M.CmBlock
36  for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
37  for +k: K
38  for +iv: B.Octets
39  for +m: B.Octets
40  for hi: {B.Octets.len(iv) == 16n : Nat}
41  for hm: {Nat.mod(B.Octets.len(m), 16n) == 0n : Nat}
42  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, C.Cbc.encrypt(~K, ~enc, k, iv, m), c => C.Cbc.decrypt(~K, ~dec, k, iv, c)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}