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

Alexander Krotov ilabdsf at gmail.com
Sun Jan 5 10:35:11 CET 2020

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 [    active]principal Alice[    knows private alice_key   
alice_key_hash = HASH(alice_key)]principal Bob[]Alice -> Bob:
alice_keyAlice -> Bob: [alice_key_hash]principal Bob[   
bob_key_verified = ASSERT(HASH(alice_key), alice_key_hash)? ]queries[   
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?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200105/bc2ac80b/attachment.htm>

More information about the Verifpal mailing list