otrv4_nobrace.pv

(* Model of OTRv4
 * Sebastian R. Verschoor
 *
 * Note that we do not model the prekey server, which reflects that it is
 * untrusted: Proverif may arbitrarily model the behaviour of the prekey
 * server.
 *
 * # Flags
 *
 * The file contains options for different models, toggled by preprocessor
 * directives (use `CPP -P` for example to set these). Here I list the flags
 * and what they do.
 *
 * - BRACE: turn the `brace_key` mechanism on and operate under the
 * assumption that Elliptic Curves are broken. Warning: this makes
 * modelchecking very slow.
 *
 * # Inaccuracies of the model
 *
 * Proverif is based on the pi-calculus and can only do so much to accurately
 * model the protocol and cryptographic primitives as specified (let alone
 * implemented). In particular, Proverif assumes perfect cryptographic
 * primitives and cannot handle associativity, but for a more complete
 * discussion of the matter see the [Proverif manual][Proverif]. This is
 * relevant for OTRv4 in at least the following ways:
 * - Diffie-Hellman is only defined relative to the base element.
 * - Hashes (also MAC and KDF) are essentially random oracles.
 *
 * Besides the above unavoidable sources of incompleteness, there are also some
 * diversions from the protocol as [currently specified][OTRv4]:
 * - Each party is assumed to have just one signed prekey.
 * - protocol negotiation/modes: it is assumed that initiator and responder
 * have agreed on this beforehand. Downgrade attacks, for example, are not
 * covered.
 * - nested KDF calls are avoided where cryptographically insignificant
 * - I modelled the protocol with only a single shared key as output. This can
 * and should be used to fully initialize the Double Ratchet.
 * Note: currently [OTRv4] does this differently.
 * - Fingerprint comparison must be modelled at a particular point in time,
 * here done just after the regular protocol completes. In reality, it
 * can be done at any time (preferably beforehand). The alternative (SMP) has
 * not been modelled.
 *
 * Some things may look strange but they should not affect the results:
 * - public data (Client-/Prekey-Profiles) is outputted only once
 * - new values are generated as early as possible, this helps Proverif
 * resolve the model quicker. In general the order of operations does not
 * matter, only the order of sent/received messages.
 * - in reality prekey management is more complicated then is modelled here.
 * However, from the protocol perspective all the server is doing is caching
 * the messages...
 * - signatures are implemented with message recovery directly from the signature.
 * This should improve Proverif performance and does not affect the model since
 * signatures are always computed over publicly known values.
 * - SSID values can be compared, but this is not required to be confidential,
 * this is modelled by simply outputting the value (but actual comparison is
 * considered out of scope).
 *
 * # Phases
 *
 * The phases may seem out-of-order, but this is necessary to model forward secrecy.
 * - Phase 0: model is executed
 * - Phase 1: Long-term keys are leaked
 * - Phase 2: Medium-term keys are leaked
 * - Phase 3: (ECC) short-term keys are leaked
 * In each phase some security properties can no longer be guaranteed. So for example
 * XZDH should provide forward secrecy for the responder after the medium-term
 * keys have been deleted, but before then a device compromise leaks the shared key:
 * in the model we expect thus expect the key to be secret in phase 1, but not in
 * phase 2.
 *
 * # References
 *
 * [Proverif]: http:
 * [OTRv4]: https:
 *)
(* The specification makes sure types cannot be mixed *)
set ignoreTypes = false.
(* Public communication channel *)
channel c.
(* Authenticated channel for fingerprint comparison *)
free ac: channel [private].
(* ECDH: key exchange *)
type ec_point.
type ec_scalar.
fun ec_point_as_bits(ec_point): bitstring [data, typeConverter].
fun ec_base(ec_scalar): ec_point.
fun ec_mul(ec_scalar, ec_point): ec_point.
equation forall x: ec_scalar, y: ec_scalar;
    ec_mul(x, ec_base(y)) = ec_mul(y, ec_base(x)).
(* Channel for delayed leaking of medium-term keys *)
free d_leak: channel [private].
(* EdDSA: digital signatures *)
type eddsa_private_key.
type eddsa_signature.
fun eddsa_scalar(eddsa_private_key): ec_scalar.
letfun eddsa_public_key(x: eddsa_private_key) = ec_base(eddsa_scalar(x)).
fun eddsa_sign(eddsa_private_key, bitstring): eddsa_signature.
reduc forall k: eddsa_private_key, m: bitstring;
    eddsa_get_msg(eddsa_sign(k, m)) = m.
