[Verifpal] Verifpal 0.6.8
Loup Vaillant David
loup at loup-vaillant.fr
Tue Sep 17 23:31:52 CEST 2019
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:
_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)?
_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.
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
> - 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
More information about the Verifpal