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

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

12 imports

import Base
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/blake/blake2b/sized.bend as IH
import ../../../src/crypto/argon2/types.bend as A
import ../../../src/crypto/argon2/blamka.bend as G
import ../../../src/crypto/argon2/argon2.bend as I
import ../../../src/crypto/argon2/phc.bend as PH
import ../../../src/crypto/password.bend as PW
import ../../../spec/crypto/argon2/blamka.bend as SG
import ../../../spec/crypto/argon2/argon2.bend as SA
import ./phc.bend as PP
import ./password.bend as PWP

Laws

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

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.gb(a, b, c, d) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GB(a, b, c, d) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad}

GB, the multiplication-hardened BLAKE2b mixing (RFC 9106 section 3.6).

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

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.p(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.P(v) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

The permutation P.

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

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.compress(x, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.G(x, y) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

The compression function G (section 3.5), and its XOR form of later passes.

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

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+old:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.compress_xor(x, y, old) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.xor(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.G(x, y), old) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

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

@+nn:Nat -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.hash(nn, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hash(nn, bs) : List<&2, U32>}

BLAKE2b with an nn-byte digest, H' and H0 (sections 3.2, 3.3).

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

@+tl:Nat -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hprime(tl, x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hprime(tl, x) : List<&2, U32>}

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

@+p:Nat -> @+tl:Nat -> @+m:Nat -> @+t:Nat -> @+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.h0(p, tl, m, t, pw, salt, key, ad) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.h0(p, tl, m, t, pw, salt, key, ad) : List<&2, U32>}

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

@+w:Nat -> @+j1:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hw:{Nat.is_lt(w, Nat.pow(2n, k)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.rel(w, j1) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rel(w, j1) : Nat}

The reference index computation of section 3.4.1.2, for |W| < 2^32.

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

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+ctr:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.addresses(r, l, s, mm, t, ctr) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.addresses(r, l, s, mm, t, ctr) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

The address blocks of the data-independent segments.

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

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.fits(m, p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.argon2id(pw, salt, key, ad, t, m, p, tl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.argon2id(pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}

Argon2id: for every password, salt, secret, associated data and parameters whose memory fits this implementation (m' <= 2^23 blocks), the tag (or None) is the specification's.

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

@+m:Nat -> @+t:Nat -> @+p:Nat -> @+salt:List<&2, U32> -> @+hash:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(salt) == True{} : Bool} -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(hash) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.parse(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.format(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Phc{m, t, p, salt, hash})) == Some{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Phc{m, t, p, salt, hash}} : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.Phc>}

The PHC string parses back to its fields (bytes below 256).

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

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+params:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.Params -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(salt) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/password.verified(pw, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.hash_password(pw, salt, params)) == True{} : Bool}

A hash verifies with its password.

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

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+params:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.Params -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(salt) == True{} : Bool} -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/password.len(salt) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.salt_len(params) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/password.fresh(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.hash_password(pw, salt, params), params) == False{} : Bool}

A hash needs no rehash with its own parameters.

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

@+tl:Nat -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/password.len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hprime(tl, x)) == tl : Nat}

The tag has T bytes, each below 256.

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

@+tl:Nat -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hprime(tl, x)) == True{} : Bool}