reduc forall k: eddsa_private_key, m: bitstring;
    eddsa_verify(eddsa_sign(k, m), ec_base(eddsa_scalar(k))) = m.
(* Elliptic curve ring signatures (three public keys) *)
type ring_signature.
fun ring_sign(ec_scalar, ec_point, ec_point, bitstring): ring_signature.
reduc forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
    ring_get_msg(ring_sign(k, a, b, m)) = m.
reduc
    forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
        ring_verify(ring_sign(k, a, b, m), ec_base(k), a, b) = m;
    forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
        ring_verify(ring_sign(k, a, b, m), ec_base(k), b, a) = m;
    forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
        ring_verify(ring_sign(k, a, b, m), a, ec_base(k), b) = m;
    forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
        ring_verify(ring_sign(k, a, b, m), a, b, ec_base(k)) = m;
    forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
        ring_verify(ring_sign(k, a, b, m), b, ec_base(k), a) = m;
    forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring;
        ring_verify(ring_sign(k, a, b, m), b, a, ec_base(k)) = m.
(* KDF *)
type tag.
fun kdf(tag, bitstring): bitstring.
(* Domain separating tags: usageID variables, superfluous ones are commented out *)
const usageFingerprint: tag [data].
(* const usageThirdBraceKey: tag [data]. *)
(* const usageBraceKey: tag [data]. *)
const usageSharedSecret: tag [data].
const usageSSID: tag [data].
(* const usageAuthRBobClientProfile: tag [data]. *)
(* const usageAuthRAliceClientProfile: tag [data]. *)
(* const usageAuthRPhi: tag [data]. *)
(* const usageAuthIBobClientProfile: tag [data]. *)
(* const usageAuthIAliceClientProfile: tag [data]. *)
(* const usageAuthIPhi: tag [data]. *)
(* const usageFirstRootKey: tag [data]. *)
const usageTmpKey: tag [data].
const usageAuthMACKey: tag [data].
(* const usageNonIntAuthBobClientProfile: tag [data]. *)
(* const usageNonIntAuthAliceClientProfile: tag [data]. *)
(* const usageNonIntAuthPhi: tag [data]. *)
const usageAuthMAC: tag [data].
(* const usageECDHFirstEphemeral: tag [data]. *)
(* const usageDHFirstEphemeral: tag [data]. *)
(* const usageRootKey: tag [data]. *)
(* const usageChainKey: tag [data]. *)
(* const usageNextChainKey: tag [data]. *)
(* const usageMessageKey: tag [data]. *)
(* const usageMACKey: tag [data]. *)
(* const usageExtraSymmKey: tag [data]. *)
(* const usageDataMessageSections: tag [data]. *)
(* const usageAuthenticator: tag [data]. *)
(* const usageSMPSecret: tag [data]. *)
(* const usageAuth: tag [data]. *)
(* Other constants *)
const zero, one: tag [data].
const fp_dakez_init: tag [data].
const fp_dakez_resp: tag [data].
const fp_xzdh_init: tag [data].
const fp_xzdh_resp: tag [data].
(* Identity of the honest parties (e.g. bare JID) *)
type identity.
free id_alice, id_bob: identity.
(* Fingerprint calculation *)
letfun fingerprint(client_profile: eddsa_signature) =
    kdf(usageFingerprint, eddsa_get_msg(client_profile)).
(* Secrecy assumptions *)
not attacker(new h_a) phase 0.
not attacker(new h_b) phase 0.
not attacker(new f_a) phase 0.
not attacker(new f_b) phase 0.
not attacker(new d_a) phase 1.
not attacker(new d_b) phase 1.
not attacker(new d_a) phase 1.
not attacker(new d_b) phase 1.
not attacker(new y_dakez) phase 2.
not attacker(new x_dakez) phase 2.
not attacker(new y_xzdh) phase 2.
not attacker(new x_xzdh) phase 2.
(* Queries *)
(* Correctness queries (can honest participants complete the protocol?):
 * we want "RESULT not event(correct) is false."
 *)
event correct_dakez_init.
event correct_dakez_resp.
event correct_xzdh_init.
event correct_xzdh_resp.
query event(correct_dakez_init).
query event(correct_dakez_resp).
query event(correct_xzdh_init).
query event(correct_xzdh_resp).
(* Secrecy queries: these remain secure in any phase *)
query secret k_dakez_init;
      secret k_dakez_resp;
      secret k_xzdh_init.
