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

[Alexander Krotov]

Attached is an attempt to implement Setup Contact protocol in Verifpal.
In its current form it takes too long to verify, I stopped it at "Stage
3, Analysis 380616..." after at least several hours of real time.
-------------- 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.
//

principal Alice [
	generates auth
]

// vc-invite
// Everything is guarded here, as it is sent
// over a second channel.
Alice -> Bob : [alice_fp], [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
	generates ad
	encrypted_auth = AEAD_ENC(bob_shared_secret, auth, ad)
	encrypted_bob_fp = AEAD_ENC(bob_shared_secret, bob_fp, ad)
]
Bob -> Alice : ad, 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, ad)?
	auth_is_ok = ASSERT(auth, decrypted_auth)?
	decrypted_bob_fp = AEAD_DEC(alice_shared_secret, encrypted_bob_fp, ad)?
	bob_key_ok = ASSERT(decrypted_bob_fp, HASH(bob_public_key))?
]


// Now we send a message from Bob to Alice

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

Bob -> Alice : ciphertext, ad2

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

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