Password Hashing


The basic problem is that user have a password, which the "system" must be able to validate, but which should be kept secret for everybody else.

Password Hash

The idea is to create a cryptographic hash of the password and save that in the "user dictionary".

class predicates
    password_hash : (string Password) -> string Hash.
    password_hash(Password) = cryptography::<someSuitableHashFunction>(Password).

To validate the password you hash again and compare the new hash to the stored hash:

class predicates
    password_validate (string Password, string Hash) determ.
    password_validate(Password, Hash) :-
        Hash = password_hash(PassWord).

A cryptographic hash is a hash with the property that it is "hard" to come from the hash value back to the password or to find something else that gives the same hash value.

Rainbow table

However, this approach has the problem that you can create a so called rainbow table: you take a huge amount of frequently used passwords and hash them with someSuitableHashFunction and then it is easy to come backwards for those frequently used passwords.


To avoid this you can make sure that the users password is not frequently use. That is done by applying salt to the users passwords.

If the users password is "horse" then you actually hash "<salt>horse", where <salt> is something strange, e.g. "Qa12#5ASGhorse" (this is the idea behind salting; in practice it is done in a slightly different way).

class predicates
    password_hash : (string Password, string Salt) -> string Hash.
    password_hash(Password, Salt) = cryptography::<someSuitableHashFunction>(Hash, Salt).

the same Salt should be used when validating the password:

class predicates
    password_validate (string Password, string Salt, string Hash) determ.
    password_validate(Password, Salt, Hash) :-
        Hash = password_hash(PassWord, Salt).

In principle you can use the same salt each time, but if a hacker gets knowledge about the salt she can make a new rainbow table with that salt, and then we are back to square one.

Subsequently, it is recommended to use a new long random salt each time. This salt does however not need to be kept secret, but can be saved in the user dictionary together with the password hash.

Here the combination of hash and salt is called a hashToken:

    hashToken = hashToken(string Salt, string Hash).
class predicates
    password_hash : (string Password) -> hashToken HashToken.
    password_hash(Password) = hashToken{Salt, Hash} :-
        Salt = generateRandomSalt(),
        cryptography::<someSuitableHashFunction>(Hash, Salt).
class predicates
    password_validate (string Password, hashToken HashToken) determ.
    password_validate(Password, hashToken(Salt, Hash)) :-
        Hash = cryptography::<someSuitableHashFunction>(PassWord, Salt).


The last issue is the choice of someSuitableHashFunction. As already mentioned it must be difficult to come from hash to password. A consequence of this is (somewhat oddly) that it must take long time to calculate the hash of a password. Because if it is fast then it is also fast to create rainbow tables and the like. Notice however that the calculation must take long time for the hacker; it does not help that you have a hopeless implementation, if the hacker has a good implementation.

A problem in that context is that what is a suitably slow algorithm today may be too fast in some years.

As a consequence of this and probably also for many other reasons you will have to expect that you will have to change or adjust the algorithm as time passes.

Currently, various places on the net state that PBKDF2+SHA1+10.000 is a good choice.

PBKDF2 is an algorithm that takes another algorithm hash H argument and makes N iterations using H in some way.

PBKDF2+SHA1+10.000 means that H is the hash algorithm SHA1 that N is 10.000 (i.e. that the algorithm makes 10.000 iterations).

The number 10.000 is assumed to be increased as computers becomes faster.

All in all, we must expect that we will have to adjust the algorithm as time goes by.


JWT (JSON Web Tokens) does not deal with this problem, but we have used some of the ideas in this context.

A Hash Token consists of three components:

  1. A description of the algorithm and its parameters
  2. the salt
  3. the hash

Like in JWT the algorithm and its parameters are described as a JSON object:

   { "alg" : "PBKDF2", "hash" : "SHA1", "p2c" : 10000 }

The three components are Base64 for URL encoded and combined with ".".

So a HashToken will look like this (the token does not have any line shifts, they are just inserted here for readability):


.1xVFoIMO9C-u3O81CYoUxkV3KB_vAxUmMvrvTG9hHaM .v9cZjPwtji27vjeCFj8SLwzkqWUDe9OmT9YC3sLOMps

  1. eyJhbGciOiJQQktERjIiLCJoYXNoIjoiU0hBMjU2IiwicDJjIjoxMDAwMH0 is the JSON object that describes the algorithm and its arguments (utf8 + base64 URL encoded)
  2. 1xVFoIMO9C-u3O81CYoUxkV3KB_vAxUmMvrvTG9hHaM is the salt (base64 URL encoded)
  3. v9cZjPwtji27vjeCFj8SLwzkqWUDe9OmT9YC3sLOMps is the hash (base64 URL encoded)

The key point is that a HashToken contains all the information that is necessary to validate a password, even though you use different algorithms, parameters and random salt.

So a single predicate can validate passwords, even when algorithms and parameters changes, and different algorithms/parameters can also be mixed in a single user dictionary.

    password_validate : (string Password, string HashToken) determ.

For now PFC supports PBKDF2 and main algorithm:

    password_pbkdf2 : (string Password, integer64 IterationCount = 10000, string HashAlgId = bcrypt_sha256_algorithm) 
	    -> string HashToken.

The actual hashing is performed by the default cryptography provider on the computer, and it has been validated that SHA1, SHA256, SHA384 and SHA512 can be used as hash algorithm.


This little example:

implement main
    open core, stdio, bCrypt_native
    run() :-
        Password = "MySweetLittlePony",
        FalsePassword = "MySweetLittleCat",
        foreach HashAlgId in [bcrypt_sha1_algorithm, bcrypt_sha256_algorithm] do
            writef("HashAlgId = %\n", HashAlgId),
            test(Password, FalsePassword, HashAlgId),
            test(Password, FalsePassword, HashAlgId)
        end foreach.
class predicates
    test : (string Password, string FalsePassword, string HashAlgId).
    test(Password, FalsePassword, HashAlgId) :-
        HashToken = cryptography::password_pbkdf2(Password, :HashAlgId = HashAlgId),
        writef("%\n", HashToken),
        validate(Password, HashToken),
        validate(FalsePassword, HashToken),
class predicates
    validate : (string Password, string HashToken).
    validate(Password, HashToken) :-
        Valid = if cryptography::password_validate(Password, HashToken) then "valid" else "invalid" end if,
        writef("% is %\n", Password, Valid).
end implement main

will produce output like this:

    HashAlgId = SHA1
    MySweetLittlePony is valid
    MySweetLittleCat is invalid

    MySweetLittlePony is valid
    MySweetLittleCat is invalid

    HashAlgId = SHA256
    MySweetLittlePony is valid
    MySweetLittleCat is invalid

    MySweetLittlePony is valid
    MySweetLittleCat is invalid

The output is only "like" this because a random salt is generated each time password_pbkdf2 is called.

The first part is the same when the algorithm (and parameters) is the same, and the length of the salt and the hash depends on the chosen algorithm.