[Verifpal] 0.7.5 combinatorial explosion?

[Nadim Kobeissi]

Dear Loup,

It’s really great to hear from you. I consider it a privilege that you’ve found the time to look at Verifpal once more.

You are complaining that Verifpal is currently experiencing state space explosions, which are a defining problem in similar tools such as Tamarin and ProVerif. This is true. What is more onerous is that the reason for these state space explosions is not the presence of new bugs in Verifpal since your last email a month ago, but rather the *fixing* of bugs. You see, it turned out that Verifpal was finding some legitimate attacks not due to sound reasoning, but due to bugs in its analysis (this is mentioned in the release notes of previous updates as well)! So, in a sense, Verifpal was “cheating”.

When I started fixing this “cheating” (starting at around Verifpal 0.6.0), immediately analysis became a lot slower. My goal since roughly Verifpal 0.7.0, therefore, became speeding up the analysis, which I’ve actually accomplished substantially so far. Verifpal 0.7.5 was the first release in the 0.7.x branch that actually aimed solely at fixing analysis bugs and did not centrally focus on performance improvements (aside from a minor fix in 0.7.2). Verifpal 0.7.3 especially dramatically improved analysis speed (generally by a factor exceeding 10x.)

The good news is that I believe that we have barely scratched the surface on performance optimization, which only recently became a goal for Verifpal (since only recently did analysis speed become slower). There are still a lot of improvements that are possible, so it’s only a matter of time.

I will use the model you’ve sent as a guide for the sort of model constructions for which performance must be improved in Verifpal. Aside from regular programming-based performance improvements, on a more theoretical level the question is currently regarding the correct balance to strike in the breadth of the bounded model checking approach that Verifpal adopts for its analysis.

Welcome back, Loup!

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

> On 19 Oct 2019, at 10:10 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> Hi,
> 
> (Sorry for the long silence, life happened.)
> 
> I have tested version 0.7.5 on my Monokex X pattern (attached). It's
> been running for several hours now, with no end in sight. I've stopped
> it. The last line said:
> 
>    Stage 2, Analysis 12847...
> 
> (It did about one analysis per second.)
> 
> I don't know if this is expected, but such explosion is why I gave up
> on Tamarin in the first place. Verifpal was always pretty fast on this
> particular analysis, so I guess this is a bug? Any idea what could have
> caused this?
> 
> Loup.
> 
> <x-active.vp>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal