proofs/crypto/argon2/laws.bend source
proofs/crypto/argon2/laws.bend on the hub · documented module
import Baseimport ../../../src/crypto/blake/blake2b/types.bend as Timport ../../../src/crypto/blake/blake2b/sized.bend as IHimport ../../../src/crypto/argon2/types.bend as Aimport ../../../src/crypto/argon2/blamka.bend as Gimport ../../../src/crypto/argon2/argon2.bend as Iimport ../../../src/crypto/argon2/phc.bend as PHimport ../../../src/crypto/password.bend as PWimport ../../../spec/crypto/argon2/blamka.bend as SGimport ../../../spec/crypto/argon2/argon2.bend as SAimport ./phc.bend as PPimport ./password.bend as PWP# The contract of src/crypto/argon2 and src/crypto/password.bend (proved in# proof.bend): the implementation equals the RFC 9106 specification of# spec/crypto/argon2/ for every input, and the password facade round-trips.# GB, the multiplication-hardened BLAKE2b mixing (RFC 9106 section 3.6).law gb_correct: for +a: T.Lane for +b: T.Lane for +c: T.Lane for +d: T.Lane {G.gb(a, b, c, d) == SG.GB(a, b, c, d) : T.Quad}# The permutation P.law p_correct: for +v: T.State {G.p(v) == SG.P(v) : T.State}# The compression function G (section 3.5), and its XOR form of later passes.law compress_correct: for +x: A.Block for +y: A.Block {G.compress(x, y) == SG.G(x, y) : A.Block}law compress_xor_correct: for +x: A.Block for +y: A.Block for +old: A.Block {G.compress_xor(x, y, old) == SG.xor(SG.G(x, y), old) : A.Block}# BLAKE2b with an nn-byte digest, H' and H0 (sections 3.2, 3.3).law hash_correct: for +nn: Nat for +bs: List<&2, U32> {IH.hash(nn, bs) == SA.hash(nn, bs) : List<&2, U32>}law hprime_correct: for +tl: Nat for +x: List<&2, U32> {I.hprime(tl, x) == SA.hprime(tl, x) : List<&2, U32>}law h0_correct: for +p: Nat for +tl: Nat for +m: Nat for +t: Nat for +pw: List<&2, U32> for +salt: List<&2, U32> for +key: List<&2, U32> for +ad: List<&2, U32> {I.h0(p, tl, m, t, pw, salt, key, ad) == SA.h0(p, tl, m, t, pw, salt, key, ad) : List<&2, U32>}# The reference index computation of section 3.4.1.2, for |W| < 2^32.law rel_correct: for +w: Nat for +j1: U32 for +k: Nat for +hk: {Nat.is_le(k, 32n) == True{} : Bool} for +hw: {Nat.is_lt(w, Nat.pow(2n, k)) == True{} : Bool} {I.rel(w, j1) == SA.rel(w, j1) : Nat}# The address blocks of the data-independent segments.law addresses_correct: for +r: Nat for +l: Nat for +s: Nat for +mm: Nat for +t: Nat for +ctr: Nat {I.addresses(r, l, s, mm, t, ctr) == SA.addresses(r, l, s, mm, t, ctr) : A.Block}# 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 argon2id_correct: for +pw: List<&2, U32> for +salt: List<&2, U32> for +key: List<&2, U32> for +ad: List<&2, U32> for +t: Nat for +m: Nat for +p: Nat for +tl: Nat for +hf: {I.fits(m, p) == True{} : Bool} {I.argon2id(pw, salt, key, ad, t, m, p, tl) == SA.argon2id(pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}# The PHC string parses back to its fields (bytes below 256).law parse_format: for +m: Nat for +t: Nat for +p: Nat for +salt: List<&2, U32> for +hash: List<&2, U32> for +hs: {PP.ok(salt) == True{} : Bool} for +hh: {PP.ok(hash) == True{} : Bool} {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}# A hash verifies with its password.law verify_hash: for +pw: List<&2, U32> for +salt: List<&2, U32> for +params: PW.Params for +hs: {PP.ok(salt) == True{} : Bool} {PWP.verified(pw, PW.hash_password(pw, salt, params)) == True{} : Bool}# A hash needs no rehash with its own parameters.law rehash_hash: for +pw: List<&2, U32> for +salt: List<&2, U32> for +params: PW.Params for +hs: {PP.ok(salt) == True{} : Bool} for +hl: {PWP.len(salt) == PW.salt_len(params) : Nat} {PWP.fresh(PW.hash_password(pw, salt, params), params) == False{} : Bool}# The tag has T bytes, each below 256.law tag_length: for +tl: Nat for +x: List<&2, U32> {PWP.len(I.hprime(tl, x)) == tl : Nat}law tag_bytes: for +tl: Nat for +x: List<&2, U32> {PP.ok(I.hprime(tl, x)) == True{} : Bool}