law xts_round_trip

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

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/xts.bend as T

68# XTS on bytes, with ciphertext stealing: for every 16-byte sequence number
69# and every data unit of at least 16 bytes, encryption succeeds and
70# decryption gives the data unit back
71law xts_round_trip:
72  for ~K: Data
73  for ~enc: K -> M.CmBlock -> M.CmBlock
74  for ~dec: K -> M.CmBlock -> M.CmBlock
75  for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
76  for +k1: K
77  for +k2: K
78  for +i: B.Octets
79  for +p: B.Octets
80  for hi: {B.Octets.len(i) == 16n : Nat}
81  for hp: {Nat.is_le(16n, B.Octets.len(p)) == True{} : Bool}
82  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, T.Xts.encrypt(~K, ~enc, k1, k2, i, p), c => T.Xts.decrypt(~K, ~enc, ~dec, k1, k2, i, c)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}