proofs/crypto/mac/hmac.bend checks

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

8 imports

import Base
import ../../../src/crypto/mac.bend as MAC
import ../../../src/crypto/sha/sha256.bend as SHA
import ../../../spec/crypto/hmac.bend as Spec
import ../../../spec/crypto/sha.bend as FIPS
import ../sha/laws.bend as ShaLaws
import ../sha/correctness.bend as ShaCorrect
import ../../lib/logic.bend as L

Definitions

def fips_len source · line 19 · raw

@+bytes:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha.sha256_bytes(bytes)) == 32n : Nat}

def le_of_len source · line 22 · raw

@+xs:List<&2, U32> -> @+n:Nat -> @+k:Nat -> @+e:{List.length(&2, U32, xs) == n : Nat} -> @+h:{Nat.is_le(n, k) == True{} : Bool} -> {Nat.is_le(List.length(&2, U32, xs), k) == True{} : Bool}

def fits_len source · line 29 · raw

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

fits(key, n) looks at most n+1 bytes, and says length(key) <= n.

def mask_nil source · line 41 · raw

@+n:Nat -> @+pad:U32 -> @+hp:{U32.xor(0, pad) == pad : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.mask([], n, pad) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.xor_pad(List.replicate(U32, n, 0), pad) : List<&2, U32>}

Past the end of the key, mask emits 0 XOR pad.

def mask_pad source · line 51 · raw

@+key:List<&2, U32> -> @+n:Nat -> @+pad:U32 -> @+hp:{U32.xor(0, pad) == pad : U32} -> @+h:{Nat.is_le(List.length(&2, U32, key), n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.mask(key, n, pad) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.xor_pad(List.append(&2, U32, key, List.replicate(U32, Nat.sub(n, List.length(&2, U32, key)), 0)), pad) : List<&2, U32>}

mask is zero padding to n bytes followed by the byte-wise XOR.

def block_mask_if source · line 63 · raw

@+key:List<&2, U32> -> @+pad:U32 -> @+hp:{U32.xor(0, pad) == pad : U32} -> @+b:Bool -> @+eb:{Nat.is_le(List.length(&2, U32, key), 64n) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.mask(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.block_key_if(key, b), 64n, pad) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.xor_pad(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.zero_pad(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.shorten_if(key, b)), pad) : List<&2, U32>}

def block_mask source · line 72 · raw

@+key:List<&2, U32> -> @+pad:U32 -> @+hp:{U32.xor(0, pad) == pad : U32} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.mask(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.block_key(key), 64n, pad) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.xor_pad(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.k0(key), pad) : List<&2, U32>}

The masked key block of the implementation is (K0 XOR pad) of FIPS 198-1.

def inner source · line 78 · raw

@+key:List<&2, U32> -> @msg:List<&2, U32> -> List<&2, U32>

def outer source · line 81 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

def sign_correct source · line 84 · 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>}

def hmac_len source · line 91 · raw

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

Every tag is 32 bytes.

def sign_len source · line 94 · raw

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