(* Proverif does not allow a query with a combination of "secret" and "phase",
 * so we use a common trick using encryption to prove secrecy of a bound value
 * using a free value.
 *)
fun enc(bitstring, bitstring): bitstring.
reduc forall key: bitstring, msg: bitstring; dec(key, enc(key, msg)) = msg.
free k_xzdh_resp: bitstring [private].
query attacker(k_xzdh_resp) phase 1.
(* Check for correctness of the model: in phase 2 we expect the key to leak *)
query attacker(k_xzdh_resp) phase 2.
(* Authentication queries *)
event accept_dakez_resp(identity, identity, bitstring).
event term_dakez_init(identity, identity, bitstring).
event accept_dakez_init(identity, identity, bitstring).
event term_dakez_resp(identity, identity, bitstring).
event accept_xzdh_resp(identity, identity, bitstring).
event term_xzdh_init(identity, identity, bitstring).
query id1: identity, id2: identity, k: bitstring;
    inj-event(term_dakez_init(id1, id2, k))
    ==> inj-event(accept_dakez_resp(id1, id2, k)).
query id1: identity, id2: identity, k: bitstring;
    inj-event(term_dakez_resp(id1, id2, k))
    ==> inj-event(accept_dakez_init(id1, id2, k)).
query id1: identity, id2: identity, k: bitstring;
    inj-event(term_xzdh_init(id1, id2, k))
    ==> inj-event(accept_xzdh_resp(id1, id2, k)).
(* Note: No authentication for Initiator in XZDH *)
(* Processes *)
(* DAKEZ: Initiator *)
let dakez_init(cp_a: eddsa_signature, h_a: eddsa_private_key, F_a: ec_point, cp_b: eddsa_signature, h_b:eddsa_private_key, F_b: ec_point) =
    (* Generate new values ASAP *)
    new y_dakez: ec_scalar;
    (* Let the adversary set the (honest) identity of the initiator *)
    in(c, id_i: identity);
    let (cp_i: eddsa_signature, h_i: eddsa_private_key, F_i: ec_point) = if id_i = id_alice then
        (cp_a, h_a, F_a)
    else if id_i = id_bob then
        (cp_b, h_b, F_b)
    in
    (* Real start of the role *)
    let Y = ec_base(y_dakez) in
    out(c, Y);
    in(c, sigma_r: ring_signature);
    let (=zero, =cp_i, cp_r: eddsa_signature, =Y, X: ec_point, =id_i, id_r: identity) = ring_get_msg(sigma_r) in
    let (H_r: ec_point, F_r: ec_point) = eddsa_get_msg(cp_r) in
    let (=H_r, =F_r) = eddsa_verify(cp_r, H_r) in
    let (=zero, =cp_i, =cp_r, =Y, =X, =id_i, =id_r) = ring_verify(sigma_r, H_r, F_i, Y) in
    let t_i = (one, cp_i, cp_r, Y, X, id_i, id_r) in
    let k = kdf(usageSharedSecret, ec_point_as_bits(ec_mul(y_dakez, X))) in
    event term_dakez_init(id_i, id_r, k);
    let ssid = kdf(usageSSID, k) in out(c, ssid);
    let sigma_i = ring_sign(eddsa_scalar(h_i), F_r, X, t_i) in
    event accept_dakez_init(id_i, id_r, k);
    out(c, sigma_i);
    (* Compare fingerprints *)
    out(ac, (fp_dakez_init, fingerprint(cp_i)));
    in(ac, (=fp_dakez_resp, =fingerprint(cp_r)));
    (* Security for the honest participants *)
    if id_r = id_alice || id_r = id_bob then
    event correct_dakez_init;
    let k_dakez_init = k in
    0.
