[Verifpal] An attempt to implement https://countermitm.readthedocs.io/en/latest/new.html#setup-contact-protocol

Alexander ilabdsf at gmail.com
Mon Jan 6 05:30:36 CET 2020

> I don't fully understand what's happening in this model/protocol, but
> my take based on my quick read is that even though `auth` is leaked to
> the attacker, Bob is obtaining that value from `qr_enc_auth` and never
> actually uses `auth` itself (as published on the network) anywhere.
> That's why no attack is found, which appears to be a sound result.
AUTH should only be known to Bob, because Bob uses it in
vc-request-with-auth step to authenticate his key.

I have attached an updated version of the model that works with Verifpal
0.8.4. I don't send a message anymore and check for authentication of
Bob's public key explicitly.

I have this line inside:

        encrypted_auth = AEAD_ENC(bob_shared_secret, qr_dec_auth, nil)

Here Bob uses qr_dec_auth. In this case verifpal finds no attack.
However, if I replace it with this line with (commented out inside the
attached file)

        encrypted_auth = AEAD_ENC(bob_shared_secret, auth, nil)

it finds an attack.

auth and qr_dec_auth are the same, because qr_dec_auth = DEC(qr_key,
qr_enc_auth) = DEC(qr_key, ENC(qr_key, auth)), but somehow changing this
line makes a difference for Verifpal.

I believe the attack should be found in both cases, because AUTH token
is the only protection of Bob's public key against modification by the

-------------- next part --------------
// SPDX-FileCopyrightText: © 2020 Alexander Krotov <ilabdsf at gmail.com>
// SPDX-License-Identifier: MIT

// Implementation of https://countermitm.readthedocs.io/en/latest/new.html#setup-contact-protocol


principal Alice[
	knows private alice_private_key
	alice_public_key = G^alice_private_key
	alice_fp = HASH(alice_public_key)

principal Bob[
	knows private bob_private_key
	bob_public_key = G^bob_private_key
	bob_fp = HASH(bob_public_key)

// Step 1.

// vc-invite
// Everything is guarded here, as it is sent
// over a second channel.
// AUTH is encrypted with a known key to model that
// attacker can't get a copy of AUTH during QR-code scanning.

principal Alice [
	knows private qr_key
        generates auth
        qr_enc_auth = ENC(qr_key, auth)
principal Bob [
	knows private qr_key
Alice -> Bob : [alice_fp], [qr_enc_auth]
principal Bob [
        qr_dec_auth = DEC(qr_key, qr_enc_auth)

// Leak AUTH to attacker!
// Attacker should be able to impersonate Bob now.
Alice -> Bob : [auth]

// Step 2.

// vc-request
Bob -> Alice : bob_public_key

// Step 3.

// vc-auth-required
Alice -> Bob : alice_public_key

// Step 4.

principal Bob[
	alice_key_is_verified = ASSERT(alice_fp, HASH(alice_public_key))?

// vc-request-with-auth
principal Bob[
	bob_shared_secret = alice_public_key^bob_private_key

	// The same line using AUTH leaked in plaintext above:
	// encrypted_auth = AEAD_ENC(bob_shared_secret, auth, nil)
	encrypted_auth = AEAD_ENC(bob_shared_secret, auth, nil)

	encrypted_bob_fp = AEAD_ENC(bob_shared_secret, bob_fp, nil)
Bob -> Alice : encrypted_auth, encrypted_bob_fp

/// Step 5.

principal Alice[
	alice_shared_secret = bob_public_key^alice_private_key
	decrypted_auth = AEAD_DEC(alice_shared_secret, encrypted_auth, nil)?
	auth_is_ok = ASSERT(auth, decrypted_auth)?
	decrypted_bob_fp = AEAD_DEC(alice_shared_secret, encrypted_bob_fp, nil)?
	bob_key_ok = ASSERT(decrypted_bob_fp, HASH(bob_public_key))?

queries [
	confidentiality? alice_private_key
	confidentiality? bob_private_key
	authentication? Alice -> Bob : alice_public_key
	authentication? Bob -> Alice : bob_public_key

More information about the Verifpal mailing list