Text.Crypt

Reexports

Definitions

data SaltQuality : Type

  Quality of a salt/setting string to be used for hashing
  a passphrase. This can also be the prefix of an already
  encrypted string. `Legacy` means that the settings are
  no longer considered to be strong enough and their usage
  is discouraged.

Totality: total
Visibility: public export
Constructors:

OK : SaltQuality

Invalid : SaltQuality

Legacy : SaltQuality

Hints:

Eq SaltQuality

Show SaltQuality

data CryptMethod : Type

Totality: total
Visibility: public export
Constructors:

YesCrypt : CryptMethod

GhostYesCrypt : CryptMethod

SCrypt : CryptMethod

BCrypt : CryptMethod

SHA512Crypt : CryptMethod

SHA256Crypt : CryptMethod

Hints:

Eq CryptMethod

Show CryptMethod

cryptPrefix : CryptMethod -> String

Totality: total
Visibility: export

MinCost : CryptMethod -> Bits32

  Minimal computational cost to specify when using
  the given hashing method. The `cost` parameter
  in the `gensalt` method should be in the range
  `[MinCost c, MaxCost c]`, where `c` is the hashing method
  (`CryptMethod`) to be used.

Totality: total
Visibility: public export

MaxCost : CryptMethod -> Bits32

  Maximal computational cost to specify when using
  the given hashing method. The `cost` parameter
  in the `gensalt` method should be in the range
  `[MinCost c, MaxCost c]`, where `c` is the hashing method
  (`CryptMethod`) to be used.

Totality: total
Visibility: public export

0 InRange : CryptMethod -> Bits32 -> Type

  Proof that the given computational cost is a valid
  value for the given hashing method

Totality: total
Visibility: public export

checkphrase : String -> Bool

  Check if the given passphrase is of the correct size
  to be used in the hashing functions. (Passphrases are limited
  to a length of 512 bytes, including the terminal zero character)

Totality: total
Visibility: export

0 Passphrase : Type

  A refined string which has been shown to be a valid
  passphrase.

Totality: total
Visibility: public export

refinePassphrase : String -> Maybe Passphrase

  Checks a string to be a valid passphrase for hashing and
  wraps it together with the resulting proof of validity.

Totality: total
Visibility: export

checksalt : String -> SaltQuality

  Validates the given string for having a correctly formatted
  prefix consisting of the hashing method, computational cost,
  and salt to use when encrypting a passphrase. Both, already
  hashed passphrases and the string returned from `gensalt`
  should have valid prefixes, and should therefore be usable
  for hashing passphrases.

Totality: total
Visibility: export

0 Salt : Type

  A refined string which has been shown to be a valid
  salt.

Totality: total
Visibility: public export

0 Hash : Type

  Alias for `Salt`

Totality: total
Visibility: public export

refineSalt : String -> Maybe Salt

  Checks a string to be a valid salt for hashing and
  wraps it together with the resulting proof of validity.

Totality: total
Visibility: export

refineHash : String -> Maybe Hash

  Alias for `refineSalt`

Totality: total
Visibility: export

gensalt : (cm : CryptMethod) -> (cost : Bits32) -> {auto 0 _ : InRange cm cost} -> IO String

  Generate a random salt for usage as the `settings` argument
  in the hashing functions.
  
  Implementation note: This fails on rare occasions for as of yet
  unknown reasons. Rerunning seems to fix it, though.

Totality: total
Visibility: export

cryptWithSalt : Salt -> Passphrase -> String

  Hash the given passphrase with the given salt.
  Usually, it is best to generate a new salt when hashing
  a passphrase for the first time, so consider using
  `crypt` instead.

Totality: total
Visibility: export

crypt : (cm : CryptMethod) -> (cost : Bits32) -> Passphrase -> {auto 0 _ : InRange cm cost} -> IO String

  Hash a passphrase with the given method and computational
  cost. This will first generate a new random salt, therefore,
  this runs in `IO`.

Totality: total
Visibility: export

cryptMaybe : (cm : CryptMethod) -> (cost : Bits32) -> String -> {auto 0 _ : InRange cm cost} -> IO (Maybe Hash)

  Hash a passphrase with the given method and computational
  cost. This returns `Nothing` if the passphrase is invalid
  (i.e. longer than 512 bytes), or the hashing procedure itself
  fails to generate a valid salt (which is a highly unlikely thing
  to happen).

Totality: total
Visibility: export

cryptcheck : Hash -> String -> Bool

  Check a clear-text passphrase against a hashed passphrase.
  If the hash is prefixed with a valid salt (as verified with
  `checksalt hash`), the hashing method, computational cost, and
  salt to be used will be extracted from the `hash`.

Totality: total
Visibility: export