law g_tag

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/sound.bend:135

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as RS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G

135law g_tag:
136  for +ok: Bool
137  for +nk: Nat
138  for +nr: Nat
139  for +key: List<&2, U32>
140  for +iv: List<&2, U32>
141  for +aad: List<&2, U32>
142  for +c: List<&2, U32>
143  for +t: List<&2, U32>
144  for +p: List<&2, U32>
145  for +hok: {RS.equal(t, G.tag(nk, nr, key, iv, aad, c)) == ok : Bool}
146  for +h: {G.accept(ok, G.gctr(nk, nr, key, c, G.inc32(G.j0(iv)))) == Some{p} : Maybe<&2, List<&2, U32>>}
147  {G.seal(nk, nr, key, iv, aad, p) == List.append(&2, U32, c, t) : List<&2, U32>}