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

Nadim Kobeissi nadim at symbolic.software
Mon Jan 6 04:41:55 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.

Do you think this is not an intuitive way for Verifpal to interpret your
model? I am interested in hearing your thoughts.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Sun, Jan 5, 2020 at 10:42 PM Alexander Krotov via Verifpal
<verifpal at lists.symbolic.software> wrote:

> > 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.
>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200106/8a7f0a89/attachment.htm>


More information about the Verifpal mailing list