[Verifpal] Apparent state explosion on seemingly simple model

Loup Vaillant-David loup at loup-vaillant.fr
Mon Nov 30 19:43:26 CET 2020


> I just noticed the subject of this email: the model is indeed simple
> but the state space explosions come from the *very* nested HKDF and
> hashing operations. The result would be the same in ProVerif, Tamarin
> and other frameworks.

I vaguely suspected as much.

Thanks for the quick answer. Now I have some deep thinking to do.

Loup.




More information about the Verifpal mailing list