1 import Base 2 import ../../../src/crypto/mac.bend as MAC 3 import ../../../src/crypto/sha/sha256.bend as SHA 4 import ../../../spec/crypto/hmac.bend as Spec 5 import ../../../spec/crypto/sha.bend as FIPS 6 import ../sha/laws.bend as ShaLaws 7 import ../sha/correctness.bend as ShaCorrect 8 import ../../lib/logic.bend as L 9 10 # HMAC-SHA256: the implementation src/crypto/mac.bend equals the RFC 2104 / 11 # FIPS 198-1 specification spec/crypto/hmac.bend for every key and message 12 # (the functional-correctness statement of HACL*'s Hacl.HMAC against 13 # Spec.HMAC, and of the VST HMAC proof of Beringer, Petcher, Ye and Appel 14 # 2015 against its FIPS 198-1 functional model). SHA-256 enters only through 15 # its proved refinement ShaLaws.sha256_bytes_correct. 16 17 # ---- SHA-256 facts ---- 18 19 def fips_len(+bytes: List<&2, U32>) -> {List.length(&2, U32, FIPS.sha256_bytes(bytes)) == 32n : Nat}: 20 ShaCorrect.digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial())) 21 22 def le_of_len(+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}: 23 %Equal.sym(Nat, List.length(&2, U32, xs), n, e) : {Nat.is_le(_, k) == True{} : Bool} 24 h 25 26 # ---- the key block ---- 27 28 # fits(key, n) looks at most n+1 bytes, and says length(key) <= n. 29 def fits_len(+key: List<&2, U32>, +n: Nat) -> {MAC.fits(key, n) == Nat.is_le(List.length(&2, U32, key), n) : Bool}: 30 match key n: 31 case Nil{} 0n: 32 {==} 33 case Nil{} 1n+p: 34 {==} 35 case k <> rest 0n: 36 {==} 37 case k <> rest 1n+ +p: 38 fits_len(rest, p) 39 40 # Past the end of the key, mask emits 0 XOR pad. 41 def mask_nil(+n: Nat, +pad: U32, +hp: {U32.xor(0, pad) == pad : U32}) -> {MAC.mask(Nil{}, n, pad) == Spec.xor_pad(List.replicate(U32, n, 0), pad) : List<&2, U32>}: 42 match n: 43 case 0n: 44 {==} 45 case 1n+ +p: 46 %hp : {_ <> MAC.mask(Nil{}, p, pad) == U32.xor(0, pad) <> Spec.xor_pad(List.replicate(U32, p, 0), pad) : List<&2, U32>} 47 %mask_nil(p, pad, hp) : {U32.xor(0, pad) <> MAC.mask(Nil{}, p, pad) == U32.xor(0, pad) <> _ : List<&2, U32>} 48 {==} 49 50 # mask is zero padding to n bytes followed by the byte-wise XOR. 51 def mask_pad(+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}) -> {MAC.mask(key, n, pad) == Spec.xor_pad(List.append(&2, U32, key, List.replicate(U32, Nat.sub(n, List.length(&2, U32, key)), 0)), pad) : List<&2, U32>}: 52 match key n: 53 case Nil{} 0n: 54 {==} 55 case Nil{} 1n+ +p: 56 mask_nil(1n+p, pad, hp) 57 case k <> rest 0n: 58 Empty.absurd({MAC.mask(k <> rest, 0n, pad) == Spec.xor_pad(List.append(&2, U32, k <> rest, List.replicate(U32, Nat.sub(0n, List.length(&2, U32, k <> rest)), 0)), pad) : List<&2, U32>}, L.false_true(h)) 59 case +k <> +rest 1n+ +p: 60 %mask_pad(rest, p, pad, hp, h) : {U32.xor(k, pad) <> MAC.mask(rest, p, pad) == U32.xor(k, pad) <> _ : List<&2, U32>} 61 {==} 62 63 def block_mask_if(+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}) -> {MAC.mask(MAC.block_key_if(key, b), 64n, pad) == Spec.xor_pad(Spec.zero_pad(Spec.shorten_if(key, b)), pad) : List<&2, U32>}: 64 match b: 65 case True{}: 66 mask_pad(key, 64n, pad, hp, eb) 67 case False{}: 68 %Equal.sym(List<&2, U32>, SHA.sha256_bytes(key), FIPS.sha256_bytes(key), ShaLaws.sha256_bytes_correct(key)) : {MAC.mask(_, 64n, pad) == Spec.xor_pad(Spec.zero_pad(FIPS.sha256_bytes(key)), pad) : List<&2, U32>} 69 mask_pad(FIPS.sha256_bytes(key), 64n, pad, hp, le_of_len(FIPS.sha256_bytes(key), 32n, 64n, fips_len(key), {==})) 70 71 # The masked key block of the implementation is (K0 XOR pad) of FIPS 198-1. 72 def block_mask(+key: List<&2, U32>, +pad: U32, +hp: {U32.xor(0, pad) == pad : U32}) -> {MAC.mask(MAC.block_key(key), 64n, pad) == Spec.xor_pad(Spec.k0(key), pad) : List<&2, U32>}: 73 %Equal.sym(Bool, MAC.fits(key, 64n), Nat.is_le(List.length(&2, U32, key), 64n), fits_len(key, 64n)) : {MAC.mask(MAC.block_key_if(key, _), 64n, pad) == Spec.xor_pad(Spec.zero_pad(Spec.shorten_if(key, Nat.is_le(List.length(&2, U32, key), 64n))), pad) : List<&2, U32>} 74 block_mask_if(key, pad, hp, Nat.is_le(List.length(&2, U32, key), 64n), {==}) 75 76 # ---- HMAC ---- 77 78 def inner(+key: List<&2, U32>, msg: List<&2, U32>) -> List<&2, U32>: 79 List.append(&2, U32, Spec.xor_pad(Spec.k0(key), 54), msg) 80 81 def outer(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>: 82 List.append(&2, U32, Spec.xor_pad(Spec.k0(key), 92), FIPS.sha256_bytes(inner(key, msg))) 83 84 def sign_correct(+key: List<&2, U32>, +msg: List<&2, U32>) -> {MAC.sign(key, msg) == Spec.hmac(key, msg) : List<&2, U32>}: 85 %Equal.sym(List<&2, U32>, MAC.mask(MAC.block_key(key), 64n, 92), Spec.xor_pad(Spec.k0(key), 92), block_mask(key, 92, {==})) : {SHA.sha256_bytes(List.append(&2, U32, _, SHA.sha256_bytes(List.append(&2, U32, MAC.mask(MAC.block_key(key), 64n, 54), msg)))) == FIPS.sha256_bytes(outer(key, msg)) : List<&2, U32>} 86 %Equal.sym(List<&2, U32>, MAC.mask(MAC.block_key(key), 64n, 54), Spec.xor_pad(Spec.k0(key), 54), block_mask(key, 54, {==})) : {SHA.sha256_bytes(List.append(&2, U32, Spec.xor_pad(Spec.k0(key), 92), SHA.sha256_bytes(List.append(&2, U32, _, msg)))) == FIPS.sha256_bytes(outer(key, msg)) : List<&2, U32>} 87 %Equal.sym(List<&2, U32>, SHA.sha256_bytes(inner(key, msg)), FIPS.sha256_bytes(inner(key, msg)), ShaLaws.sha256_bytes_correct(inner(key, msg))) : {SHA.sha256_bytes(List.append(&2, U32, Spec.xor_pad(Spec.k0(key), 92), _)) == FIPS.sha256_bytes(outer(key, msg)) : List<&2, U32>} 88 ShaLaws.sha256_bytes_correct(outer(key, msg)) 89 90 # Every tag is 32 bytes. 91 def hmac_len(+key: List<&2, U32>, +msg: List<&2, U32>) -> {List.length(&2, U32, Spec.hmac(key, msg)) == 32n : Nat}: 92 fips_len(outer(key, msg)) 93 94 def sign_len(+key: List<&2, U32>, +msg: List<&2, U32>) -> {List.length(&2, U32, MAC.sign(key, msg)) == 32n : Nat}: 95 %Equal.sym(List<&2, U32>, MAC.sign(key, msg), Spec.hmac(key, msg), sign_correct(key, msg)) : {List.length(&2, U32, _) == 32n : Nat} 96 hmac_len(key, msg)