proofs/crypto/argon2/password.bend checks

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

20 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/hash/hash.bend as HH
import ./words.bend as LW
import ../../math/typed/width.bend as WW
import ../../math/typed/shrn.bend as SR
import ../subtle/word.bend as SW
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/blake/blake2b/sized.bend as H
import ../../../src/crypto/argon2/argon2.bend as A2
import ../../../src/crypto/argon2/blamka.bend as G
import ../../../src/crypto/argon2/memory.bend as M
import ../../../src/crypto/argon2/phc.bend as PH
import ../../../src/crypto/password.bend as PW
import ../../../src/crypto/subtle.bend as Subtle
import ./phc.bend as PP

Definitions

def len source · line 28 · raw

@xs:List<&2, U32> -> Nat

def len_append source · line 31 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> {len(List.append(&2, U32, a, b)) == Nat.add(len(a), len(b)) : Nat}

def len_take source · line 38 · raw

@+xs:List<&2, U32> -> @+k:Nat -> @+h:{Nat.is_le(k, len(xs)) == True{} : Bool} -> {len(List.take(&2, U32, xs, k)) == k : Nat}

def chain_len source · line 49 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.chain_bytes(h)) == 64n : Nat}

def hash_len source · line 54 · raw

@+nn:Nat -> @+bs:List<&2, U32> -> @+h:{Nat.is_le(nn, 64n) == True{} : Bool} -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.hash(nn, bs)) == nn : Nat}

def hp_go_len source · line 59 · raw

@+n:Nat -> @+v:List<&2, U32> -> @+last:Nat -> @+hv:{len(v) == 64n : Nat} -> @+hl:{Nat.is_le(last, 64n) == True{} : Bool} -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hp_go(n, v, last)) == Nat.add(Nat.mul(1n+n, 32n), last) : Nat}

W1 || .. : 32 bytes per chained digest, then the last digest.

def lt96 source · line 75 · raw

@+q:Nat -> @+r:Nat -> @+hq:{Nat.is_lt(q, 3n) == True{} : Bool} -> @+hr:{Nat.is_lt(r, 32n) == True{} : Bool} -> {Nat.is_lt(Nat.add(Nat.mul(q, 32n), r), 96n) == True{} : Bool}

def ge96 source · line 86 · raw

@+tl:Nat -> @+h:{Nat.is_le(65n, tl) == True{} : Bool} -> {Nat.is_le(96n, Nat.add(tl, 31n)) == True{} : Bool}

def sub_cancel source · line 90 · raw

@+c:Nat -> @+m:Nat -> @+r:Nat -> {Nat.sub(Nat.add(c, Nat.add(m, r)), m) == Nat.add(c, r) : Nat}

def big source · line 94 · raw

@+tl:Nat -> @+q:Nat -> @+r:Nat -> @+e:{Nat.add(tl, 31n) == Nat.add(Nat.mul(q, 32n), r) : Nat} -> @+hr:{Nat.is_lt(r, 32n) == True{} : Bool} -> @+ht:{Nat.is_le(65n, tl) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 3n) == True{} : Bool} -> Empty

def long_len source · line 100 · raw

@+tl:Nat -> @+q:Nat -> @+r:Nat -> @+v:List<&2, U32> -> @+e:{Nat.add(tl, 31n) == Nat.add(Nat.mul(q, 32n), r) : Nat} -> @+hr:{Nat.is_lt(r, 32n) == True{} : Bool} -> @+ht:{Nat.is_le(65n, tl) == True{} : Bool} -> @+hv:{len(v) == 64n : Nat} -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hp_go(Nat.sub(Nat.sub(q, 2n), 1n), v, Nat.sub(tl, Nat.mul(32n, Nat.sub(q, 2n))))) == tl : Nat}

The long case of H': with Q = (T + 31) / 32, r = Q - 2 digests of 32 bytes and a last one of T - 32 r.

def pick_len source · line 119 · raw

@+tl:Nat -> @+x:List<&2, U32> -> @+short:Bool -> @+es:{Nat.is_le(tl, 64n) == short : Bool} -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hp_pick(tl, x, short)) == tl : Nat}

def hprime_len source · line 129 · raw

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

H'^T has T bytes.

def ok_append source · line 134 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(List.append(&2, U32, a, b)) == True{} : Bool}

def ok_take source · line 141 · raw

