[Verifpal] New Feature: Modeling Passwords and Password Hashing

Nadim Kobeissi nadim at symbolic.software
Sat Jan 25 18:06:07 CET 2020

Hello everyone,

Verifpal 0.9.13 comes with a new exciting feature: modeling for
passwords and password hashing.

This exciting new feature allows us to declare constants with the
qualifier "password": like this:
knows password x

Now, if x is used as an encryption key or in any other way within a
primitive, and that primitive is revelaed to the attacker, for example:
Alice -> Bob: ENC(x, m1), PKE_ENC(G^x, m2)

The attacker will be able to obtain x and therefore both m1 and m2.
However, had we done:

Alice -> Bob: ENC(PW_HASH(x), m1)

... then the attacker would not have been able to obtain x or m1. This
is because values declared with the password qualifier are only usable
securely in publicly communicated values if first put through a
primitive that is a password hashing function. The newly introduced
PW_HASH primitive is currently the only primitive that can act as a
password hashing function. HASH, HKDF and others won't cut it.

This is very useful for modeling protocols that include user-provided
passwords at points, and is a great way to separate guessable passwords
from material that can actually securely be used as an encryption key of
some kind.

I would like to sincerely thank Jean-Philippe Aumasson, who completely
came up with the idea for this feature. I got so excited about it that I
implemented it in the same day.

Update to Verifpal 0.9.13 today and give it a shot! The Verifpal User
Manual, Visual Studio Code and Vim extensions have also been updated
to reflect this new feature.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

More information about the Verifpal mailing list