
   0 | module Text.Crypt
   1 | 
   2 | import public Data.DPair
   3 | 
   4 | %default total
   5 | 
   6 | --------------------------------------------------------------------------------
   7 | --          FFI Bindings
   8 | --------------------------------------------------------------------------------
   9 | 
  10 | %foreign "C:idris_gensalt,libcrypt-idris"
  11 | prim__gensalt : String -> Bits32 -> PrimIO String
  12 | 
  13 | %foreign "C:idris_crypt,libcrypt-idris"
  14 | prim__crypt : String -> String -> String
  15 | 
  16 | %foreign "C:idris_checksalt,libcrypt-idris"
  17 | prim__checksalt : String -> Int
  18 | 
  19 | %foreign "C:idris_checkphrase,libcrypt-idris"
  20 | prim__checkphrase : String -> Int
  21 | 
  22 | %foreign "C:idris_crypt_check,libcrypt-idris"
  23 | prim__cryptcheck : String -> String -> Int
  24 | 
  25 | --------------------------------------------------------------------------------
  26 | --          Types
  27 | --------------------------------------------------------------------------------
  28 | 
  29 | ||| Quality of a salt/setting string to be used for hashing
  30 | ||| a passphrase. This can also be the prefix of an already
  31 | ||| encrypted string. `Legacy` means that the settings are
  32 | ||| no longer considered to be strong enough and their usage
  33 | ||| is discouraged.
  34 | public export
  35 | data SaltQuality = OK | Invalid | Legacy
  36 | 
  37 | public export
  38 | Eq SaltQuality where
  39 |   OK      == OK      = True
  40 |   Invalid == Invalid = True
  41 |   Legacy  == Legacy  = True
  42 |   _       == _       = False
  43 | 
  44 | export
  45 | Show SaltQuality where
  46 |   show OK      = "OK"
  47 |   show Invalid = "Invalid"
  48 |   show Legacy  = "Legacy"
  49 | 
  50 | public export
  51 | data CryptMethod =
  52 |     YesCrypt
  53 |   | GhostYesCrypt
  54 |   | SCrypt
  55 |   | BCrypt
  56 |   | SHA512Crypt
  57 |   | SHA256Crypt
  58 | 
  59 | public export
  60 | Eq CryptMethod where
  61 |   YesCrypt      == YesCrypt      = True
  62 |   GhostYesCrypt == GhostYesCrypt = True
  63 |   SCrypt        == SCrypt        = True
  64 |   BCrypt        == BCrypt        = True
  65 |   SHA512Crypt   == SHA512Crypt   = True
  66 |   SHA256Crypt   == SHA256Crypt   = True
  67 |   _             == _             = False
  68 | 
  69 | export
  70 | Show CryptMethod where
  71 |   show YesCrypt      = "YesCrypt"
  72 |   show GhostYesCrypt = "GhostYesCrypt"
  73 |   show SCrypt        = "SCrypt"
  74 |   show BCrypt        = "BCrypt"
  75 |   show SHA512Crypt   = "SHA512Crypt"
  76 |   show SHA256Crypt   = "SHA256Crypt"
  77 | 
  78 | export
  79 | cryptPrefix : CryptMethod -> String
  80 | cryptPrefix YesCrypt      = "$y$"
  81 | cryptPrefix GhostYesCrypt = "$gy$"
  82 | cryptPrefix SCrypt        = "$7$"
  83 | cryptPrefix BCrypt        = "$2b$"
  84 | cryptPrefix SHA512Crypt   = "$6$"
  85 | cryptPrefix SHA256Crypt   = "$5$"
  86 | 
  87 | ||| Minimal computational cost to specify when using
  88 | ||| the given hashing method. The `cost` parameter
  89 | ||| in the `gensalt` method should be in the range
  90 | ||| `[MinCost c, MaxCost c]`, where `c` is the hashing method
  91 | ||| (`CryptMethod`) to be used.
  92 | public export
  93 | MinCost : CryptMethod -> Bits32
  94 | MinCost YesCrypt      = 1
  95 | MinCost GhostYesCrypt = 1
  96 | MinCost SCrypt        = 6
  97 | MinCost BCrypt        = 4
  98 | MinCost SHA512Crypt   = 1000
  99 | MinCost SHA256Crypt   = 1000
 100 | 
 101 | ||| Maximal computational cost to specify when using
 102 | ||| the given hashing method. The `cost` parameter
 103 | ||| in the `gensalt` method should be in the range
 104 | ||| `[MinCost c, MaxCost c]`, where `c` is the hashing method
 105 | ||| (`CryptMethod`) to be used.
 106 | public export
 107 | MaxCost : CryptMethod -> Bits32
 108 | MaxCost YesCrypt      = 11
 109 | MaxCost GhostYesCrypt = 11
 110 | MaxCost SCrypt        = 11
 111 | MaxCost BCrypt        = 31
 112 | MaxCost SHA512Crypt   = 999999999
 113 | MaxCost SHA256Crypt   = 999999999
 114 | 
 115 | ||| Proof that the given computational cost is a valid
 116 | ||| value for the given hashing method
 117 | public export
 118 | 0 InRange : CryptMethod -> (cost : Bits32) -> Type
 119 | InRange cm c = (MinCost cm <= c && c <= MaxCost cm) === True
 120 | 
 121 | ||| Check if the given passphrase is of the correct size
 122 | ||| to be used in the hashing functions. (Passphrases are limited
 123 | ||| to a length of 512 bytes, including the terminal zero character)
 124 | export
 125 | checkphrase : (phrase : String) -> Bool
 126 | checkphrase phrase = prim__checkphrase phrase /= 0
 127 | 
 128 | ||| A refined string which has been shown to be a valid
 129 | ||| passphrase.
 130 | public export
 131 | 0 Passphrase : Type
 132 | Passphrase = Subset String (\x => checkphrase x === True)
 133 | 
 134 | ||| Checks a string to be a valid passphrase for hashing and
 135 | ||| wraps it together with the resulting proof of validity.
 136 | export
 137 | refinePassphrase : String -> Maybe Passphrase
 138 | refinePassphrase str with (checkphrase str) proof eq
 139 |   _ | True  = Just (Element str eq)
 140 |   _ | False = Nothing
 141 | 
 142 | ||| Validates the given string for having a correctly formatted
 143 | ||| prefix consisting of the hashing method, computational cost,
 144 | ||| and salt to use when encrypting a passphrase. Both, already
 145 | ||| hashed passphrases and the string returned from `gensalt`
 146 | ||| should have valid prefixes, and should therefore be usable
 147 | ||| for hashing passphrases.
 148 | export
 149 | checksalt : (salt : String) -> SaltQuality
 150 | checksalt salt = case prim__checksalt salt of
 151 |   0 => OK
 152 |   2 => Legacy
 153 |   _ => Invalid
 154 | 
 155 | ||| A refined string which has been shown to be a valid
 156 | ||| salt.
 157 | public export
 158 | 0 Salt : Type
 159 | Salt = Subset String (\x => checksalt x === OK)
 160 | 
 161 | ||| Alias for `Salt`
 162 | public export
 163 | 0 Hash : Type
 164 | Hash = Subset String (\x => checksalt x === OK)
 165 | 
 166 | ||| Checks a string to be a valid salt for hashing and
 167 | ||| wraps it together with the resulting proof of validity.
 168 | export
 169 | refineSalt : String -> Maybe Salt
 170 | refineSalt str with (checksalt str) proof eq
 171 |   _ | OK = Just (Element str eq)
 172 |   _ | _  = Nothing
 173 | 
 174 | ||| Alias for `refineSalt`
 175 | export %inline
 176 | refineHash : String -> Maybe Hash
 177 | refineHash = refineSalt
 178 | 
 179 | 
 180 | --------------------------------------------------------------------------------
 181 | --          Functions
 182 | --------------------------------------------------------------------------------
 183 | 
 184 | ||| Generate a random salt for usage as the `settings` argument
 185 | ||| in the hashing functions.
 186 | |||
 187 | ||| Implementation note: This fails on rare occasions for as of yet
 188 | ||| unknown reasons. Rerunning seems to fix it, though.
 189 | export
 190 | gensalt :
 191 |      (cm         : CryptMethod)
 192 |   -> (cost       : Bits32)
 193 |   -> {auto 0 prf : InRange cm cost}
 194 |   -> IO String
 195 | gensalt cm cost = fromPrim (go 100)
 196 | 
 197 |   where
 198 |     go : Nat -> PrimIO String
 199 |     go Z     w = prim__gensalt (cryptPrefix cm) cost w
 200 |     go (S n) w =
 201 |       let MkIORes str w2 := prim__gensalt (cryptPrefix cm) cost w
 202 |        in case checksalt str of
 203 |             Invalid => go n w2
 204 |             _       => MkIORes str w2
 205 | 
 206 | ||| Hash the given passphrase with the given salt.
 207 | ||| Usually, it is best to generate a new salt when hashing
 208 | ||| a passphrase for the first time, so consider using
 209 | ||| `crypt` instead.
 210 | export %inline
 211 | cryptWithSalt : Salt -> Passphrase -> String
 212 | cryptWithSalt (Element s _) (Element p _) = prim__crypt s p
 213 | 
 214 | ||| Hash a passphrase with the given method and computational
 215 | ||| cost. This will first generate a new random salt, therefore,
 216 | ||| this runs in `IO`.
 217 | export
 218 | crypt :
 219 |      (cm        : CryptMethod)
 220 |   -> (cost      : Bits32)
 221 |   -> (phrase    : Passphrase)
 222 |   -> {auto 0 p1 : InRange cm cost}
 223 |   -> IO String
 224 | crypt cm cost (Element p _) = do
 225 |   salt <- gensalt cm cost
 226 |   pure $ prim__crypt salt p
 227 | 
 228 | ||| Hash a passphrase with the given method and computational
 229 | ||| cost. This returns `Nothing` if the passphrase is invalid
 230 | ||| (i.e. longer than 512 bytes), or the hashing procedure itself
 231 | ||| fails to generate a valid salt (which is a highly unlikely thing
 232 | ||| to happen).
 233 | export
 234 | cryptMaybe :
 235 |      (cm        : CryptMethod)
 236 |   -> (cost      : Bits32)
 237 |   -> (phrase    : String)
 238 |   -> {auto 0 p1 : InRange cm cost}
 239 |   -> IO (Maybe Hash)
 240 | cryptMaybe cm cost phrase = do
 241 |   Just pp <- pure (refinePassphrase phrase) | Nothing => pure Nothing
 242 |   hash    <- crypt cm cost pp
 243 |   pure (refineHash hash)
 244 | 
 245 | ||| Check a clear-text passphrase against a hashed passphrase.
 246 | ||| If the hash is prefixed with a valid salt (as verified with
 247 | ||| `checksalt hash`), the hashing method, computational cost, and
 248 | ||| salt to be used will be extracted from the `hash`.
 249 | export %inline
 250 | cryptcheck : Hash -> String -> Bool
 251 | cryptcheck (Element h _) str =
 252 |   let Just (Element p _) := refinePassphrase str | Nothing => False
 253 |    in prim__cryptcheck h p == 0
 254 |