[Verifpal] Verifpal 0.6.8

[Loup Vaillant David]

Hello,

Very impressed by the speed increase.

Indeed, this one looks more strict in the current models.  As expected,
hmac_ok.vp and x-active.vp (monokex.vp in the examples), have results
not found by previous versions: that is, some primitives are used
before we ASSERT the equality between hashes.

Those attacks are avoided by inlining the relevant primitives in the
ASSERT line itself, but I cringe a little about the repetitions that
this sometimes entails.  x-active.vp for instance is modified thus:

    principal R[
        // _H0
        _H1  = HASH(pid, RS)
        _H2  = HASH(_H1)
        _H3  = HASH(_H2, IE)
        _H4  = HASH(_H3, IE^R)
        _H5  = HASH(_H4, zero)
        _K1  = HASH(_H4, one)
        _    = ASSERT(T1, HASH(HASH(_H5, S1), one))? // Ugly line
        _H6  = HASH(_H5, S1)                         // repetition
        _H7  = HASH(_H6, zero)
        _IS  = DEC(_K1, S1)
        _H8  = HASH(_H7, _IS^R)
        _H11 = HASH(_H8, zero)
        _T2  = HASH(_H8, one)
        _    = ASSERT(_T2, T2)?
    ]

See, I had to repeat the computation of _H6, and the long line is not
most readable. If instead I could write something like this:

        _H6  = HASH(_H5, S1)!
        _T1  = HASH(_H5, one)!
        _    = ASSERT(T1, _T1)?

Or maybe:

        _H6  = HASH(_H5, [S1])
        _T1  = HASH([_H5], one)
   
    _    = ASSERT(T1, _T1)?

So I can tell Verifpal to ignore authentication results pertaining
to the relevant lines or constants (whichever would make most sense).
But that's only a nice to have at this point, the current approach
feels good enough for now.

Loup.



On Tue, 2019-09-17 at 16:04 +0200, Nadim Kobeissi via Verifpal wrote:
> Hello everyone,
> Verifpal 0.6.8 is now available.
> 
> Change Log
> 
>    - Major refactor of analysis logic. Missed attacks in more complex
> models should be expected. However, Verifpal’s behavior is now
> significantly more correct, more complete, and analysis speed has
> increased dramatically.
> 
> Release Notes
> 
>    - This is for sure the most significant update since Verifpal was
> originally released a few weeks ago.
>    - Ouf, where to begin. While debugging 0.6.7, one thing led to
> another, and I’ve spent the last three days obsessively refactoring a
> huge part of the analysis logic. Overall, this release is much faster
> (due to less resolution steps) and I think much more correct in its
> analysis — however, I am also certain that it misses more attacks
> than 0.6.7.
>    - “But Nadim, if it’s more correct in its analysis, how can it
> miss more attacks?” — turns out a lot of attacks detected in earlier
> versions were due to incorrect analysis — Verifpal was more or less
> cheating.
>    - To be clear, 0.6.8 still matches all the expected results from
> Loup’s test models as well as my internal testing models. In fact it
> even finds missed attacks in 0.6.7! There’s no obvious regression…
> yet. But I am 100% sure that 0.6.8 will miss attacks that 0.6.7
> “finds”. I am absolutely certain of this. What I would really like
> you guys to do is find those missed attacks and document them. They
> are *certainly* out there.
> 
> Installing and Updating Verifpal
> 
>    - If you’re fine with running arbitrary scripts in your terminal,
> you can instantly update like this:
>        - bash -c 'curl -sL https://verifpal.com/install|bash'
>    - Or you can download a pre-compiled binary here:
>        - https://source.symbolic.software/verifpal/verifpal/releases
> 
> Looking forward to hearing from you all!
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal