[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 11:27:20 CET 2020
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
]
More information about the Verifpal
mailing list