proofs/crypto/poly1305/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 75 lines · 9 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/src/crypto/poly1305/poly1305.bend as P
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
5
6# The Poly1305 clauses (proved in proof.bend).
7
8# The implementation's tag is the RFC 8439 tag, for every key and message
9# (keys of other lengths than 32 included: both read missing bytes as absent).
10law mac_correct:
11  for +key: List<&2, U32>
12  for +msg: List<&2, U32>
13  {P.mac(key, msg) == R.mac(key, msg) : List<&2, U32>}
14
15# The tag has 16 bytes.
16law mac_length:
17  for +key: List<&2, U32>
18  for +msg: List<&2, U32>
19  {List.length(&2, U32, R.mac(key, msg)) == 16n : Nat}
20
21# The specification's reduction is x mod (2^130 - 5), for every x
22# (2^130 written C.shift(130n, one) with one == 1, as the checker would
23# expand a closed 2^130 in unary).
24law modp_mod:
25  for +one: Nat
26  for +h1: {one == 1n : Nat}
27  for +x: Nat
28  {R.modp(x) == Nat.mod(x, Nat.sub(C.shift(130n, one), 5n)) : Nat}
29
30# The checked API: the tag for a 32-byte key, None for any other length.
31law poly1305_valid:
32  for +key: List<&2, U32>
33  for +msg: List<&2, U32>
34  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}
35  {P.poly1305(key, msg) == Some{R.mac(key, msg)} : Maybe<&2, List<&2, U32>>}
36
37law poly1305_invalid:
38  for +key: List<&2, U32>
39  for +msg: List<&2, U32>
40  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool}
41  {P.poly1305(key, msg) == None{} : Maybe<&2, List<&2, U32>>}
42
43# verify accepts the RFC tag under a 32-byte key ...
44law verify_accepts:
45  for +key: List<&2, U32>
46  for +msg: List<&2, U32>
47  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}
48  {P.verify(key, msg, R.mac(key, msg)) == True{} : Bool}
49
50# ... and rejects every other tag.
51law verify_rejects:
52  for +key: List<&2, U32>
53  for +msg: List<&2, U32>
54  for +tag: List<&2, U32>
55  for h: {tag != R.mac(key, msg) : List<&2, U32>}
56  {P.verify(key, msg, tag) == False{} : Bool}
57
58# The RFC's polynomial reading of the accumulator: absorbing the blocks
59# (reducing after every block) is evaluating the polynomial of the blocks at
60# r and reducing once mod 2^130 - 5 (2^130 written C.shift(130n, one)).
61law absorb_poly:
62  for +one: Nat
63  for +h1: {one == 1n : Nat}
64  for +bs: List<&2, List<&2, U32>>
65  for +r: Nat
66  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}
67
68# Hence the tag: ((poly(blocks, r) mod p) + s) mod 2^128, as 16 little-endian
69# bytes, with r the clamped first half of the key and s the second half.
70law mac_poly:
71  for +one: Nat
72  for +h1: {one == 1n : Nat}
73  for +key: List<&2, U32>
74  for +msg: List<&2, U32>
75  {R.poly1305_mac(key, msg) == R.le_bytes(16n, Nat.add(Nat.mod(R.poly(R.blocks(List.length(&2, U32, msg), msg), R.le_num(R.clamp(R.prefix(16n, key)))), Nat.sub(C.shift(130n, one), 5n)), R.le_num(R.prefix(16n, R.suffix(16n, key))))) : List<&2, U32>}