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:
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 gets merged.):
// 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
]
$ 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 for everyone to enjoy.
Unfortunately, while being a breeze to use compared to the domain heavyweight contenders like CryptoVerif, Tamarin, Proverif, … Verifpal has some shortcomings:
- It isn't maintained anymore.
- Nadim Kobeissi, the author of Verifpal, who did his Phd on "Formal verification for real-world cryptographic protocols and implementations", to put it mildly, doesn't seem to be a great human being. Moreover, his stupid dunks on Citizen Lab ended up being cited in José Javier Olivas-Osuna's completely phony Pegasus report.
- 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 withgˣ, but this can't be done on function results, like asserting thatg_xobtained fromDEC(…)is a legal value. - Some errors are silently ignored, like
SPLIT(SPLIT(CONCAT(…)))instead ofSPLIT(CONCAT(…)). - Multiplications aren't implemented:
gˣ·gʸisn't a thing, making it impossible to model OTR's SMP.