proofs/crypto/mac/laws.bend open laws/TODOs

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

4 imports

import Base
import ../../../src/crypto/mac.bend as MAC
import ../../../spec/crypto/hmac.bend as Spec
import ../../../spec/crypto/subtle.bend as SubtleSpec

Laws

law Sign.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 10 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.sign(key, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.hmac(key, msg) : List<&2, U32>}

sign is RFC 2104 / FIPS 198-1 HMAC over FIPS 180-4 SHA-256.

law Sign.length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 16 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.sign(key, msg)) == 32n : Nat}

Every tag is 32 bytes.

law Verify.value openits proof in laws_crypto.bend does not pass the checker (fails)source · line 22 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+tag:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.verify(key, msg, tag) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.hmac(key, msg), tag) : Bool}

verify is the reference comparison of the tag with the specified HMAC.

law Verify.accepts openits proof in laws_crypto.bend does not pass the checker (fails)source · line 29 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.verify(key, msg, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.sign(key, msg)) == True{} : Bool}

The tag of a message verifies.

law Verify.sound openits proof in laws_crypto.bend does not pass the checker (fails)source · line 35 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+tag:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.verify(key, msg, tag) == True{} : Bool} -> {tag == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.sign(key, msg) : List<&2, U32>}

A tag that verifies is the tag.

law Verify.rejects openits proof in laws_crypto.bend does not pass the checker (fails)source · line 43 · 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) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.verify(key, msg, tag) == False{} : Bool}

Any other tag is rejected.