[Verifpal] Verifpal 0.6

[Loup Vaillant David]

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
-------------- next part --------------
attacker[active]

// initialisation
principal Alice[
    knows private a
    a_public = G^a
]
principal Bob[
    knows private b
    b_public = G^b
]
Alice -> Bob   : a_public
Bob   -> Alice : [b_public]


// Key exchange
principal Alice[
    generates plaintext
    ss         = b_public^a
    key        = HASH(ss)
    ciphertext = ENC(key, plaintext)
    tag        = MAC(key, ciphertext)
]
Alice -> Bob : ciphertext, tag

principal Bob[
    ss_        = a_public^b
    key_       = HASH(ss_)
    tag_       = MAC(key_, ciphertext)
    _          = ASSERT(tag, tag_)?
    plaintext_ = DEC(key_, ciphertext)
]

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
]
-------------- next part --------------
attacker[active]

// initialisation
principal Alice[
    knows private a
    a_public = G^a
]
principal Bob[
    knows private b
    b_public = G^b
]
Alice -> Bob   : [a_public]
Bob   -> Alice : b_public


// Key exchange
principal Alice[
    generates plaintext
    ss         = b_public^a
    key        = HASH(ss)
    ciphertext = ENC(key, plaintext)
    tag        = MAC(key, ciphertext)
]
Alice -> Bob : ciphertext, tag

principal Bob[
    ss_        = a_public^b
    key_       = HASH(ss_)
    tag_       = MAC(key_, ciphertext)
    _          = ASSERT(tag, tag_)?
    plaintext_ = DEC(key_, ciphertext)
]

queries[
    confidentiality? plaintext
    authentication? Alice -> Bob : ciphertext
]