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

Alexander Krotov ilabdsf at gmail.com
Sun Jan 5 22:42:17 CET 2020


> I have made a slight improvement to your proposed model that should
> decrease analysis time, please find it attached. By running a diff
> between your original model and my suggested modifications, the changes
> should become apparent.
> 
> The attached model completes analysis on my machine in about 3 minutes
> when running Verifpal 0.8.4. It seems to find some attacks, you might
> want to take a look.

The attack found is due to attacker accessing the generated AUTH token
during QR-code scanning. Normally it does not happen.

I have modified QR-code exchange as follows, qr_key is used to model
second channel which attacker can't read. AUTH is now transferred in
encrypted form:

// 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)
]

Now verifpal doesn't find any attack. However, if I add another line,
leaking AUTH to attacker, it still doesn't find any attack:

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

Looks like Verifpal is missing an attack now.

Complete model with code that leaks AUTH is attached.
-------------- 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

attacker[active]

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
	encrypted_auth = AEAD_ENC(bob_shared_secret, qr_dec_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))?
]


// Now we send a message from Bob to Alice

principal Bob [
	generates plaintext
	ciphertext = AEAD_ENC(bob_shared_secret, plaintext, nil)
]

Bob -> Alice : ciphertext

principal Alice [
	plaintext_dec = AEAD_DEC(alice_shared_secret, ciphertext, nil)?
]

queries [
	confidentiality? alice_private_key
	confidentiality? bob_private_key
	confidentiality? plaintext
	authentication? Bob -> Alice: ciphertext
]


More information about the Verifpal mailing list