[Verifpal] Authenticating keys with a hash sent over a second channel

Alexander Krotov ilabdsf at gmail.com
Sun Jan 5 10:56:52 CET 2020

(sending again as plaintext)

I am trying to verify a simple protocol for contact verification that is
used in Delta Chat:

I have a question with respect to authentication? query. I have this
minimal example:

attacker [

principal Alice[
    knows private alice_key
    alice_key_hash = HASH(alice_key)

principal Bob[

Alice -> Bob: alice_key

Alice -> Bob: [alice_key_hash]

principal Bob[
    bob_key_verified = ASSERT(HASH(alice_key), alice_key_hash)?

    authentication? Alice -> Bob: alice_key

It models Alice sending her public key over the network to Bob, while at
the same time showing a QR code of the key hash to him. Bob then
computes the same key and verifies that the key is valid.

With Verifpal 0.8.3 I get this error: "alice_key, sent by Alice and
resolving to alice_key, is successfully used in primitive
ASSERT(HASH(alice_key), HASH(alice_key))? in Bob's state, despite it
being vulnerable to tampering by Attacker" But the fact that Bob used
unauthenticated alice_key to compute its hash is not a problem in this
protocol: computing the hash is done exactly to authenticate alice_key.

Currently I sidestep this problem by using alice_key together with
bob_key (not present in this example) to construct a shared secret and
use it to send a message. Then I check for confidentiality of the
message plaintext. But it would be nice to check for authenticity of
alice_key directly. Is there any way to do it?

More information about the Verifpal mailing list