law aes256_forgery_l

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

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

542law aes256_forgery_l:
543  for +key: List<&2, U32>
544  for +h: {List.length(&2, U32, key) == 32n : Nat}
545  for +nonce: List<&2, U32>
546  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
547  for +aad: List<&2, U32>
548  for +c: List<&2, U32>
549  for +t: List<&2, U32>
550  for +ht: {List.length(&2, U32, t) == 16n : Nat}
551  for ne: {t != G.aes_tag(key, nonce, aad, c) : List<&2, U32>}
552  {GCM.aes256_gcm_decrypt(key, nonce, aad, List.append(&2, U32, c, t)) == None{} : Maybe<&2, List<&2, U32>>}