(* DAKEZ: Responder *)
let dakez_resp(cp_a: eddsa_signature, h_a: eddsa_private_key, F_a: ec_point, cp_b: eddsa_signature, h_b: eddsa_private_key, F_b: ec_point) =
    (* Generate new values ASAP *)
    new x_dakez: ec_scalar;
    (* Let the adversary set the (honest) identity of the responder *)
    in(c, id_r: identity);
    let (cp_r: eddsa_signature, h_r: eddsa_private_key, F_r: ec_point) = if id_r = id_alice then
        (cp_a, h_a, F_a)
    else if id_r = id_bob then
        (cp_b, h_b, F_b)
    in
    (* Real start of the role *)
    in(c, (id_i: identity, cp_i: eddsa_signature, Y: ec_point));
    let (H_i: ec_point, F_i: ec_point) = eddsa_get_msg(cp_i) in
    let (=H_i, =F_i) = eddsa_verify(cp_i, H_i) in
    let X = ec_base(x_dakez) in
    let t_r = (zero, cp_i, cp_r, Y, X, id_i, id_r) in
    let k = kdf(usageSharedSecret, ec_point_as_bits(ec_mul(x_dakez, Y))) in
    let ssid = kdf(usageSSID, k) in out(c, ssid);
    let sigma_r = ring_sign(eddsa_scalar(h_r), F_i, Y, t_r) in
    event accept_dakez_resp(id_i, id_r, k);
    out(c, sigma_r);
    in(c, sigma_i: ring_signature);
    let (=one, =cp_i, =cp_r, =Y, =X, =id_i, =id_r) = ring_verify(sigma_i, H_i, F_r, X) in
    event term_dakez_resp(id_i, id_r, k);
    (* Compare fingerprints *)
    in(ac, (=fp_dakez_init, =fingerprint(cp_i)));
    out(ac, (fp_dakez_resp, fingerprint(cp_r)));
    (* Security for honest participants *)
    if id_i = id_alice || id_i = id_bob then
    event correct_dakez_resp;
    let k_dakez_resp = k in
    0.
(* XZDH: Initiator (uploads the prekey) *)
let xzdh_init(cp_a: eddsa_signature, h_a: eddsa_private_key, F_a: ec_point, d_a: ec_scalar, cp_b: eddsa_signature, h_b: eddsa_private_key, F_b: ec_point, d_b: ec_scalar) =
    (* Generate new values ASAP *)
    new y_xzdh: ec_scalar;
    (* Let the adversary set the (honest) identity of the responder *)
    in(c, id_i: identity);
    let (cp_i: eddsa_signature, h_i: eddsa_private_key, F_i: ec_point, d: ec_scalar) = if id_i = id_alice then
        (cp_a, h_a, F_a, d_a)
    else if id_i = id_bob then
        (cp_b, h_b, F_b, d_b)
    in
    (* Prekey part, cached by the Prekey server together with D *)
    let Y = ec_base(y_xzdh) in
    out(c, Y);
    (* Remainder of the role *)
    in(c, (sigma: ring_signature, xzdh_mac: bitstring));
    let t = ring_get_msg(sigma) in
    let (=cp_i, cp_r: eddsa_signature, =Y, X: ec_point, =ec_base(d), =id_i, id_r: identity) = t in
    let (H_r: ec_point, F_r: ec_point) = eddsa_get_msg(cp_r) in
    let (=H_r, =F_r) = eddsa_verify(cp_r, H_r) in
    let (=cp_i, =cp_r, =Y, =X, =ec_base(d), =id_i, =id_r) = ring_verify(sigma, H_r, F_i, Y) in
    let k_tmp = kdf(usageTmpKey, (ec_mul(y_xzdh, X), ec_mul(d, X), ec_mul(eddsa_scalar(h_i), X))) in
    let xzdh_mac_key = kdf(usageAuthMACKey, k_tmp) in
    if xzdh_mac = kdf(usageAuthMAC, (xzdh_mac_key, t)) then
    let k = kdf(usageSharedSecret, k_tmp) in
    let ssid = kdf(usageSSID, k) in out(c, ssid);
    event term_xzdh_init(id_i, id_r, k);
    (* Compare fingerprints *)
    out(ac, (fp_xzdh_init, fingerprint(cp_i)));
    in(ac, (=fp_xzdh_resp, =fingerprint(cp_r)));
    (* Security for honest participants *)
    if id_r = id_alice || id_r = id_bob then
    event correct_xzdh_init;
    let k_xzdh_init = k in
    0.
(* XZDH: Responder *)
let xzdh_resp(cp_a: eddsa_signature, h_a: eddsa_private_key, cp_b: eddsa_signature, h_b: eddsa_private_key) =
    (* Generate new values ASAP *)
    new x_xzdh: ec_scalar;
    (* Let the adversary set the (honest) identity of the responder *)
    in(c, id_r: identity);
    let (cp_r: eddsa_signature, h_r: eddsa_private_key) = if id_r = id_alice then
        (cp_a, h_a)
    else if id_r = id_bob then
        (cp_b, h_b)
    in
    (* Real start of the role *)
    in(c, (id_i: identity, cp_i: eddsa_signature, pkp: eddsa_signature, Y: ec_point));
    let (H_i: ec_point, F_i: ec_point) = eddsa_get_msg(cp_i) in
    let (=H_i, =F_i) = eddsa_verify(cp_i, H_i) in
    let ec_point_as_bits(D) = eddsa_verify(pkp, H_i) in
    let X = ec_base(x_xzdh) in
    let k_tmp = kdf(usageTmpKey, (ec_mul(x_xzdh, Y), ec_mul(x_xzdh, D), ec_mul(x_xzdh, H_i))) in
    let t = (cp_i, cp_r, Y, X, D, id_i, id_r) in
    let k = kdf(usageSharedSecret, k_tmp) in
    let ssid = kdf(usageSSID, k) in out(c, ssid);
    let sigma = ring_sign(eddsa_scalar(h_r), F_i, Y, t) in
    let xzdh_mac_key = kdf(usageAuthMACKey, k_tmp) in
    let xzdh_mac = kdf(usageAuthMAC, (xzdh_mac_key, t)) in
    event accept_xzdh_resp(id_i, id_r, k);
    out(c, (sigma, xzdh_mac));
    (* Compare fingerprints *)
    in(ac, (=fp_xzdh_init, =fingerprint(cp_i)));
    out(ac, (fp_xzdh_resp, fingerprint(cp_r)));
    (* Security for the honest participants *)
    if id_i = id_alice || id_i = id_bob then
    event correct_xzdh_resp;
    out(c, enc(k, k_xzdh_resp));
    0.
(* The main process. The idea is to generate two honest parties (Alice and Bob)
 * and let both execute both roles (initiator and responder) in both protocols
 * (XZDH and DAKEZ). The adversary can then execute and complete arbitrary many
 * protocol runs with either party in any role, however we only expect security
 * in case it was an interaction between the two honest parties.
 *)
process
    (* Generate the honest parties Client Profiles *)
    new h_a: eddsa_private_key; let H_a = eddsa_public_key(h_a) in
    new f_a: ec_scalar; let F_a = ec_base(f_a) in
    let cp_a = eddsa_sign(h_a, (H_a, F_a)) in
    new h_b: eddsa_private_key; let H_b = eddsa_public_key(h_b) in
    new f_b: ec_scalar; let F_b = ec_base(f_b) in
    let cp_b = eddsa_sign(h_b, (H_b, F_b)) in
    out(c, (cp_a, cp_b));
    (* Generate the honest parties Prekey Profiles *)
    new d_a: ec_scalar; let D_a = ec_base(d_a) in
    let pkp_a = eddsa_sign(h_a, ec_point_as_bits(D_a)) in
    new d_b: ec_scalar; let D_b = ec_base(d_b) in
    let pkp_b = eddsa_sign(h_b, ec_point_as_bits(D_b)) in
    out(c, (pkp_a, pkp_b));
    (
        (!dakez_init(cp_a, h_a, F_a, cp_b, h_b, F_b)) |
        (!dakez_resp(cp_a, h_a, F_a, cp_b, h_b, F_b)) |
        (*
        (!(
            new d_b: ec_scalar; let D_b = ec_base(d_b) in
            let pkp_b = eddsa_sign(h_b, ec_points_as_bits(D_b) in
            out(c, pkp_b);
            out(d_leak, d_b);
            !xzdh_init(id_bob, cp_b, h_b, d_b, F_b)
        ) |
        (!(
            new d_a: ec_scalar; let D_a = ec_base(d_a) in
            let pkp_a = eddsa_sign(h_a, ec_points_as_bits(D_a) in
            out(c, pkp_a);
            out(d_leak, d_a);
            !xzdh_init(id_alice, cp_a, h_a, d_a, F_a)
        ) |
        *)
        (!xzdh_init(cp_a, h_a, F_a, d_a, cp_b, h_b, F_b, d_b)) |
        (!xzdh_resp(cp_a, h_a, cp_b, h_b)) |
        (* Make ac non-confidential *)
        (!(in(ac, x: bitstring); out(c, x); out(ac, x))) |
        (* Reveal long-term secret values *)
        (phase 1; out(c, (h_a, f_a, h_b, f_b))) |
        (* Reveal medium-term secret values *)
        (* (!(in(d_leak, d: ec_scalar); phase 2; out(c, d))) *)
        (phase 2; out(c, (d_a, d_b)))
    )