proofs/crypto/ed25519/proof.bend
bend-collections-laws-crypto@1.0.0.0 · 170 lines · 21 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as SX
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as SHA
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/sign.bend as SG
13import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sign.bend as SS
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
15import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend as PRM
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as S3
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as BY
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend as TP
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC
22
23
24
25
26
27
28def v(+x: U32) -> Nat:
29 U32.to_nat(x)
30
31def pp1(+one: Nat) -> Nat:
32 PRM.pp_of(one)
33
34def ok(+n: Nat, +a: List<&2, U32>, +h: {FS.bytes_ok(n, a) == True{} : Bool}) -> {LM.okb(n, a, 255n) == True{} : Bool}:
35 LM.bytes_okb(n, a, h)
36
37def ell_m(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+S3.mmL(one) == SE.ell(one) : Nat}:
38 S3.ell_eq(one, h1)
39
40
41
42def scalar_reduce(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {FS.bytes_ok(64n, bs) == True{} : Bool}) -> SE.Scalar.reduce(one, h1, bs, hb):
43 +M = {1n+S3.mmL(one) : Nat}
44 Equal.trans(Nat, FS.value(ESC.reduce(bs)), Nat.mod(FS.value(bs), M), Nat.mod(FS.value(bs), SE.ell(one)), S3.reduce_m(one, h1, bs, LM.okb_lea(64n, bs, 255n, ok(64n, bs, hb))), Equal.cong(Nat, Nat, z => Nat.mod(FS.value(bs), z), M, SE.ell(one), ell_m(one, h1)))
45
46def below(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +h: {Nat.is_lt(x, SE.ell(one)) == True{} : Bool}) -> {Nat.is_lt(x, 1n+S3.mmL(one)) == True{} : Bool}:
47 L.subst(Nat, z => {Nat.is_lt(x, z) == True{} : Bool}, SE.ell(one), 1n+S3.mmL(one), Equal.sym(Nat, 1n+S3.mmL(one), SE.ell(one), ell_m(one, h1)), h)
48
49def scalar_mul_add(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +s: List<&2, U32>, +r: List<&2, U32>, +hk: {FS.tight(k) == True{} : Bool}, +hs: {FS.tight(s) == True{} : Bool}, +hr: {FS.tight(r) == True{} : Bool}, +hsl: {Nat.is_lt(FS.value(s), SE.ell(one)) == True{} : Bool}, +hrl: {Nat.is_lt(FS.value(r), SE.ell(one)) == True{} : Bool}) -> SE.Scalar.mul_add(one, h1, k, s, r, hk, hs, hr, hsl, hrl):
50 +M = {1n+S3.mmL(one) : Nat}
51 +X = Nat.add(FS.value(r), Nat.mul(FS.value(k), FS.value(s)))
52 +e = S3.mul_add_m(one, h1, k, s, r, LM.okb_lea(32n, k, 255n, ok(32n, k, hk)), ok(32n, s, hs), ok(32n, r, hr), below(one, h1, FS.value(s), hsl), below(one, h1, FS.value(r), hrl))
53 Equal.trans(Nat, FS.value(ESC.mul_add(k, s, r)), Nat.mod(X, M), Nat.mod(X, SE.ell(one)), e, Equal.cong(Nat, Nat, z => Nat.mod(X, z), M, SE.ell(one), ell_m(one, h1)))
54
55
56
57def ed_public(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> SE.Ed25519.public(one, h1, seed, hs):
58 +pp = pp1(one)
59 +P = {1n+pp : Nat}
60 +D = SE.dconst(one, P)
61 +h = H.sha512(seed)
62 +sh = SHA.sha512_bytes(seed)
63 +e1 = TP.public_rel(one, h1, pp, PRM.hP(one, h1), seed, D, PC.r_d(one, h1, pp, PRM.hP(one, h1), seed), PC.r_d2(one, h1, pp, PRM.hP(one, h1), seed), h, BY.sha_okb(seed))
64 +e2 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.public_of(one, P, D, z), h, sh, BY.sha_eq(seed))
65 +e12 = Equal.trans(List<&2, U32>, E.public_key(seed), SE.public_of(one, P, D, h), SE.public_key_at(one, P, seed), e1, e2)
66 L.subst(Nat, z => {E.public_key(seed) == SE.public_key_at(one, z, seed) : List<&2, U32>}, P, FS.prime(one), Equal.sym(Nat, FS.prime(one), P, PRM.prime_eq(one, h1)), e12)
67
68def ed_sign(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> SE.Ed25519.sign(one, h1, seed, msg, hs):
69 +pp = pp1(one)
70 +P = {1n+pp : Nat}
71 +D = SE.dconst(one, P)
72 +h = H.sha512(seed)
73 +sh = SHA.sha512_bytes(seed)
74 +e1 = TP.sign_rel(one, h1, pp, PRM.hP(one, h1), seed, D, PC.r_d(one, h1, pp, PRM.hP(one, h1), seed), PC.r_d2(one, h1, pp, PRM.hP(one, h1), seed), h, BY.sha_okb(seed), msg)
75 +e2 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.sign_with(one, P, D, z, msg), h, sh, BY.sha_eq(seed))
76 +e12 = Equal.trans(List<&2, U32>, E.sign_raw(seed, msg), SE.sign_with(one, P, D, h, msg), SE.sign_at(one, P, seed, msg), e1, e2)
77 L.subst(Nat, z => {E.sign_raw(seed, msg) == SE.sign_at(one, z, seed, msg) : List<&2, U32>}, P, FS.prime(one), Equal.sym(Nat, FS.prime(one), P, PRM.prime_eq(one, h1)), e12)
78
79def ed_verify(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +hp: {FS.tight(pk) == True{} : Bool}, +hg: {FS.bytes_ok(64n, sig) == True{} : Bool}) -> SE.Ed25519.verify(one, h1, pk, msg, sig, hp, hg):
80 +pp = pp1(one)
81 +P = {1n+pp : Nat}
82 +D = SE.dconst(one, P)
83 +el = SE.ell(one)
84 +cs = PT.consts(pk)
85 +hsig = ok(64n, sig, hg)
86 +rb = F.take(32n, sig)
87 +sb = F.drop(32n, sig)
88 +srb = SE.first(32n, sig)
89 +ssb = SE.rest(32n, sig)
90 +hrb = BY.take_okb(32n, 32n, sig, 255n, hsig)
91 +hsb = BY.drop_okb(32n, 32n, sig, 255n, hsig)
92 +lt = Nat.is_lt(FS.value(sb), el)
93 +slt = Nat.is_lt(FS.value(ssb), el)
94 +e0 = Equal.trans(Bool, ESC.lt_l(sb), Nat.is_lt(FS.value(sb), 1n+S3.mmL(one)), lt, S3.lt_l_m(one, h1, sb, hsb), Equal.cong(Nat, Bool, z => Nat.is_lt(FS.value(sb), z), 1n+S3.mmL(one), el, ell_m(one, h1)))
95 +e1 = Equal.cong(Bool, Bool, z => E.verify_with(cs, pk, msg, rb, sb, z), ESC.lt_l(sb), lt, e0)
96 +e2 = TP.verify_with_rel(one, h1, pp, PRM.hP(one, h1), pk, ok(32n, pk, hp), msg, rb, hrb, sb, hsb, lt)
97 +e3 = Equal.cong(List<&2, U32>, Bool, z => SE.verify_with(one, P, D, pk, msg, z, FS.value(sb), lt), rb, srb, BY.take_eq(32n, sig))
98 +e4 = Equal.cong(List<&2, U32>, Bool, z => SE.verify_with(one, P, D, pk, msg, srb, FS.value(z), Nat.is_lt(FS.value(z), el)), sb, ssb, BY.drop_eq(32n, sig))
99 +e5 = Equal.cong(Nat, Bool, z => SE.verify_with(one, z, SE.dconst(one, z), pk, msg, srb, FS.value(ssb), slt), P, FS.prime(one), Equal.sym(Nat, FS.prime(one), P, PRM.prime_eq(one, h1)))
100 +V0 = E.verify_with(cs, pk, msg, rb, sb, ESC.lt_l(sb))
101 +V1 = E.verify_with(cs, pk, msg, rb, sb, lt)
102 +V2 = SE.verify_with(one, P, D, pk, msg, rb, FS.value(sb), lt)
103 +V3 = SE.verify_with(one, P, D, pk, msg, srb, FS.value(sb), lt)
104 +V4 = SE.verify_with(one, P, D, pk, msg, srb, FS.value(ssb), slt)
105 +V5 = SE.verify_with(one, FS.prime(one), SE.dconst(one, FS.prime(one)), pk, msg, srb, FS.value(ssb), slt)
106 Equal.trans(Bool, V0, V1, V5, e1, Equal.trans(Bool, V1, V2, V5, e2, Equal.trans(Bool, V2, V3, V5, e3, Equal.trans(Bool, V3, V4, V5, e4, e5))))
107
108
109
110def valid_eq(+n: Nat, +xs: List<&2, U32>) -> {X.valid_bytes(n, xs) == FS.bytes_ok(n, xs) : Bool}:
111 match n xs:
112 case 0n Nil{}:
113 {==}
114 case 0n Con{y, yt}:
115 {==}
116 case 1n+m Nil{}:
117 {==}
118 case 1n+ +m Con{+y, +yt}:
119 +e1 = U.is_lt_nat(y, 256)
120 +e2 = valid_eq(m, yt)
121 Equal.trans(Bool, Bool.and(U32.is_lt(y, 256), X.valid_bytes(m, yt)), Bool.and(Nat.is_lt(v(y), 256n), X.valid_bytes(m, yt)), Bool.and(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt)), Equal.cong(Bool, Bool, z => Bool.and(z, X.valid_bytes(m, yt)), U32.is_lt(y, 256), Nat.is_lt(v(y), 256n), e1), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_lt(v(y), 256n), z), X.valid_bytes(m, yt), FS.bytes_ok(m, yt), e2))
122
123def keypair_if_eq(+seed: List<&2, U32>, +ok: Bool, +pk: List<&2, U32>, +hok: {ok == True{} : Bool}, +e: {E.public_key(seed) == pk : List<&2, U32>}) -> {SG.keypair_if(seed, ok) == Some{SG.Keypair{seed, pk}} : Maybe<&2, SG.Keypair>}:
124 match ok:
125 case True{}:
126 Equal.cong(List<&2, U32>, Maybe<&2, SG.Keypair>, z => Some{SG.Keypair{seed, z}}, E.public_key(seed), pk, e)
127 case False{}:
128 Empty.absurd({SG.keypair_if(seed, False{}) == Some{SG.Keypair{seed, pk}} : Maybe<&2, SG.Keypair>}, L.true_false(Equal.sym(Bool, False{}, True{}, hok)))
129
130def sign_if_eq(+sk: List<&2, U32>, +msg: List<&2, U32>, +ok: Bool, +S: List<&2, U32>, +hok: {ok == True{} : Bool}, +e: {E.sign_raw(sk, msg) == S : List<&2, U32>}) -> {SG.sign_if(sk, msg, ok) == Some{S} : Maybe<&2, List<&2, U32>>}:
131 match ok:
132 case True{}:
133 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, z => Some{z}, E.sign_raw(sk, msg), S, e)
134 case False{}:
135 Empty.absurd({SG.sign_if(sk, msg, False{}) == Some{S} : Maybe<&2, List<&2, U32>>}, L.true_false(Equal.sym(Bool, False{}, True{}, hok)))
136
137def verify_if_eq(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +ok: Bool, +V: Bool, +hok: {ok == True{} : Bool}, +e: {E.verify_raw(pk, msg, sig) == V : Bool}) -> {SG.verify_if(pk, msg, sig, ok) == V : Bool}:
138 match ok:
139 case True{}:
140 e
141 case False{}:
142 Empty.absurd({SG.verify_if(pk, msg, sig, False{}) == V : Bool}, L.true_false(Equal.sym(Bool, False{}, True{}, hok)))
143
144def valid_ok(+n: Nat, +xs: List<&2, U32>, +h: {FS.bytes_ok(n, xs) == True{} : Bool}) -> {X.valid_bytes(n, xs) == True{} : Bool}:
145 Equal.trans(Bool, X.valid_bytes(n, xs), FS.bytes_ok(n, xs), True{}, valid_eq(n, xs), h)
146
147def sign_keypair(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> SS.Sign.keypair(one, h1, seed, hs):
148 keypair_if_eq(seed, X.valid_bytes(32n, seed), SE.public_key(one, seed), valid_ok(32n, seed, hs), ed_public(one, h1, seed, hs))
149
150def sign_sign(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}) -> SS.Sign.sign(one, h1, sk, msg, hs):
151 sign_if_eq(sk, msg, X.valid_bytes(32n, sk), SE.sign(one, sk, msg), valid_ok(32n, sk, hs), ed_sign(one, h1, sk, msg, hs))
152
153def sign_verify(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +hp: {FS.tight(pk) == True{} : Bool}, +hg: {FS.bytes_ok(64n, sig) == True{} : Bool}) -> SS.Sign.verify(one, h1, pk, msg, sig, hp, hg):
154 verify_if_eq(pk, msg, sig, Bool.and(X.valid_bytes(32n, pk), X.valid_bytes(64n, sig)), SE.verify(one, pk, msg, sig), L.and_intro(X.valid_bytes(32n, pk), X.valid_bytes(64n, sig), valid_ok(32n, pk, hp), valid_ok(64n, sig, hg)), ed_verify(one, h1, pk, msg, sig, hp, hg))
155
156def sign_reject_seed(+seed: List<&2, U32>, +h: {FS.tight(seed) == False{} : Bool}) -> SS.Sign.reject_seed(seed, h):
157 %Equal.sym(Bool, X.valid_bytes(32n, seed), FS.bytes_ok(32n, seed), valid_eq(32n, seed)) : {SG.keypair_if(seed, _) == None{} : Maybe<&2, SG.Keypair>}
158 %Equal.sym(Bool, FS.tight(seed), False{}, h) : {SG.keypair_if(seed, _) == None{} : Maybe<&2, SG.Keypair>}
159 {==}
160
161def sign_reject_key(+sk: List<&2, U32>, +msg: List<&2, U32>, +h: {FS.tight(sk) == False{} : Bool}) -> SS.Sign.reject_key(sk, msg, h):
162 %Equal.sym(Bool, X.valid_bytes(32n, sk), FS.bytes_ok(32n, sk), valid_eq(32n, sk)) : {SG.sign_if(sk, msg, _) == None{} : Maybe<&2, List<&2, U32>>}
163 %Equal.sym(Bool, FS.tight(sk), False{}, h) : {SG.sign_if(sk, msg, _) == None{} : Maybe<&2, List<&2, U32>>}
164 {==}
165
166def sign_reject(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +h: {Bool.and(FS.tight(pk), FS.bytes_ok(64n, sig)) == False{} : Bool}) -> SS.Sign.reject(pk, msg, sig, h):
167 %Equal.sym(Bool, X.valid_bytes(32n, pk), FS.bytes_ok(32n, pk), valid_eq(32n, pk)) : {SG.verify_if(pk, msg, sig, Bool.and(_, X.valid_bytes(64n, sig))) == False{} : Bool}
168 %Equal.sym(Bool, X.valid_bytes(64n, sig), FS.bytes_ok(64n, sig), valid_eq(64n, sig)) : {SG.verify_if(pk, msg, sig, Bool.and(FS.bytes_ok(32n, pk), _)) == False{} : Bool}
169 %Equal.sym(Bool, Bool.and(FS.tight(pk), FS.bytes_ok(64n, sig)), False{}, h) : {SG.verify_if(pk, msg, sig, _) == False{} : Bool}
170 {==}