proofs/crypto/argon2/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 136 lines · 15 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as IH
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as G
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/password.bend as PW
9import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
10import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as PWP
13
14# The contract of src/crypto/argon2 and src/crypto/password.bend (proved in
15# proof.bend): the implementation equals the RFC 9106 specification of
16# spec/crypto/argon2/ for every input, and the password facade round-trips.
17
18# GB, the multiplication-hardened BLAKE2b mixing (RFC 9106 section 3.6).
19law gb_correct:
20  for +a: T.Lane
21  for +b: T.Lane
22  for +c: T.Lane
23  for +d: T.Lane
24  {G.gb(a, b, c, d) == SG.GB(a, b, c, d) : T.Quad}
25
26# The permutation P.
27law p_correct:
28  for +v: T.State
29  {G.p(v) == SG.P(v) : T.State}
30
31# The compression function G (section 3.5), and its XOR form of later passes.
32law compress_correct:
33  for +x: A.Block
34  for +y: A.Block
35  {G.compress(x, y) == SG.G(x, y) : A.Block}
36
37law compress_xor_correct:
38  for +x: A.Block
39  for +y: A.Block
40  for +old: A.Block
41  {G.compress_xor(x, y, old) == SG.xor(SG.G(x, y), old) : A.Block}
42
43# BLAKE2b with an nn-byte digest, H' and H0 (sections 3.2, 3.3).
44law hash_correct:
45  for +nn: Nat
46  for +bs: List<&2, U32>
47  {IH.hash(nn, bs) == SA.hash(nn, bs) : List<&2, U32>}
48
49law hprime_correct:
50  for +tl: Nat
51  for +x: List<&2, U32>
52  {I.hprime(tl, x) == SA.hprime(tl, x) : List<&2, U32>}
53
54law h0_correct:
55  for +p: Nat
56  for +tl: Nat
57  for +m: Nat
58  for +t: Nat
59  for +pw: List<&2, U32>
60  for +salt: List<&2, U32>
61  for +key: List<&2, U32>
62  for +ad: List<&2, U32>
63  {I.h0(p, tl, m, t, pw, salt, key, ad) == SA.h0(p, tl, m, t, pw, salt, key, ad) : List<&2, U32>}
64
65# The reference index computation of section 3.4.1.2, for |W| < 2^32.
66law rel_correct:
67  for +w: Nat
68  for +j1: U32
69  for +k: Nat
70  for +hk: {Nat.is_le(k, 32n) == True{} : Bool}
71  for +hw: {Nat.is_lt(w, Nat.pow(2n, k)) == True{} : Bool}
72  {I.rel(w, j1) == SA.rel(w, j1) : Nat}
73
74# The address blocks of the data-independent segments.
75law addresses_correct:
76  for +r: Nat
77  for +l: Nat
78  for +s: Nat
79  for +mm: Nat
80  for +t: Nat
81  for +ctr: Nat
82  {I.addresses(r, l, s, mm, t, ctr) == SA.addresses(r, l, s, mm, t, ctr) : A.Block}
83
84# Argon2id: for every password, salt, secret, associated data and
85# parameters whose memory fits this implementation (m' <= 2^23 blocks), the
86# tag (or None) is the specification's.
87law argon2id_correct:
88  for +pw: List<&2, U32>
89  for +salt: List<&2, U32>
90  for +key: List<&2, U32>
91  for +ad: List<&2, U32>
92  for +t: Nat
93  for +m: Nat
94  for +p: Nat
95  for +tl: Nat
96  for +hf: {I.fits(m, p) == True{} : Bool}
97  {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>>}
98
99# The PHC string parses back to its fields (bytes below 256).
100law parse_format:
101  for +m: Nat
102  for +t: Nat
103  for +p: Nat
104  for +salt: List<&2, U32>
105  for +hash: List<&2, U32>
106  for +hs: {PP.ok(salt) == True{} : Bool}
107  for +hh: {PP.ok(hash) == True{} : Bool}
108  {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
109
110# A hash verifies with its password.
111law verify_hash:
112  for +pw: List<&2, U32>
113  for +salt: List<&2, U32>
114  for +params: PW.Params
115  for +hs: {PP.ok(salt) == True{} : Bool}
116  {PWP.verified(pw, PW.hash_password(pw, salt, params)) == True{} : Bool}
117
118# A hash needs no rehash with its own parameters.
119law rehash_hash:
120  for +pw: List<&2, U32>
121  for +salt: List<&2, U32>
122  for +params: PW.Params
123  for +hs: {PP.ok(salt) == True{} : Bool}
124  for +hl: {PWP.len(salt) == PW.salt_len(params) : Nat}
125  {PWP.fresh(PW.hash_password(pw, salt, params), params) == False{} : Bool}
126
127# The tag has T bytes, each below 256.
128law tag_length:
129  for +tl: Nat
130  for +x: List<&2, U32>
131  {PWP.len(I.hprime(tl, x)) == tl : Nat}
132
133law tag_bytes:
134  for +tl: Nat
135  for +x: List<&2, U32>
136  {PP.ok(I.hprime(tl, x)) == True{} : Bool}