1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/crypto/poly1305.bend as R 4 import ../../../spec/crypto/subtle.bend as SS 5 import ../../../src/crypto/subtle.bend as Subtle 6 import ../../../src/crypto/poly1305/poly1305.bend as P 7 import ../../lib/logic.bend as L 8 import ../subtle/word.bend as SW 9 import ./modp.bend as MP 10 import ./mac.bend as M 11 import ./laws.bend as Laws 12 import ./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 19 def Laws.mac_correct(key, msg): M.mac_correct(key, msg) 20 21 def Laws.mac_length(key, msg): M.mac_length(key, msg) 22 23 def 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 27 def 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 32 def 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 37 law 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 44 def 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 52 law 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 59 def 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 76 law 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 82 def 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 94 law equal_refl: 95 for +a: List<&2, U32> 96 {SS.equal(a, a) == True{} : Bool} 97 98 def 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 107 def 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 116 def 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 125 def 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 132 def Laws.absorb_poly(one, h1, bs, r): 133 PY.absorb_poly(one, h1, bs, r) 134 135 def 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))