proofs/crypto/kdf/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 99 lines · 9 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/src/crypto/mac.bend as MAC
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Spec
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as HMAC
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as MacP
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/okm.bend as O
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/laws.bend as Laws
11
12# Gate for src/crypto/kdf.bend: `bend proofs/crypto/kdf/proof.bend`.
13# The block chain and OKM lemmas are in okm.bend.
14
15def is_done(r: Result<&2, &2, KDF.KdfError, List<&2, U32>>) -> Bool:
16  match r:
17    case Fail{e}:
18      False{}
19    case Done{x}:
20      True{}
21
22def value(r: Result<&2, &2, KDF.KdfError, List<&2, U32>>) -> List<&2, U32>:
23  match r:
24    case Fail{e}:
25      Nil{}
26    case Done{x}:
27      x
28
29def fail_done(+e: KDF.KdfError, +x: List<&2, U32>, +h: {Fail{e} == Done{x} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}) -> Empty:
30  L.false_true(Equal.cong(Result<&2, &2, KDF.KdfError, List<&2, U32>>, Bool, is_done, Fail{e}, Done{x}, h))
31
32def done_inj(+x: List<&2, U32>, +y: List<&2, U32>, +h: {Done{x} == Done{y} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}) -> {x == y : List<&2, U32>}:
33  Equal.cong(Result<&2, &2, KDF.KdfError, List<&2, U32>>, List<&2, U32>, value, Done{x}, Done{y}, h)
34
35def done_cong(+x: List<&2, U32>, +y: List<&2, U32>, +h: {x == y : List<&2, U32>}) -> {Done{x} == Done{y} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}:
36  %h : {Done{x} == Done{_} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
37  {==}
38
39def Laws.Extract.correct(salt, ikm):
40  MacP.sign_correct(salt, ikm)
41
42def expand_if(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, +b: Bool) -> {KDF.expand_if(prk, info, len, b) == Laws.as_result(Spec.expand_if(prk, info, len, b)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}:
43  match b:
44    case True{}:
45      done_cong(KDF.blocks(len, prk, info, Nil{}, 1), Spec.okm(prk, info, len), O.okm_correct(prk, info, len))
46    case False{}:
47      {==}
48
49def Laws.Expand.correct(prk, info, len):
50  expand_if(prk, info, len, Nat.is_le(len, 8160n))
51
52def Laws.Expand.done(prk, info, len, h):
53  %Equal.sym(Bool, Nat.is_le(len, 8160n), True{}, h) : {KDF.expand_if(prk, info, len, _) == Done{Spec.okm(prk, info, len)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
54  done_cong(KDF.blocks(len, prk, info, Nil{}, 1), Spec.okm(prk, info, len), O.okm_correct(prk, info, len))
55
56def Laws.Expand.too_long(prk, info, len, h):
57  %Equal.sym(Bool, Nat.is_le(len, 8160n), False{}, h) : {KDF.expand_if(prk, info, len, _) == Fail{KDF.LengthTooLarge{}} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
58  {==}
59
60# From expand's result: the length fits, and the value is the block stream.
61def done_ok(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, +out: List<&2, U32>, +b: Bool, +eb: {Nat.is_le(len, 8160n) == b : Bool}, +h: {KDF.expand_if(prk, info, len, b) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}) -> {Nat.is_le(len, 8160n) == True{} : Bool}:
62  match b:
63    case True{}:
64      eb
65    case False{}:
66      Empty.absurd({Nat.is_le(len, 8160n) == True{} : Bool}, fail_done(KDF.LengthTooLarge{}, out, h))
67
68def done_value(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, +out: List<&2, U32>, +b: Bool, +h: {KDF.expand_if(prk, info, len, b) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}) -> {KDF.blocks(len, prk, info, Nil{}, 1) == out : List<&2, U32>}:
69  match b:
70    case True{}:
71      done_inj(KDF.blocks(len, prk, info, Nil{}, 1), out, h)
72    case False{}:
73      Empty.absurd({KDF.blocks(len, prk, info, Nil{}, 1) == out : List<&2, U32>}, fail_done(KDF.LengthTooLarge{}, out, h))
74
75# out is the specification's OKM.
76def done_okm(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, +out: List<&2, U32>, +h: {KDF.expand(prk, info, len) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}) -> {Spec.okm(prk, info, len) == out : List<&2, U32>}:
77  Equal.trans(List<&2, U32>, Spec.okm(prk, info, len), KDF.blocks(len, prk, info, Nil{}, 1), out,
78    Equal.sym(List<&2, U32>, KDF.blocks(len, prk, info, Nil{}, 1), Spec.okm(prk, info, len), O.okm_correct(prk, info, len)),
79    done_value(prk, info, len, out, Nat.is_le(len, 8160n), h))
80
81def Laws.Expand.length(prk, info, len, out, h):
82  %done_okm(prk, info, len, out, h) : {List.length(&2, U32, _) == len : Nat}
83  O.okm_length(prk, info, len)
84
85def Laws.Expand.prefix(prk, info, a, b, out, hab, h):
86  +hb = done_ok(prk, info, b, out, Nat.is_le(b, 8160n), {==}, h)
87  %done_okm(prk, info, b, out, h) : {KDF.expand(prk, info, a) == Done{List.take(&2, U32, _, a)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
88  %Equal.sym(Result<&2, &2, KDF.KdfError, List<&2, U32>>, KDF.expand(prk, info, a), Done{Spec.okm(prk, info, a)}, Laws.Expand.done(prk, info, a, N.le_trans(a, b, 8160n, hab, hb))) : {_ == Done{List.take(&2, U32, Spec.okm(prk, info, b), a)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
89  done_cong(Spec.okm(prk, info, a), List.take(&2, U32, Spec.okm(prk, info, b), a), O.okm_prefix(prk, info, a, b, hab))
90
91def Laws.Hkdf.correct(salt, ikm, info, len):
92  %Equal.sym(List<&2, U32>, MAC.sign(salt, ikm), HMAC.hmac(salt, ikm), MacP.sign_correct(salt, ikm)) : {KDF.expand(_, info, len) == Laws.as_result(Spec.expand(HMAC.hmac(salt, ikm), info, len)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
93  Laws.Expand.correct(HMAC.hmac(salt, ikm), info, len)
94
95def Laws.Okm.length(prk, info, len):
96  O.okm_length(prk, info, len)
97
98def Laws.Okm.prefix(prk, info, a, b, h):
99  O.okm_prefix(prk, info, a, b, h)