law decrypt.invalid
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend as Lawsimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead.bend as A
153law decrypt.invalid:
154 for +alg: A.Alg
155 for +key: List<&2, U32>
156 for +nonce: List<&2, U32>
157 for +aad: List<&2, U32>
158 for +data: List<&2, U32>
159 for +h: {A.valid(alg, key, nonce) == False{} : Bool}
160 {A.decrypt(alg, key, nonce, aad, data) == None{} : Maybe<&2, List<&2, U32>>}
Uses (10)
Used by (0)
No other definition uses this definition.