[Verifpal] Authenticating keys with a hash sent over a second channel
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
attacker [ active]principal Alice[ knows private alice_key
alice_key_hash = HASH(alice_key)]principal BobAlice -> 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...
More information about the Verifpal