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

Nadim Kobeissi nadim at symbolic.software
Sun Jan 5 14:06:06 CET 2020


Dear Alexander,

Thank you very much for sending in this model of Delta Chat's Setup Contact
Protocol:
https://countermitm.readthedocs.io/en/latest/new.html#setup-contact-protocol

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.

Very happy to discuss more! Thank you for using Verifpal.

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


On Sun, Jan 5, 2020 at 11:27 AM Alexander Krotov via Verifpal
<verifpal at lists.symbolic.software> wrote:

> 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.
>
> _______________________________________________
> 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/20200105/57c7b860/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: countermitm.vp
Type: application/octet-stream
Size: 1894 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200105/57c7b860/attachment.obj>


More information about the Verifpal mailing list