1 import Base 2 import ../../../src/crypto/kdf.bend as KDF 3 import ../../../src/crypto/mac.bend as MAC 4 import ../../../spec/crypto/hkdf.bend as Spec 5 import ../../../spec/crypto/hmac.bend as HMAC 6 import ../mac/hmac.bend as MacP 7 import ../../lib/logic.bend as L 8 import ../../lib/nat.bend as N 9 import ./okm.bend as O 10 import ./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 15 def 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 22 def 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 29 def 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 32 def 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 35 def 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 39 def Laws.Extract.correct(salt, ikm): 40 MacP.sign_correct(salt, ikm) 41 42 def 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 49 def Laws.Expand.correct(prk, info, len): 50 expand_if(prk, info, len, Nat.is_le(len, 8160n)) 51 52 def 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 56 def 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. 61 def 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 68 def 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. 76 def 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 81 def 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 85 def 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 91 def 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 95 def Laws.Okm.length(prk, info, len): 96 O.okm_length(prk, info, len) 97 98 def Laws.Okm.prefix(prk, info, a, b, h): 99 O.okm_prefix(prk, info, a, b, h)