law ccm_round_trip

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

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/ccm.bend as CC

84# CCM: decryption accepts what encryption produced and gives the message
85# back, for every cipher, key, tag length, nonce, associated data and
86# message; when the parameters are refused, both refuse alike
87law ccm_round_trip:
88  for ~K: Data
89  for ~enc: K -> M.CmBlock -> M.CmBlock
90  for +k: K
91  for +m: Nat
92  for +nonce: B.Octets
93  for +aad: B.Octets
94  for +p: B.Octets
95  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, CC.Ccm.encrypt(~K, ~enc, k, m, nonce, aad, p), c => CC.Ccm.decrypt(~K, ~enc, k, m, nonce, aad, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => p, CC.Ccm.encrypt(~K, ~enc, k, m, nonce, aad, p)) : Result<&2, &2, M.CmError, B.Octets>}