~/bend-docscommunity

proofs/crypto/poly1305/laws.bend open laws/TODOs

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws.bend as Laws

4 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../src/crypto/poly1305/poly1305.bend as P
import ../../../spec/crypto/poly1305.bend as R

Laws

law mac_correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 10 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.mac(key, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg) : List<&2, U32>}

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_length openits proof in laws_crypto.bend does not pass the checker (fails)source · line 16 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg)) == 16n : Nat}

The tag has 16 bytes.

law modp_mod openits proof in laws_crypto.bend does not pass the checker (fails)source · line 24 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.modp(x) == Nat.mod(x, Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one), 5n)) : 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 poly1305_valid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 31 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.poly1305(key, msg) == Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg)} : Maybe<&2, List<&2, U32>>}

The checked API: the tag for a 32-byte key, None for any other length.

law poly1305_invalid openits proof in laws_crypto.bend does not pass the checker (fails)source · line 37 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.poly1305(key, msg) == None{} : Maybe<&2, List<&2, U32>>}

law verify_accepts openits proof in laws_crypto.bend does not pass the checker (fails)source · line 44 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+h:{Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.verify(key, msg, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg)) == True{} : Bool}

verify accepts the RFC tag under a 32-byte key ...

law verify_rejects openits proof in laws_crypto.bend does not pass the checker (fails)source · line 51 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+tag:List<&2, U32> -> @h:(@_:{tag == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.verify(key, msg, tag) == False{} : Bool}

... and rejects every other tag.

law absorb_poly openits proof in laws_crypto.bend does not pass the checker (fails)source · line 61 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, List<&2, U32>> -> @+r:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.absorb(bs, r, 0n) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.poly(bs, r), Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one), 5n)) : Nat}

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 mac_poly openits proof in laws_crypto.bend does not pass the checker (fails)source · line 70 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+key:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.poly1305_mac(key, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_bytes(16n, Nat.add(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.poly(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.blocks(List.length(&2, U32, msg), msg), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_num(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.clamp(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.prefix(16n, key)))), Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one), 5n)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_num(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.prefix(16n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.suffix(16n, key))))) : List<&2, U32>}

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.