[Verifpal] Runtime for analysis?

Friedrich Wiemer friedrich.wiemer at rub.de
Tue Mar 3 20:40:13 CET 2020


Dear Nadim,

thats indeed much faster! Thanks for the explanation. However, I think
this is not really a good modification, but I'll think about it a bit
more.

Best,
Friedrich

On Mon, Mar 02, 2020 at 10:54:43PM +0100, Nadim Kobeissi wrote:
> 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
> 

-- 
Dr. Friedrich Wiemer,
Research Assistant

Symmetric Cryptography
Horst Goertz Institute for IT-Security,
Ruhr-University Bochum,

orcid.org/0000-0003-2998-6777
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200303/d76905b0/attachment.sig>


More information about the Verifpal mailing list