hacspec_poly1305/
poly1305.rs

1use std::convert::TryInto;
2
3// WARNING:
4// This spec does not provide secret independence, and treats all keys as public.
5// Consequently, it should only be used as a FORMAL SPEC, NOT as a reference implementation.
6use hacspec_lib::hacspec_helper::*;
7
8// Type definitions for use in poly1305.
9pub type PolyKey = [u8; 32];
10
11const BLOCKSIZE: usize = 16;
12
13// These are type aliases for convenience
14pub type PolyBlock = [u8; 16];
15
16// These are actual types; fixed-length arrays.
17pub type Poly1305Tag = [u8; 16];
18
19// A byte sequence of length <= BLOCKSIZE
20pub type SubBlock = Vec<u8>;
21
22// A length <= BLOCKSIZE
23pub type BlockIndex = usize;
24
25// This defines the field for modulo 2^130-5.
26// In particular `FieldElement` is defined.
27// The `FieldElement` is a natural integer modulo 2^130-5.
28#[nat_mod("03fffffffffffffffffffffffffffffffb", 17)]
29pub struct FieldElement {}
30
31// Internal Poly1305 State
32pub type PolyState = (FieldElement, FieldElement, PolyKey); //(accumulator,r,key)
33
34pub fn poly1305_encode_r(b: &PolyBlock) -> FieldElement {
35    let mut n = u128::from_le_bytes(*b);
36    n &= 0x0fff_fffc_0fff_fffc_0fff_fffc_0fff_ffffu128;
37    FieldElement::from_u128(n)
38}
39
40pub fn poly1305_encode_block(b: &PolyBlock) -> FieldElement {
41    let n = u128::from_le_bytes(*b);
42    let f = FieldElement::from_u128(n);
43    f + FieldElement::pow2(128)
44}
45
46// In Poly1305 as used in this spec, pad_len is always the length of b, i.e. there is no padding
47// In Chacha20Poly1305, pad_len is set to BLOCKSIZE
48pub fn poly1305_encode_last(pad_len: BlockIndex, b: &SubBlock) -> FieldElement {
49    let mut bytes = [0u8; 16];
50    bytes[0..b.len()].copy_from_slice(b);
51    let n = u128::from_le_bytes(bytes);
52    let f = FieldElement::from_u128(n);
53    f + FieldElement::pow2(8 * pad_len)
54}
55
56pub fn poly1305_init(k: PolyKey) -> PolyState {
57    let r = poly1305_encode_r(&k[0..16].try_into().unwrap());
58    (FieldElement::zero(), r, k)
59}
60
61pub fn poly1305_update_block(b: &PolyBlock, st: PolyState) -> PolyState {
62    let (acc, r, k) = st;
63    ((poly1305_encode_block(b) + acc) * r, r, k)
64}
65
66pub fn poly1305_update_blocks(m: &[u8], st: PolyState) -> PolyState {
67    let mut st = st;
68    for block in m.chunks_exact(BLOCKSIZE) {
69        st = poly1305_update_block(block.try_into().unwrap(), st);
70    }
71    st
72}
73
74pub fn poly1305_update_last(pad_len: usize, b: &SubBlock, st: PolyState) -> PolyState {
75    let mut st = st;
76    if !b.is_empty() {
77        let (acc, r, k) = st;
78        st = ((poly1305_encode_last(pad_len, b) + acc) * r, r, k);
79    }
80    st
81}
82
83pub fn poly1305_update(m: &[u8], st: PolyState) -> PolyState {
84    let st = poly1305_update_blocks(m, st);
85    let mchunks = m.chunks_exact(BLOCKSIZE);
86    let last = mchunks.remainder();
87    poly1305_update_last(last.len(), &last.to_vec(), st)
88}
89
90pub fn poly1305_finish(st: PolyState) -> Poly1305Tag {
91    let (acc, _, k) = st;
92    let n = u128::from_le_bytes(k[16..32].try_into().unwrap());
93    let aby = acc.to_le_bytes();
94    // We can't use from_seq here because the accumulator is larger than 16 bytes.
95    let a = u128::from_le_bytes(aby[0..16].try_into().unwrap());
96    a.wrapping_add(n).to_le_bytes()
97}
98
99pub fn poly1305(m: &[u8], key: PolyKey) -> Poly1305Tag {
100    let mut st = poly1305_init(key);
101    st = poly1305_update(m, st);
102    poly1305_finish(st)
103}
hacspec_poly1305/poly1305.rs

hacspec_poly1305/
poly1305.rs