@+xs:List<&2, U32> -> @+k:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(List.take(&2, U32, xs, k)) == True{} : Bool}

def and255 source · line 150 · raw

@+w:U32 -> {Nat.is_lt(U32.to_nat(U32.and(w, 255)), 256n) == True{} : Bool}

def top8 source · line 153 · raw

@+w:U32 -> {Nat.is_lt(U32.to_nat(U32.shrn(w, 24n)), 256n) == True{} : Bool}

def le_ok source · line 158 · raw

@+w:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.le(w)) == True{} : Bool}

def lane_ok source · line 164 · raw

@+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.lane_bytes(l)) == True{} : Bool}

def chain_ok source · line 169 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.chain_bytes(h)) == True{} : Bool}

def hash_ok source · line 181 · raw

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

def hp_go_ok source · line 185 · raw

@+n:Nat -> @+v:List<&2, U32> -> @+last:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(v) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hp_go(n, v, last)) == True{} : Bool}

def pick_ok source · line 194 · raw

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

def hprime_ok source · line 203 · raw

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

Every byte of H'^T is below 256.

def tag_of source · line 208 · raw

@+ok:Bool -> @+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+tag:List<&2, U32> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.checked(ok, pw, salt, [], [], t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.run(pw, salt, [], [], t, m, p, tl) == tag : List<&2, U32>}

def run_arg source · line 216 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> List<&2, U32>

The bytes H' is applied to in run.

def run_ok source · line 221 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.run(pw, salt, [], [], t, m, p, tl)) == True{} : Bool}

def run_len source · line 224 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.run(pw, salt, [], [], t, m, p, tl)) == tl : Nat}

def tag_ok source · line 227 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+tag:List<&2, U32> -> @+er:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.argon2id(pw, salt, [], [], t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(tag) == True{} : Bool}

def tag_len source · line 231 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+tag:List<&2, U32> -> @+er:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.argon2id(pw, salt, [], [], t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>} -> {len(tag) == tl : Nat}

def diff_self source · line 237 · raw

@+a:List<&2, U32> -> @+acc:U32 -> @+h:{U32.is_eq(acc, 0) == True{} : Bool} -> {U32.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/subtle.diff(a, a, acc), 0) == True{} : Bool}

def eq_refl source · line 248 · raw

@+a:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/subtle.eq(a, a) == True{} : Bool}

subtle.eq(a, a) == True (proofs/crypto/subtle proves it too, as Eq.refl).

def verified source · line 254 · raw

@+pw:List<&2, U32> -> @r:Maybe<&2, String> -> Bool

The result of hash_password verifies (vacuously when it is None).

def fresh source · line 262 · raw

@r:Maybe<&2, String> -> @+params:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.Params -> Bool

The result of hash_password does not need a rehash (vacuously when None).

def enc_ver source · line 269 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+m:Nat -> @+t:Nat -> @+p:Nat -> @+tl:Nat -> @+r:Maybe<&2, List<&2, U32>> -> @+er:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.argon2id(pw, salt, [], [], t, m, p, tl) == r : Maybe<&2, List<&2, U32>>} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(salt) == True{} : Bool} -> {verified(pw, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.encode(m, t, p, salt, r)) == True{} : Bool}

def verify_hash source · line 281 · 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} -> {verified(pw, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.hash_password(pw, salt, params)) == True{} : Bool}

verify_password(pw, hash_password(pw, salt, params)) == True whenever hash_password returns a string, for every salt of bytes below 256.

def enc_fresh source · line 286 · raw

@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+m:Nat -> @+t:Nat -> @+p:Nat -> @+tl:Nat -> @+sl:Nat -> @+r:Maybe<&2, List<&2, U32>> -> @+er:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.argon2id(pw, salt, [], [], t, m, p, tl) == r : Maybe<&2, List<&2, U32>>} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.ok(salt) == True{} : Bool} -> @+hl:{len(salt) == sl : Nat} -> {fresh(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.encode(m, t, p, salt, r), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.Params{m, t, p, tl, sl}) == False{} : Bool}

def rehash_hash source · line 304 · 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:{len(salt) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.salt_len(params) : Nat} -> {fresh(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.hash_password(pw, salt, params), params) == False{} : Bool}

needs_rehash(hash_password(pw, salt, params), params) == False whenever hash_password returns a string, for every salt of bytes below 256 with the parameters' salt length.