proofs/crypto/poly1305/laws.bend source

proofs/crypto/poly1305/laws.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../src/crypto/poly1305/poly1305.bend as Pimport ../../../spec/crypto/poly1305.bend as R# The Poly1305 clauses (proved in proof.bend).# The implementation's tag is the RFC 8439 tag, for every key and message# (keys of other lengths than 32 included: both read missing bytes as absent).law mac_correct:  for +key: List<&2, U32>  for +msg: List<&2, U32>  {P.mac(key, msg) == R.mac(key, msg) : List<&2, U32>}# The tag has 16 bytes.law mac_length:  for +key: List<&2, U32>  for +msg: List<&2, U32>  {List.length(&2, U32, R.mac(key, msg)) == 16n : Nat}# The specification's reduction is x mod (2^130 - 5), for every x# (2^130 written C.shift(130n, one) with one == 1, as the checker would# expand a closed 2^130 in unary).law modp_mod:  for +one: Nat  for +h1: {one == 1n : Nat}  for +x: Nat  {R.modp(x) == Nat.mod(x, Nat.sub(C.shift(130n, one), 5n)) : Nat}# The checked API: the tag for a 32-byte key, None for any other length.law poly1305_valid:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}  {P.poly1305(key, msg) == Some{R.mac(key, msg)} : Maybe<&2, List<&2, U32>>}law poly1305_invalid:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool}  {P.poly1305(key, msg) == None{} : Maybe<&2, List<&2, U32>>}# verify accepts the RFC tag under a 32-byte key ...law verify_accepts:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}  {P.verify(key, msg, R.mac(key, msg)) == True{} : Bool}# ... and rejects every other tag.law verify_rejects:  for +key: List<&2, U32>  for +msg: List<&2, U32>  for +tag: List<&2, U32>  for h: {tag != R.mac(key, msg) : List<&2, U32>}  {P.verify(key, msg, tag) == False{} : Bool}# The RFC's polynomial reading of the accumulator: absorbing the blocks# (reducing after every block) is evaluating the polynomial of the blocks at# r and reducing once mod 2^130 - 5 (2^130 written C.shift(130n, one)).law absorb_poly:  for +one: Nat  for +h1: {one == 1n : Nat}  for +bs: List<&2, List<&2, U32>>  for +r: Nat  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}# Hence the tag: ((poly(blocks, r) mod p) + s) mod 2^128, as 16 little-endian# bytes, with r the clamped first half of the key and s the second half.law mac_poly:  for +one: Nat  for +h1: {one == 1n : Nat}  for +key: List<&2, U32>  for +msg: List<&2, U32>  {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>}