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@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@lists.symbolic.software
https://lists.symbolic.software/mailman/listinfo/verifpal