law Aead.roundtrip

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/laws.bend:151

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

151# AEAD correctness of the specification: opening the sealed message gives
152# it back; C || T with T other than the tag of C is rejected.
153law Aead.roundtrip:
154  for +nk: Nat
155  for +nr: Nat
156  for +key: List<&2, U32>
157  for +iv: List<&2, U32>
158  for +aad: List<&2, U32>
159  for +pt: List<&2, U32>
160  {G.open(nk, nr, key, iv, aad, G.seal(nk, nr, key, iv, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}