spec/crypto/poly1305.bend

bend-collections@1.0.0.0 · 142 lines · 19 definitions

1import Base
2import bend-collections@1.0.0.0/spec/lib/common.bend as C
3
4# Specification of the Poly1305 one-time authenticator (RFC 8439 section
5# 2.5), transcribed from the RFC's pseudocode over natural numbers. Nothing
6# is shared with the implementation (src/crypto/poly1305/): the accumulator
7# is one Nat reduced mod p = 2^130 - 5 after every block, as in HACL*'s
8# Spec.Poly1305. Numbers are little-endian byte strings; a byte is the low 8
9# bits of a U32. Multiplication by 256 is written C.shift(8n, x) (eight
10# doublings, spec/lib/common.bend).
11#
12# The proof checker expands a closed Nat in unary, so 2^130 is never formed
13# (as spec/math/w64.bend never forms 2^64): "x mod p" is modp(x) below, which
14# uses only 2^130 = p + 5 through C.low / C.high (k halvings). That modp(x)
15# is Nat.mod(x, 2^130 - 5) is proved for every x in
16# proofs/crypto/poly1305/modp.bend (law modp_mod, stated with 2^130 written
17# C.shift(130n, one) for a variable one = 1). p() below is the constant,
18# for the reader; no proof unfolds it.
19#
20# Bend's native runtime keeps a Nat below 2^48, so this specification is a
21# proof object; tools/check_poly1305.py runs a line-by-line mirror of it.
22
23# p = 2^130 - 5
24def p() -> Nat:
25  Nat.sub(C.pow2(130n), 5n)
26
27# x = lo + 2^130 hi is congruent to lo + 5 hi mod p (2^130 = p + 5); the fold
28# strictly decreases x while hi > 0, so x folds bring x below 2^130.
29def fold(+x: Nat) -> Nat:
30  Nat.add(C.low(130n, x), Nat.mul(C.high(130n, x), 5n))
31
32def folds(n: Nat, x: Nat) -> Nat:
33  match n:
34    case 0n: x
35    case 1n+k: folds(k, fold(x))
36
37def pick(b: Bool, x: Nat, y: Nat) -> Nat:
38  match b:
39    case True{}: x
40    case False{}: y
41
42# y < 2^130: y itself when y < p, else y - p = (y + 5) - 2^130.
43def canon(+y: Nat) -> Nat:
44  match y:
45    case 0n: 0n
46    case 1n+z: pick(C.fits(130n, Nat.add(1n+z, 5n)), 1n+z, C.low(130n, Nat.add(1n+z, 5n)))
47
48# x mod p
49def modp(+x: Nat) -> Nat:
50  canon(folds(x, x))
51
52# le_bytes_to_num
53def le_num(bytes: List<&2, U32>) -> Nat:
54  match bytes:
55    case Nil{}: 0n
56    case b <> rest: Nat.add(U32.to_nat(U32.and(b, 255)), C.shift(8n, le_num(rest)))
57
58# num_to_n_le_bytes: the low n bytes of x.
59def le_bytes(n: Nat, +x: Nat) -> List<&2, U32>:
60  match n:
61    case 0n: Nil{}
62    case 1n+k: U32.from_nat(C.low(8n, x)) <> le_bytes(k, C.high(8n, x))
63
64def prefix(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
65  match n xs:
66    case 0n _: Nil{}
67    case 1n+k Nil{}: Nil{}
68    case 1n+k x <> rest: x <> prefix(k, rest)
69
70def suffix(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
71  match n xs:
72    case 0n _: xs
73    case 1n+k Nil{}: Nil{}
74    case 1n+k x <> rest: suffix(k, rest)
75
76# clamp(r): r &= 0x0ffffffc0ffffffc0ffffffc0fffffff, i.e. r[3], r[7], r[11]
77# and r[15] keep their low four bits, r[4], r[8] and r[12] lose their low two.
78def clamp_mask(i: Nat) -> U32:
79  match i:
80    case 3n: 15
81    case 7n: 15
82    case 11n: 15
83    case 15n: 15
84    case 4n: 252
85    case 8n: 252
86    case 12n: 252
87    case _: 255
88
89def clamp_from(r: List<&2, U32>, +i: Nat) -> List<&2, U32>:
90  match r:
91    case Nil{}: Nil{}
92    case b <> rest: U32.and(b, clamp_mask(i)) <> clamp_from(rest, 1n+i)
93
94def clamp(r: List<&2, U32>) -> List<&2, U32>:
95  clamp_from(r, 0n)
96
97# The message cut into 16-byte blocks, the last one possibly shorter; fuel
98# bounds the number of blocks (the length of the message is enough).
99def blocks(fuel: Nat, +msg: List<&2, U32>) -> List<&2, List<&2, U32>>:
100  match fuel msg:
101    case 0n _: Nil{}
102    case 1n+k Nil{}: Nil{}
103    case 1n+k b <> rest: prefix(16n, b <> rest) <> blocks(k, suffix(16n, b <> rest))
104
105# for each block: n = le_bytes_to_num(block | [0x01]); a += n; a = (r * a) % p
106def absorb(bs: List<&2, List<&2, U32>>, +r: Nat, a: Nat) -> Nat:
107  match bs:
108    case Nil{}: a
109    case b <> rest:
110      +n = le_num(List.append(&2, U32, b, [1]))
111      absorb(rest, r, modp(Nat.mul(r, Nat.add(a, n))))
112
113# poly1305_mac(msg, key): r = clamp(key[0..16]), s = key[16..32];
114# a = 0, absorb every block, a += s; the tag is num_to_16_le_bytes(a).
115def poly1305_mac(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
116  +r = le_num(clamp(prefix(16n, key)))
117  +s = le_num(prefix(16n, suffix(16n, key)))
118  le_bytes(16n, Nat.add(absorb(blocks(List.length(&2, U32, msg), msg), r, 0n), s))
119
120# The same function, split on the message first so that a proof about an
121# unknown message does not unfold it.
122def mac(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
123  match msg:
124    case Nil{}: poly1305_mac(key, [])
125    case b <> rest: poly1305_mac(key, b <> rest)
126
127# ---------------------------------------------------------------- the polynomial
128
129# RFC 8439 2.5 describes the accumulator as the evaluation, at r and
130# modulo p, of the polynomial whose coefficients are the blocks (each with
131# its 0x01 byte): with q blocks n_1 .. n_q,
132#   poly(r) = n_1 r^q + n_2 r^(q-1) + ... + n_q r
133# (as Spec.Poly1305 in HACL* and the field statements of Mathlib's ZMod p).
134# Clause absorb_poly (proofs/crypto/poly1305/poly.bend) proves
135# absorb(blocks, r, 0) == poly(blocks, r) mod (2^130 - 5).
136def coeff(b: List<&2, U32>) -> Nat:
137  le_num(List.append(&2, U32, b, [1]))
138
139def poly(+bs: List<&2, List<&2, U32>>, +r: Nat) -> Nat:
140  match bs:
141    case Nil{}: 0n
142    case b <> rest: Nat.add(Nat.mul(coeff(b), Nat.pow(r, 1n+List.length(&2, List<&2, U32>, rest))), poly(rest, r))