law authenc_tamper

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

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/authenc.bend as Au

77# a tag of tlen bytes other than the computed one is refused, and the
78# cipher never runs
79law authenc_tamper:
80  for ~KE: Data
81  for ~KM: Data
82  for ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>
83  for ~mac: KM -> B.Octets -> B.Octets
84  for ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets
85  for ~tlen: Nat
86  for +k: Au.AdAuthencKey<KE, KM>
87  for +iv: B.Octets
88  for +aad: B.Octets
89  for +c: B.Octets
90  for +t: B.Octets
91  for hl: {B.Octets.len(t) == tlen : Nat}
92  for ht: {Ad.AdTag.is_eq(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c), t) == False{} : Bool}
93  {Au.AdAuthenc.open(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, k, iv, aad, B.Octets.append(c, t)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}