[Verifpal] Runtime for analysis?

Nadim Kobeissi nadim at symbolic.software
Tue Mar 3 20:42:50 CET 2020


Finding a way to illustrate a model that performs the analyses you want without causing state space explosions is a classic tedious task in symbolic protocol modeling, welcome to the club :-)

Let me know if you find out a creative way to illustrate your protocol without running into this issue.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 3 Mar 2020, at 8:40 PM, Friedrich Wiemer <friedrich.wiemer at rub.de> wrote:
> 
> 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: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200303/ed290a75/attachment.sig>


More information about the Verifpal mailing list