[Verifpal] Verifpal 0.6.8

[Nadim Kobeissi]

I’ve made some headway on the missed attacks. What’s nice is that they’re being missed for good reasons (active attacker is not injecting the right values) instead of being found for the wrong reasons (“cheating” in previous versions.)

I suspect 0.6.9 will be just as fast as 0.6.8 but will find the missed attacks. If you want an example of missed attacks try unchecking all the primitives in the Scuttlebutt model — not all queries will be contradicted, and especially, message 2 won’t be found.

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

> On Sep 17, 2019, at 11:31 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> 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
>