// Violation of forward secrecy without prekey signing
// closely follows: https://gitlab.matrix.org/matrix-org/olm/blob/master/docs/olm.md
// signage is discussed here: https://gitlab.matrix.org/matrix-org/olm/-/blob/master/docs/signing.md
attacker[active]

principal Bob[
    // initialize private key, ot key
    generates bob_private, bob_ot_private
    bob_ot_public = G^bob_ot_private
    bob_public = G^bob_private
]

Bob -> Alice: [bob_public], bob_ot_public

principal Alice[
    // initialize private key, ot key
    generates alice_private, alice_ot_private
    alice_ot_public = G^alice_ot_private
    alice_public = G^alice_private

    knows public c0, c1, c2, c3, c4

    k1a = bob_public^alice_private
    k2a = bob_ot_public^alice_private
    k3a = bob_public^alice_ot_private

    // derive the master secret
    sa = HASH(k1a, k2a, k3a, bob_public, alice_public)

    // create the root and chain key from the 3DH'ed secret
    ra1, ca1 = HKDF(sa, c1, c2)
    
    // create ratchet key
    generates ta1_private
    ta1_public = G^ta1_private
    ta1_sig = SIGN(alice_private, ta1_public)

    // computing the first message key
    mak1 = MAC(ca1, c3)

    // ciphertext
    generates ma1
    xa1 = AEAD_ENC(mak1, ma1, CONCAT(alice_public, bob_public))

    // signage not specified
    xa1_sig = SIGN(alice_private, xa1)
]

// in the implementation we'd include a chain index, but since this is a model we do not
Alice -> Bob: [alice_public], alice_ot_public, ta1_public, ta1_sig, xa1, xa1_sig

principal Bob[
    _ = SIGNVERIF(alice_public, xa1, xa1_sig)
    _ = SIGNVERIF(alice_public, ta1_public, ta1_sig)?

    k1b = alice_public^bob_private
    k2b = alice_public^bob_ot_private
    k3b = alice_ot_public^bob_private

    // derive master
    knows public c0, c1, c2, c3, c4
    sb = HASH(k1b, k2b, k3b, bob_public, alice_public)

    // derive root and chain
    rb1, cb1 = HKDF(sb, c1, c2)

    // create bob's initial message key
    mbk1 = MAC(cb1, c3)

    // decrypt
    mb1 = AEAD_DEC(mbk1, xa1, CONCAT(alice_public, bob_public))

    // now, bob wants to send a message back and advances the ratchet

    // generate new ratchet key
    generates tb2_private
    tb2_public = G^tb2_private
    tb2_sig = SIGN(bob_private, tb2_public)

    // advance the ratchet using prev root key, other ratchet stuff
    rb2, cb2 = HKDF(MAC(rb1, c3), ta1_public^tb2_private, c3)

    // create message key
    mbk2 = MAC(cb2, c3)

    // ciphertext
    generates mb2
    xb2 = AEAD_ENC(mbk2, mb2, CONCAT(alice_public, bob_public))

    // signage not specified
    xb2_sig = SIGN(bob_private, xb2)
]

Bob -> Alice: xb2, xb2_sig, tb2_public, tb2_sig

principal Alice[
    _ = SIGNVERIF(bob_public, xb2, xb2_sig)?
    _ = SIGNVERIF(bob_public, tb2_public, tb2_sig)?
    // derive new root key
    ra2, ca2 = HKDF(MAC(ra1, c3), tb2_public^ta1_private, c3)

    // derive new message key from the chain key
    mak2 = MAC(ca2, c3)

    // decrypt
    ma2 = AEAD_DEC(mak2, xb2, CONCAT(alice_public, bob_public))
]

// phase[1]
principal Bob[leaks bob_private]
// principal Alice[leaks alice_private]

// first two queries violate, while the second two do not
// first two queries take a few seconds to violate, while the second two
// take a full exploration to confirm
queries[
    // confidentiality? ma1
    // authentication? Alice -> Bob: xa1
    confidentiality? ma2
    // authentication? Bob -> Alice: xb2
]