[Verifpal] Apparent state explosion on seemingly simple model

Loup Vaillant-David loup at loup-vaillant.fr
Mon Nov 30 16:10:05 CET 2020


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


-------------- next part --------------

// Verifpal 0.19.4
// Monokex, "N" pattern


principal A[]
principal B[
    generates R
    RS = G^R

B -> A: [RS]

principal A[
    knows public pid, zero
    knows private p1, text1
    generates E

    IE = G^E
    H0 = HASH(pid)
    H1 = HKDF(H0, RS, nil)
    H2 = HKDF(H1, H1, nil)
    H3 = HKDF(H2, IE, nil)
    H4 = HKDF(H3, RS^E, nil)
    H5, K1 = HKDF(H4, zero, zero)
    S1 = ENC(K1, p1)
    H6, T1 = HKDF(S1, H5, nil)

    // Ready, use it
    TRY1 = ENC(H6, text1)

A -> B: IE, S1, T1, TRY1

principal B[
    knows private text2
    _H0 = HASH(pid)
    _H1 = HKDF(_H0, RS, nil)
    _H2 = HKDF(_H1, _H1, nil)
    _H3 = HKDF(_H2, IE, nil)
    _H4 = HKDF(_H3, IE^R, nil)
    _H5, _K1 = HKDF(_H4, zero, zero)
    _H6, _T1 = HKDF(S1, _H5, nil)
    _ = ASSERT(_T1, T1)?

    // Ready, use it
    TRY2 = ENC(_H6, text2)

B -> A: TRY2

    confidentiality? text1
    confidentiality? text2

More information about the Verifpal mailing list