[Verifpal] Runtime for analysis?

Nadim Kobeissi nadim at symbolic.software
Mon Mar 2 22:54:43 CET 2020


Dear Friedrich,

I just took a look at your model and checked how Verifpal was analyzing it.
Verifpal's analysis appears to be proceeding correctly.

The reason why your model is going to take a long time to analyze has to do
with the value `m_alice`, which is equal to CONCAT(k_ab, B, Na, e_bob).
Such values can quickly cause a "state space explosion" in Verifpal and
other symbolic model verifiers due to the fact that they force the attacker
to consider a very high number of potential replacements for m_alice, given
the number of possible different concatenations that match the
type/skeleton of all the elements involved (all constants except for e_bob).

If you make e_alice a guarded constant as it travels across the network,
like this, you will notice that analysis speed will increase dramatically:
Server -> Alice: [e_alice]

That being said, I am not sure if this is an acceptable modification to
make to your model, that's entirely up to you. Either way, what I would do
is avoid creating values like `m_alice` which have a very large number of
valid and type-safe rewrites. Or, if I do create and communicate them, I
would try to avoid making them malleable by the attacker unless such a
thing would greatly reduce the usefulness of my model at spotting attacks.

I hope this is helpful and am happy to discuss further.

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


On Mon, Mar 2, 2020 at 8:46 PM Friedrich Wiemer via Verifpal
<verifpal at lists.symbolic.software> wrote:

> Hi,
>
> I expect I now have a working model of the Needham-Schroeder protocol in
> verifpal (see attached). When I run verifpal on this, it seems to run
> very long at "Step 4, Analysis 430..." (I have started the same run on a
> remote server, to see if there is an output in some hours.)
>
> I assume that sometime (often?) the analysis runtime is quite high, so
> this might be expected. But is it possible to get some information, if
> verifpal is still working as expected?
>
> Best,
> Friedrich
>
> --
> Dr. Friedrich Wiemer,
> Research Assistant
>
> Symmetric Cryptography
> Horst Goertz Institute for IT-Security,
> Ruhr-University Bochum,
>
> orcid.org/0000-0003-2998-6777
>
> _______________________________________________
> 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/20200302/65a1e1eb/attachment.htm>


More information about the Verifpal mailing list