proofs/crypto/poly1305/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 139 lines · 5 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as SS
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
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/crypto/subtle/word.bend as SW
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/modp.bend as MP
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as M
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws.bend as Laws
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/poly.bend as PY
13
14# Entry point: `bend proofs/crypto/poly1305/proof.bend` checks every clause of
15# laws.bend. The work is in value.bend (limb values), step.bend (one block),
16# modp.bend (the spec's reduction), final.bend (freeze, tag bytes) and
17# mac.bend (the accumulator against the spec, block by block).
18
19def Laws.mac_correct(key, msg): M.mac_correct(key, msg)
20
21def Laws.mac_length(key, msg): M.mac_length(key, msg)
22
23def Laws.modp_mod(one, h1, x):
24  Equal.trans(Nat, R.modp(x), Nat.mod(x, 1n+M.bpv(one)), Nat.mod(x, Nat.sub(C.shift(130n, one), 5n)), MP.modp_mod(one, h1, M.bpv(one), M.bp5(one, h1), x),
25    Equal.cong(Nat, Nat, z => Nat.mod(x, z), 1n+M.bpv(one), Nat.sub(C.shift(130n, one), 5n), Equal.sym(Nat, Nat.sub(C.shift(130n, one), 5n), 1n+M.bpv(one), M.pp_eq(one, h1, M.bpv(one), M.bp5(one, h1)))))
26
27def Laws.poly1305_valid(key, msg, h):
28  Equal.trans(Maybe<&2, List<&2, U32>>, P.poly1305(key, msg), Some{P.mac(key, msg)}, Some{R.mac(key, msg)},
29    Equal.cong(Bool, Maybe<&2, List<&2, U32>>, b => P.when(b, P.mac(key, msg)), P.has_key(key), True{}, h),
30    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, t => Some{t}, P.mac(key, msg), R.mac(key, msg), M.mac_correct(key, msg)))
31
32def Laws.poly1305_invalid(key, msg, h):
33  Equal.cong(Bool, Maybe<&2, List<&2, U32>>, b => P.when(b, P.mac(key, msg)), P.has_key(key), False{}, h)
34
35# ---- constant-time equality (after proofs/crypto/subtle/proof.bend) ----
36
37law step:
38  for +acc: U32
39  for +x: U32
40  for +y: U32
41  for +e: Bool
42  {Bool.and(U32.is_eq(U32.or(acc, U32.xor(x, y)), 0), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
43
44def step(acc, x, y, e):
45  %Equal.sym(Bool, U32.is_eq(U32.or(acc, U32.xor(x, y)), 0),
46    Bool.and(U32.is_eq(acc, 0), U32.is_eq(U32.xor(x, y), 0)), SW.u32_or_zero(acc, U32.xor(x, y))) :
47    {Bool.and(_, e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
48  %Equal.sym(Bool, U32.is_eq(U32.xor(x, y), 0), U32.is_eq(x, y), SW.u32_xor_zero(x, y)) :
49    {Bool.and(Bool.and(U32.is_eq(acc, 0), _), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
50  SW.and_assoc(U32.is_eq(acc, 0), U32.is_eq(x, y), e)
51
52law fold:
53  for +a: List<&2, U32>
54  for +b: List<&2, U32>
55  for +acc: U32
56  {Bool.and(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, b)), U32.is_eq(Subtle.diff(a, b, acc), 0)) ==
57    Bool.and(U32.is_eq(acc, 0), SS.equal(a, b)) : Bool}
58
59def fold(a, b, acc):
60  match a b:
61    case Nil{} Nil{}:
62      Equal.sym(Bool, Bool.and(U32.is_eq(acc, 0), True{}), U32.is_eq(acc, 0), SW.and_true(U32.is_eq(acc, 0)))
63    case Nil{} y <> ys:
64      Equal.sym(Bool, Bool.and(U32.is_eq(acc, 0), False{}), False{}, SW.and_false(U32.is_eq(acc, 0)))
65    case x <> xs Nil{}:
66      Equal.sym(Bool, Bool.and(U32.is_eq(acc, 0), False{}), False{}, SW.and_false(U32.is_eq(acc, 0)))
67    case x <> xs y <> ys:
68      +acc2 = U32.or(acc, U32.xor(x, y))
69      Equal.trans(Bool,
70        Bool.and(Nat.is_eq(List.length(&2, U32, xs), List.length(&2, U32, ys)), U32.is_eq(Subtle.diff(xs, ys, acc2), 0)),
71        Bool.and(U32.is_eq(acc2, 0), SS.equal(xs, ys)),
72        Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), SS.equal(xs, ys))),
73        fold(xs, ys, acc2),
74        step(acc, x, y, SS.equal(xs, ys)))
75
76law equal_sound:
77  for +a: List<&2, U32>
78  for +b: List<&2, U32>
79  for +h: {SS.equal(a, b) == True{} : Bool}
80  {a == b : List<&2, U32>}
81
82def equal_sound(a, b, h):
83  match a b:
84    case Nil{} Nil{}: {==}
85    case Nil{} y <> ys: Empty.absurd({Nil{} == y <> ys : List<&2, U32>}, L.false_true(h))
86    case x <> xs Nil{}: Empty.absurd({x <> xs == Nil{} : List<&2, U32>}, L.false_true(h))
87    case x <> xs y <> ys:
88      +exy = SW.u32_sound(x, y, L.and_left(U32.is_eq(x, y), SS.equal(xs, ys), h))
89      +et = equal_sound(xs, ys, L.and_right(U32.is_eq(x, y), SS.equal(xs, ys), h))
90      %et : {x <> xs == y <> _ : List<&2, U32>}
91      %exy : {x <> xs == _ <> xs : List<&2, U32>}
92      {==}
93
94law equal_refl:
95  for +a: List<&2, U32>
96  {SS.equal(a, a) == True{} : Bool}
97
98def equal_refl(a):
99  match a:
100    case Nil{}: {==}
101    case x <> xs:
102      %Equal.sym(Bool, U32.is_eq(x, x), True{}, SW.u32_refl(x)) : {Bool.and(_, SS.equal(xs, xs)) == True{} : Bool}
103      equal_refl(xs)
104
105# ---- verify ----
106
107def Laws.verify_accepts(key, msg, h):
108  +t = R.mac(key, msg)
109  +pm = P.mac(key, msg)
110  Equal.trans(Bool, P.verify(key, msg, t), SS.equal(pm, t), True{},
111    Equal.trans(Bool, P.verify(key, msg, t), Subtle.eq(pm, t), SS.equal(pm, t),
112      Equal.cong(Bool, Bool, b => Bool.and(b, Subtle.eq(pm, t)), P.has_key(key), True{}, h),
113      fold(pm, t, 0)),
114    Equal.trans(Bool, SS.equal(pm, t), SS.equal(t, t), True{}, Equal.cong(List<&2, U32>, Bool, l => SS.equal(l, t), pm, t, M.mac_correct(key, msg)), equal_refl(t)))
115
116def rej_c(+key: List<&2, U32>, +msg: List<&2, U32>, +tag: List<&2, U32>, h: {tag != R.mac(key, msg) : List<&2, U32>}, +c: Bool, +hc: {SS.equal(P.mac(key, msg), tag) == c : Bool}) -> {Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)) == False{} : Bool}:
117  match c:
118    case True{}:
119      Empty.absurd({Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)) == False{} : Bool},
120        h(Equal.trans(List<&2, U32>, tag, P.mac(key, msg), R.mac(key, msg), Equal.sym(List<&2, U32>, P.mac(key, msg), tag, equal_sound(P.mac(key, msg), tag, hc)), M.mac_correct(key, msg))))
121    case False{}:
122      Equal.trans(Bool, Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)), Bool.and(P.has_key(key), False{}), False{},
123        Equal.cong(Bool, Bool, b => Bool.and(P.has_key(key), b), SS.equal(P.mac(key, msg), tag), False{}, hc), SW.and_false(P.has_key(key)))
124
125def Laws.verify_rejects(key, msg, tag, h):
126  Equal.trans(Bool, P.verify(key, msg, tag), Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)), False{},
127    Equal.cong(Bool, Bool, b => Bool.and(P.has_key(key), b), Subtle.eq(P.mac(key, msg), tag), SS.equal(P.mac(key, msg), tag), fold(P.mac(key, msg), tag, 0)),
128    rej_c(key, msg, tag, h, SS.equal(P.mac(key, msg), tag), {==}))
129
130# ---- the polynomial
131
132def Laws.absorb_poly(one, h1, bs, r):
133  PY.absorb_poly(one, h1, bs, r)
134
135def Laws.mac_poly(one, h1, key, msg):
136  +r = R.le_num(R.clamp(R.prefix(16n, key)))
137  +s = R.le_num(R.prefix(16n, R.suffix(16n, key)))
138  +bs = R.blocks(List.length(&2, U32, msg), msg)
139  Equal.cong(Nat, List<&2, U32>, z => R.le_bytes(16n, Nat.add(z, s)), R.absorb(bs, r, 0n), Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)), PY.absorb_poly(one, h1, bs, r))