proofs/crypto/mac/proof.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/proof.bend as Proof

9 imports

import Base
import ../../../src/crypto/mac.bend as MAC
import ../../../src/crypto/subtle.bend as Subtle
import ../../../spec/crypto/hmac.bend as Spec
import ../../../spec/crypto/subtle.bend as SubtleSpec
import ../subtle/laws.bend as SubtleLaws
import ../subtle/proof.bend as SubtleProof
import ./hmac.bend as P
import ./laws.bend as Laws

Definitions

def rejects source · line 31 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+tag:List<&2, U32> -> @ne:(@_:{tag == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.sign(key, msg) : List<&2, U32>} -> Empty) -> @+b:Bool -> @+eb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.verify(key, msg, tag) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.verify(key, msg, tag) == False{} : Bool}