~/jendhub

proofs/crypto/mac/hmac.bend

bend-collections-laws-crypto@1.0.0.0 · 96 lines · 12 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Spec
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/laws.bend as ShaLaws
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/correctness.bend as ShaCorrect
8import bend-collections-laws-crypto@1.0.0.0/proofs/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
19def 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
22def 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.
29def 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.
41def 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.
51def 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
63def 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.
72def 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
78def 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
81def 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
84def 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.
91def 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
94def 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)