law aegis128_tamper

bend-osdev-aead@0.1.0.0 · LAWS.bend:41

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-aead@0.1.0.0/aead.bend as Ad
import bend-osdev-aead@0.1.0.0/aegis128.bend as G

41# a tag of 16 bytes other than the one AEGIS-128 computes for the ciphertext
42# is refused, under a 16-byte nonce
43law aegis128_tamper:
44  for +k: G.AdAegisKey
45  for +n: B.Octets
46  for +a: B.Octets
47  for +c: B.Octets
48  for +t: B.Octets
49  for hn: {B.Octets.len(n) == 16n : Nat}
50  for hl: {B.Octets.len(t) == 16n : Nat}
51  for ht: {Ad.AdTag.is_eq(G.AdAegis128.tag_of(k, n, a, c), t) == False{} : Bool}
52  {G.AdAegis128.open(k, n, a, B.Octets.append(c, t)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}