[Verifpal] Apparent state explosion on seemingly simple model

Nadim Kobeissi nadim at symbolic.software
Mon Nov 30 16:14:11 CET 2020

Dear Loup,

I’ve looked at Monokex in Verifpal twice before, and I can confidently tell you that it is absolutely impossible to analyze this protocol on 2GB of RAM.

I have never seen a protocol more likely to cause state space explosions than Monokex during analysis. It’s even worse than Noise (which itself is quite likely to cause them especially in patterns such as IK). There is no way that 2GB of RAM will cut it, and even in ProVerif and Tamarin I am certain the result will require a *lot* of patience.

For comparison. Noise IKpsk2’s ProVerif model took 30 days to analyze.

You will need to split up the protocol into multiple models or find some way to simplify how it’s expressed. 

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

> On Nov 30, 2020, at 4:10 PM, Loup Vaillant-David <loup at loup-vaillant.fr> wrote:
> Hi,
> We are currently trying to analyse Monokex with Verifpal, and it is not
> working.  Typical behaviour, with both 0.19.3 and 0.19.4, is hanging
> for a few hours, and eventually being killed by the OOM killer (my
> laptop has 2GB of RAM).
> The model is attached. This is based on the latest version of Monokex,
> pattern N (non-interactive, anonymous sender). It was chosen because it
> was the simplest pattern of them all. Least likely to trigger state
> explosion, or so we thought.
> Any idea what might cause the problem, and how we may get around it?
> Ways to cull the search space, maybe? Or do I just need a bigger
> computer?
> Loup.
> <monokex-n.vp>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal

More information about the Verifpal mailing list