law Verify.sound

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/mac/laws.bend:34

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC

34# A tag that verifies is the tag.
35law Verify.sound:
36  for +key: List<&2, U32>
37  for +msg: List<&2, U32>
38  for +tag: List<&2, U32>
39  for +h: {MAC.verify(key, msg, tag) == True{} : Bool}
40  {tag == MAC.sign(key, msg) : List<&2, U32>}