1	import Base
2	import ./argon2/argon2.bend as A2
3	import ./argon2/phc.bend as PHC
4	import ./subtle.bend as Subtle
5	
6	# Password hashing with Argon2id (RFC 9106, version 0x13), stored as PHC
7	# strings:
8	#
9	#   hash_password(pw, salt, params)   Some{"$argon2id$v=19$m=..,t=..,p=..$salt$hash"},
10	#                                     None when a parameter is out of range
11	#   hash_password_os(pw, params)      the same with a fresh random salt of
12	#                                     params' salt length (IO.random_u32)
13	#   verify_password(pw, encoded)      the password hashes to the encoded tag
14	#                                     (constant-time comparison, subtle.eq)
15	#   needs_rehash(encoded, params)     the string is not Argon2id v=19 with
16	#                                     exactly these parameters
17	#
18	# Passwords and salts are byte lists (U32 values below 256). Parameters are
19	# m (memory, KiB), t (passes), p (lanes), the tag length and the salt length
20	# in bytes. owasp() is OWASP's Argon2id recommendation (m = 19 MiB, t = 2,
21	# p = 1); rfc9106() is RFC 9106 section 4's second recommended option
22	# (m = 64 MiB, t = 3, p = 4); both with 16-byte salts and 32-byte tags.
23	
24	type Params is Data:
25	  Params{m: Nat, t: Nat, p: Nat, tag: Nat, salt: Nat}
26	
27	def owasp() -> Params:
28	  Params{19456n, 2n, 1n, 32n, 16n}
29	
30	def rfc9106() -> Params:
31	  Params{65536n, 3n, 4n, 32n, 16n}
32	
33	def len(xs: List<&2, U32>) -> Nat:
34	  List.length(&2, U32, xs)
35	
36	def encode(+m: Nat, +t: Nat, +p: Nat, +salt: List<&2, U32>, r: Maybe<&2, List<&2, U32>>) -> Maybe<&2, String>:
37	  match r:
38	    case None{}:
39	      None{}
40	    case Some{h}:
41	      Some{PHC.format(PHC.Phc{m, t, p, salt, h})}
42	
43	# The PHC string of Argon2id(pw, salt) with the parameters, or None when they
44	# are out of the RFC 9106 ranges (or m > 2^23 KiB, this implementation's limit).
45	def hash_password(+pw: List<&2, U32>, +salt: List<&2, U32>, params: Params) -> Maybe<&2, String>:
46	  match params:
47	    case Params{+m, +t, +p, +tag, s}:
48	      encode(m, t, p, salt, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tag))
49	
50	def verify_tag(+hash: List<&2, U32>, r: Maybe<&2, List<&2, U32>>) -> Bool:
51	  match r:
52	    case None{}:
53	      False{}
54	    case Some{tag}:
55	      Subtle.eq(tag, hash)
56	
57	def verify_phc(+pw: List<&2, U32>, x: PHC.Phc) -> Bool:
58	  match x:
59	    case PHC.Phc{+m, +t, +p, +salt, +hash}:
60	      verify_tag(hash, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, len(hash)))
61	
62	def verify_parsed(+pw: List<&2, U32>, r: Maybe<&2, PHC.Phc>) -> Bool:
63	  match r:
64	    case None{}:
65	      False{}
66	    case Some{x}:
67	      verify_phc(pw, x)
68	
69	# The password matches the encoded Argon2id hash.
70	def verify_password(+pw: List<&2, U32>, encoded: String) -> Bool:
71	  verify_parsed(pw, PHC.parse(encoded))
72	
73	def same(+x: PHC.Phc, params: Params) -> Bool:
74	  match x params:
75	    case PHC.Phc{+m, +t, +p, +salt, +hash} Params{+pm, +pt, +pp, +ptag, +psalt}:
76	      Bool.and(Bool.and(Nat.is_eq(m, pm), Bool.and(Nat.is_eq(t, pt), Nat.is_eq(p, pp))), Bool.and(Nat.is_eq(len(hash), ptag), Nat.is_eq(len(salt), psalt)))
77	
78	def rehash_parsed(r: Maybe<&2, PHC.Phc>, params: Params) -> Bool:
79	  match r:
80	    case None{}:
81	      True{}
82	    case Some{x}:
83	      Bool.not(same(x, params))
84	
85	# The encoded hash should be recomputed: it is not an Argon2id v=19 PHC string
86	# with exactly these memory, passes, lanes, tag and salt lengths.
87	def needs_rehash(encoded: String, params: Params) -> Bool:
88	  rehash_parsed(PHC.parse(encoded), params)
89	
90	# n bytes from the operating system's generator.
91	def random_bytes(n: Nat) -> IO(List<&2, U32>):
92	  match n:
93	    case 0n:
94	      IO.pure(List<&2, U32>, Nil{})
95	    case 1n+k:
96	      do IO<List<&2, U32>>:
97	        w : U32 <- IO.try(U32, IO.random_u32())
98	        rest : List<&2, U32> <- random_bytes(k)
99	        return U32.and(w, 255) <> rest
100	
101	def salt_len(+params: Params) -> Nat:
102	  match params:
103	    case Params{m, t, p, tag, s}:
104	      s
105	
106	# hash_password with a fresh salt of params' salt length from IO.random_u32.
107	def hash_password_os(+pw: List<&2, U32>, +params: Params) -> IO(Maybe<&2, String>):
108	  do IO<Maybe<&2, String>>:
109	    salt : List<&2, U32> <- random_bytes(salt_len(params))
110	    return hash_password(pw, salt, params)