proofs/crypto/mac/laws.bend source

proofs/crypto/mac/laws.bend on the hub · documented module

import Baseimport ../../../src/crypto/mac.bend as MACimport ../../../spec/crypto/hmac.bend as Specimport ../../../spec/crypto/subtle.bend as SubtleSpec# The clauses of src/crypto/mac.bend (HMAC-SHA256), proved in proof.bend.# Every clause is for every key, message and tag (any U32 lists).# sign is RFC 2104 / FIPS 198-1 HMAC over FIPS 180-4 SHA-256.law Sign.correct:  for +key: List<&2, U32>  for +msg: List<&2, U32>  {MAC.sign(key, msg) == Spec.hmac(key, msg) : List<&2, U32>}# Every tag is 32 bytes.law Sign.length:  for +key: List<&2, U32>  for +msg: List<&2, U32>  {List.length(&2, U32, MAC.sign(key, msg)) == 32n : Nat}# verify is the reference comparison of the tag with the specified HMAC.law Verify.value:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +tag: List<&2, U32>  {MAC.verify(key, msg, tag) == SubtleSpec.equal(Spec.hmac(key, msg), tag) : Bool}# The tag of a message verifies.law Verify.accepts:  for +key: List<&2, U32>  for +msg: List<&2, U32>  {MAC.verify(key, msg, MAC.sign(key, msg)) == True{} : Bool}# A tag that verifies is the tag.law Verify.sound:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +tag: List<&2, U32>  for +h: {MAC.verify(key, msg, tag) == True{} : Bool}  {tag == MAC.sign(key, msg) : List<&2, U32>}# Any other tag is rejected.law Verify.rejects:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +tag: List<&2, U32>  for ne: {tag != MAC.sign(key, msg) : List<&2, U32>}  {MAC.verify(key, msg, tag) == False{} : Bool}