proofs/crypto/kdf/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 84 lines · 10 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend as KDF
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Spec
4
5# The clauses of src/crypto/kdf.bend (HKDF-SHA256), proved in proof.bend.
6# Every clause is for every salt, key material, info and length.
7
8# The specification's partial expand, as the implementation's result type.
9def as_result(m: Maybe<&2, List<&2, U32>>) -> Result<&2, &2, KDF.KdfError, List<&2, U32>>:
10  match m:
11    case None{}:
12      Fail{KDF.LengthTooLarge{}}
13    case Some{okm}:
14      Done{okm}
15
16# extract is RFC 5869 section 2.2 (HMAC-SHA256(salt, IKM)).
17law Extract.correct:
18  for +salt: List<&2, U32>
19  for +ikm: List<&2, U32>
20  {KDF.extract(salt, ikm) == Spec.extract(salt, ikm) : List<&2, U32>}
21
22# expand is RFC 5869 section 2.3, and fails exactly where it is undefined.
23law Expand.correct:
24  for +prk: List<&2, U32>
25  for +info: List<&2, U32>
26  for +len: Nat
27  {KDF.expand(prk, info, len) == as_result(Spec.expand(prk, info, len)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
28
29law Expand.done:
30  for +prk: List<&2, U32>
31  for +info: List<&2, U32>
32  for +len: Nat
33  for +h: {Nat.is_le(len, 8160n) == True{} : Bool}
34  {KDF.expand(prk, info, len) == Done{Spec.okm(prk, info, len)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
35
36law Expand.too_long:
37  for +prk: List<&2, U32>
38  for +info: List<&2, U32>
39  for +len: Nat
40  for +h: {Nat.is_le(len, 8160n) == False{} : Bool}
41  {KDF.expand(prk, info, len) == Fail{KDF.LengthTooLarge{}} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
42
43# The output has the requested length.
44law Expand.length:
45  for +prk: List<&2, U32>
46  for +info: List<&2, U32>
47  for +len: Nat
48  for +out: List<&2, U32>
49  for +h: {KDF.expand(prk, info, len) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
50  {List.length(&2, U32, out) == len : Nat}
51
52# A shorter output is a prefix of a longer one (same key and info).
53law Expand.prefix:
54  for +prk: List<&2, U32>
55  for +info: List<&2, U32>
56  for +a: Nat
57  for +b: Nat
58  for +out: List<&2, U32>
59  for +hab: {Nat.is_le(a, b) == True{} : Bool}
60  for +h: {KDF.expand(prk, info, b) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
61  {KDF.expand(prk, info, a) == Done{List.take(&2, U32, out, a)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
62
63# hkdf is extract then expand.
64law Hkdf.correct:
65  for +salt: List<&2, U32>
66  for +ikm: List<&2, U32>
67  for +info: List<&2, U32>
68  for +len: Nat
69  {KDF.hkdf(salt, ikm, info, len) == as_result(Spec.hkdf(salt, ikm, info, len)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
70
71# The specification's OKM (any length): L bytes, and prefixes of each other.
72law Okm.length:
73  for +prk: List<&2, U32>
74  for +info: List<&2, U32>
75  for +len: Nat
76  {List.length(&2, U32, Spec.okm(prk, info, len)) == len : Nat}
77
78law Okm.prefix:
79  for +prk: List<&2, U32>
80  for +info: List<&2, U32>
81  for +a: Nat
82  for +b: Nat
83  for +h: {Nat.is_le(a, b) == True{} : Bool}
84  {Spec.okm(prk, info, a) == List.take(&2, U32, Spec.okm(prk, info, b), a) : List<&2, U32>}