Title: OTR AKE in Verifpal
Date: 2023-05-15 19:15

I recently attended a talk at work about formal verification of cryptographic
protocol, and was horrified by the nested amount of complexity to do basic
reasoning. Which reminded me about [Verifpal](https://verifpal.com/):

> Verifpal® is new software for verifying the security of cryptographic
protocols. Building upon contemporary research in symbolic formal verification,
Verifpal’s main aim is to appeal more to real-world practitioners, students and
engineers without sacrificing comprehensive formal verification features.

So I modelled OTRv3's Authenticate Key Exchange in it, and here is the result
(it'll look prettier once [this](https://github.com/pygments/pygments/pull/2430) gets merged.):

```verifpal
// OTRv3 Authenticated Key Exchange (AKE)
// https://otr.cypherpunks.ca/Protocol-v3-4.1.1.html

attacker[passive]

// Setup
principal Bob [
    knows private priv_b
    pub_b = G^priv_b
]
Bob → Alice: [pub_b]
principal Alice[
    knows private priv_a
    pub_a = G^priv_a
]
Alice → Bob: [pub_a]

// Go!
principal Bob [
    generates r, x
    g_x = G^x
    enc_gx = ENC(r, g_x)
    hash_gx = HASH(g_x)
]

Bob → Alice: enc_gx, hash_gx

principal Alice [
    generates y
    g_y = G^y
]

Alice → Bob: g_y

principal Bob [
    s = g_y^x
    c, c_ = HKDF(s, nil, nil)
    m1, m2, m1_, m2_ = HKDF(nil, s, nil)
    generates keyid_b
    Mb = MAC(m1, CONCAT(g_x, g_y, pub_b, keyid_b))
    Xb = CONCAT(pub_b, keyid_b, SIGN(priv_b, Mb))
    enc_c_x_b = ENC(c, Xb)
    mac_mc2_enc_c_x_b  = MAC(m2, ENC(c, Xb))
]

Bob → Alice: r, enc_c_x_b, mac_mc2_enc_c_x_b

principal Alice [
    dec_gx = DEC(r, enc_gx)
    _ = ASSERT(HASH(dec_gx), hash_gx)?
    s_ = dec_gx^y
    c_alice, c__alice = HKDF(s_, nil, nil)
    m1_alice, m2_alice, m1__alice, m2__alice = HKDF(nil, s_, nil)
    _ = ASSERT(mac_mc2_enc_c_x_b, MAC(m2_alice, enc_c_x_b))?
    xb_alice = DEC(c_alice, enc_c_x_b)
    pub_b_alice, keyd_b_alice, sig_b_mb_alice = SPLIT(xb_alice)
    mb_alice = MAC(m1_alice, CONCAT(dec_gx, g_y, pub_b_alice, keyd_b_alice))
    _ = SIGNVERIF(pub_b_alice, mb_alice, sig_b_mb_alice)?
    generates keyid_a
    ma = MAC(m1__alice, CONCAT(g_y, dec_gx, pub_a, keyid_a))
    xa = CONCAT(pub_a, keyid_a, SIGN(priv_a, ma))
    enc_c__x_a = ENC(c__alice, xa)
    mac_m2_enc_c__xa = MAC(m2__alice, ENC(c__alice, xa))
]

Alice → Bob: enc_c__x_a, mac_m2_enc_c__xa

principal Bob [
    _ = ASSERT(mac_m2_enc_c__xa, MAC(m2_, enc_c__x_a))?
    xa_bob = DEC(c_, enc_c__x_a)
    pub_a_bob, keyid_a_bob, sig_a_ma_bob = SPLIT(xa_bob)
    ma_bob = MAC(m1_, CONCAT(g_y, g_x, pub_a_bob, keyid_a_bob))
    _ = SIGNVERIF(pub_a_bob, ma_bob, sig_a_ma_bob)?
    _ = ASSERT(pub_a_bob, pub_a)?
]

queries [
    equivalence? s, s_
    confidentiality? s
    freshness? s

    equivalence? pub_b, pub_b_alice
    equivalence? pub_a, pub_a_bob
]
```

```console
$ verifpal verify ./otr_ake.vp | tail -n 5

 Verifpal • Verification completed for 'otr_ake.vp' at 11:11:52 PM. 
 Verifpal • All queries pass. 

 Verifpal • Thank you for using Verifpal. 
$
```

The model was [sent to
VerifHub](https://verifhub.verifpal.com/8834e56e498c673309d0aa435d3f0252) for
everyone to enjoy.

Unfortunately, while being a breeze to use compared to the domain heavyweight
contenders like
[CryptoVerif](https://bblanche.gitlabpages.inria.fr/CryptoVerif/),
[Tamarin](https://tamarin-prover.github.io/),
[Proverif](https://bblanche.gitlabpages.inria.fr/proverif/), … Verifpal has
some shortcomings:

- It [isn't maintained anymore](https://source.symbolic.software/verifpal/verifpal/activity).
- Nadim Kobeissi, the author of Verifpal, who did [his Phd](https://inria.hal.science/tel-01950884) on
  "Formal verification for real-world cryptographic protocols and
  implementations", to put it mildly, doesn't seem to be
  [a](https://twitter.com/LeaKissner/status/1268579266209263622)
  [great](https://storage.courtlistener.com/recap/gov.uscourts.cand.340308/gov.uscourts.cand.340308.27.0.pdf)
  [human](https://web.archive.org/web/20200806001638/https://twitter.com/jilliancyork/status/1290940217000681473)
  [being]( https://twitter.com/isislovecruft/status/1098270385148022784).
  Moreover, his [stupid](https://twitter.com/kaepora/status/1549008483978285063)
  [dunks](https://twitter.com/kaepora/status/1549007373175586818) on [Citizen Lab](https://en.wikipedia.org/wiki/Citizen_Lab)
  ended up being cited in [José Javier Olivas-Osuna's completely phony](https://www.untidy.news/p/fact-check-jose-javier-olivas-osunas)
  [Pegasus report](https://eprints.lse.ac.uk/118492/5/ThePegasusspywarescandal_AcriticalreviewCatalanGate_OlivasOsunaJJ2023.pdf).
- Only constants can be sent between `principal`, meaning that there are a ton of intermediary variables.
- There is no way to add constrains on variables, like `Alice verifies that Bob's gˣ is a legal value (2 ≤ gˣ ≤ modulus-2)`. One could use *guarded constants* like `[g_x]`
  to prevent an active attacker from messing with `gˣ`, but this can't be done
  on function results, like asserting that `g_x` obtained from `DEC(…)` is a
  legal value.
- Some errors are silently ignored, like `SPLIT(SPLIT(CONCAT(…)))` instead of `SPLIT(CONCAT(…))`.
- Multiplications aren't implemented: `gˣ·gʸ` isn't a thing, making it
  impossible to model OTR's [SMP]( https://en.wikipedia.org/wiki/Socialist_millionaire_problem ).