[Verifpal] Verifpal 0.6

[Nadim Kobeissi]

Verifpal 0.6.2 is out with more improvements.

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

> On Sep 10, 2019, at 5:21 AM, Nadim Kobeissi <nadim at symbolic.software> wrote:
> 
> Dear Loup,
> 
> Thanks again for your feedback! Once I read your email, I couldn’t sleep until I had resolved the issues you’ve pointed out.
> 
> Verifpal 0.6.1 is now available, and it should address the issues — please continue your testing!
> 
>> I feel there's some amount of redundancy in Verifpal: aead can be
>> expressed in terms of encrypt then mac. The respective models should be
>> equivalent —trivially so. But they're not…
>> 
>> It looks like Verifpal uses different code paths to treat AEAD and
>> encrypt then mac. This would explain the discrepancy. So while the user
>> interface should probably not be unified, for usability reasons, the
>> *implementation* should probably be, if only because it would shorten
>> the proof of Verifpal's soundness.
> 
> Respectfully, I’d like to express that I am annoyed by this sort of baseless conjecture. It’s really, really not that simple.
> 
> The implementation of AEAD_ENC and ENC+MAC, when it comes to most cases involving authentication queries, is unified in the abstract. But this doesn’t even hold for all cases. There are scenarios where unification simply does not hold, and this has to do with how MACs are communicated separately and some other things.
> 
> This particular issue was not due to the interfaces for these functions or the intuition for Verifpal’s proof of soundness. It actually had to do with how the attacker chose to replace values as they are being communicated over the network, as well as two unrelated silly code bugs (two bad boolean checks). The fix required quite a bit of re-engineering with regards to how the attacker decided to send malicious values on the network.
> 
> A common theme in open source software development is people jumping to conclusions about a certain issue or bug. I don’t want this in the Verifpal community, and I hope nobody engages in allusions so long as they have not read the code.
> 
> This sounds harsher than intended, but I want to offset this sort of pontification early on in the mailing list’s history. I hope you understand.
> 
>> Internally, MAC and KDF (is is still called HKDF?) and HASH should
>> probably be unified into a hash that can return multiple results. (That
>> could be HASH itself, if we modify such that it does return multiple
>> results.)
> 
> Yes, we’re going to stick to HKDF, only because we use the same interface as the Krawczyk construction, and he decided to call it HKDF instead of KDF.
> 
>> Likewise, AEAD_ENC and AEAD_DEC should expand internally into their
>> encrypt then mac counterparts. We may need to implement an abstraction
>> mechanism (function or macro), but we don't have to expose it to users.
> 
> Nope. AEAD and ENC+HMAC are not strictly interchangeable in the symbolic model.
> 
> Thanks again, Loup — I really believe the Verifpal project is very lucky to have you as a contributor.
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
>> On Sep 9, 2019, at 11:15 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
>> 
>> Hi,
>> 
>> I have added 2 files to my test "suite":
>> 
>> - hmac_unguarded_alice.vp
>> - hmac_unguarded_bob.vp
>> 
>> The unguarded Bob file went as expected: confidentiality (and only
>> confidentiality) is broken.
>> 
>> The unguarded Alice file however missed the authenticity violation
>> (since Alice's key is not guarded, she is basically indistinguishable
>> from an attacker).
>> 
>> ---
>> 
>> I feel there's some amount of redundancy in Verifpal: aead can be
>> expressed in terms of encrypt then mac. The respective models should be
>> equivalent —trivially so. But they're not…
>> 
>> It looks like Verifpal uses different code paths to treat AEAD and
>> encrypt then mac. This would explain the discrepancy. So while the user
>> interface should probably not be unified, for usability reasons, the
>> *implementation* should probably be, if only because it would shorten
>> the proof of Verifpal's soundness.
>> 
>> Internally, MAC and KDF (is is still called HKDF?) and HASH should
>> probably be unified into a hash that can return multiple results. (That
>> could be HASH itself, if we modify such that it does return multiple
>> results.)
>> 
>> Likewise, AEAD_ENC and AEAD_DEC should expand internally into their
>> encrypt then mac counterparts. We may need to implement an abstraction
>> mechanism (function or macro), but we don't have to expose it to users.
>> 
>> Loup.
>> 
>> 
>> 
>> On Mon, 2019-09-09 at 19:21 +0200, Nadim Kobeissi via Verifpal wrote:
>>> Hello everyone,
>>> Verifpal 0.6 is now available.
>>> 
>>> RELEASE NOTES
>>>   - BREAKING: `HMACVERIF` has been renamed to `ASSERT`.
>>>   - BREAKING: `HMAC` has been renamed to `MAC`.
>>>   - Reduced the number of false positives.
>>> 
>>> INSTALLING AND UPDATING
>>>   - 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
>>> 
>>> NOTES ABOUT THIS VERSION
>>>   - Loup, this finally fixes the false positives on your hmac_ok
>>> and other models! Please do continue testing!
>>> 
>>> 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
>> <hmac_unguarded_alice.vp><hmac_unguarded_bob.vp>
>