src/crypto/password.bend

bend-collections-laws-crypto@1.0.0.0 · 110 lines · 16 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PHC
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/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
24type Params is Data:
25  Params{m: Nat, t: Nat, p: Nat, tag: Nat, salt: Nat}
26
27def owasp() -> Params:
28  Params{19456n, 2n, 1n, 32n, 16n}
29
30def rfc9106() -> Params:
31  Params{65536n, 3n, 4n, 32n, 16n}
32
33def len(xs: List<&2, U32>) -> Nat:
34  List.length(&2, U32, xs)
35
36def 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).
45def 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
50def 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
57def 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
62def 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.
70def verify_password(+pw: List<&2, U32>, encoded: String) -> Bool:
71  verify_parsed(pw, PHC.parse(encoded))
72
73def 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
78def 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.
87def needs_rehash(encoded: String, params: Params) -> Bool:
88  rehash_parsed(PHC.parse(encoded), params)
89
90# n bytes from the operating system's generator.
91def 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
101def 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.
107def 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)