1	import Base
2	import ../../../src/crypto/blake/blake2b/types.bend as T
3	import ../../../src/crypto/blake/blake2b/sized.bend as IH
4	import ../../../src/crypto/argon2/types.bend as A
5	import ../../../src/crypto/argon2/blamka.bend as G
6	import ../../../src/crypto/argon2/argon2.bend as I
7	import ../../../src/crypto/argon2/phc.bend as PH
8	import ../../../src/crypto/password.bend as PW
9	import ../../../spec/crypto/argon2/blamka.bend as SG
10	import ../../../spec/crypto/argon2/argon2.bend as SA
11	import ./phc.bend as PP
12	import ./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).
19	law 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.
27	law 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.
32	law compress_correct:
33	  for +x: A.Block
34	  for +y: A.Block
35	  {G.compress(x, y) == SG.G(x, y) : A.Block}
36	
37	law 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).
44	law 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	
49	law 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	
54	law 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.
66	law 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.
75	law 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.
87	law 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).
100	law 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.
111	law 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.
119	law 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.
128	law tag_length:
129	  for +tl: Nat
130	  for +x: List<&2, U32>
131	  {PWP.len(I.hprime(tl, x)) == tl : Nat}
132	
133	law tag_bytes:
134	  for +tl: Nat
135	  for +x: List<&2, U32>
136	  {PP.ok(I.hprime(tl, x)) == True{} : Bool}