(*
  3DH MUTUAL DENIABILITY
  Author: [redacted]

  model assumption #1: same key is used for signing and encryption (i.e. X25519)
*)

free m1: bitstring [private].

set selFun = Nounifset.   
set simplifyProcess = false.
(*
set simpEqAll = false. 
set redundancyElim = best.
set redundantHypElim = true.  
set simplifyProcess = true.
set stopTerm = false.
*)

free c: channel.
free a: channel. (* channel for the attacker *)
free p: channel [private]. (* For the distribution of public keys with integrity and authenticity - verification happens out of band. This is a standard assumption. *)

(* Symmetric key encryption *)

type key.

fun senc(key, bitstring): bitstring.
reduc forall m: bitstring, k: key; sdec(k, senc(k,m)) = m.

(* Asymmetric key encryption *)

type skey.
type pkey.

fun rb(pkey): bitstring.
fun pk(skey): pkey.

(* Digital signatures *)

fun sign(skey, bitstring): bitstring.
fun okay():bitstring.
reduc forall m: bitstring, sk: skey; checksign(pk(sk), m, sign(sk, m)) = okay.

(* MACs *)
fun mac(key, bitstring): bitstring.
reduc forall k: key, m: bitstring; checkmac(k, m, mac(k, m)) = okay.

(* Diffie-Hellman *)
(* DH -> Public^Private *)

fun dh(pkey, skey): key.
equation forall a: skey, b: skey; dh(pk(a), b) = dh(pk(b), a). (* symmetry of DH *)

(* the concat functions *)
fun hkdf1(key, key, key): key [data].

fun khash(key): key.

fun hkdf2_dev1(key): key.
fun hkdf2_dev2(key): key.
letfun hkdf2(k: key) =
  (hkdf2_dev1(k), hkdf2_dev2(k)).

(* the concats *)

fun concat1(bitstring, pkey): bitstring [data].

(* events *)
event sendE1(bitstring, key, pkey).
event recvE1(bitstring, key, pkey).

event compromiseSKA(skey).

event compromiseSKB(skey).

event start().

let PeerA(SK_A: skey, PK_A: pkey, PK_B: pkey) =
  phase 1;

  new ao: skey;
  let gao = pk(ao) in

  (* generate amaster and enc msg (PHASE 1) *)

  (* in(c, gbo: pkey); *)
  in(c, (gbo: pkey, gbo_sig: bitstring));
  if checksign(PK_B, rb(gbo), gbo_sig) = okay then (  
  
  let amaster = hkdf1(dh(PK_B, SK_A), dh(gbo, SK_A), dh(PK_B, ao)) in
  let (ra1: key, ca1: key) = hkdf2(amaster) in (* derive the root and chain key *)

  let mak1 = khash(ca1) in
  let (mak1_auth: key, mak1_enc: key) = hkdf2(mak1) in

  let x1 = senc(mak1_enc, m1) in 
  let x1_mac = mac(mak1_auth, concat1(x1, gao)) in
  event sendE1(m1, mak1, gao);

  phase 2;

  out(c, (x1, x1_mac, gao))

  ).

let PeerB(SK_B: skey, PK_B: pkey, PK_A: pkey) =
  new bo: skey;

  let gbo = pk(bo) in
  let gbo_sig = sign(SK_B, rb(gbo)) in

  out(c, (gbo, gbo_sig)); 
  phase 1;

   (* first stage: derive bmaster, verfiy a's msgs, decrypt prekey message, reply *)

  in(c, (x1: bitstring, x1_mac: bitstring, gao: pkey)); 

  let bmaster = hkdf1(dh(PK_A, SK_B), dh(PK_A, bo), dh(gao, SK_B)) in
  let (rb1: key, cb1: key) = hkdf2(bmaster) in (* derive the root and chain key *)

  let mbk1 = khash(cb1) in
  let (mbk1_auth: key, mbk1_enc: key) = hkdf2(mbk1) in
  if checkmac(mbk1_auth, concat1(x1, gao), x1_mac) = okay then 
  (
    let m1 = sdec(mbk1_enc, x1) in 
    event recvE1(m1, mbk1, gao);

    phase 2;
    event compromiseSKB(SK_B);
    out(c, SK_B)

  ).

(*

query event(start()). (* reachable from all possible executions *)

(* auth *)
query m: bitstring, rk: key, k1: pkey; inj-event(recvE1(m, rk, k1)) ==> inj-event(sendE1(m, rk, k1)).

(* secrecy *)

query attacker(m1). 

(* reachability *) 
query m: bitstring, rk: key, k1: pkey; event(recvE1(m, rk, k1)). (* reachable from all executions *)
query m: bitstring, rk: key, k1: pkey; event(sendE1(m, rk, k1)). (* reachable from all executions *)
*)

process
  new SK_A: skey; let PK_A = pk(SK_A) in 
  new SK_B: skey; let PK_B = pk(SK_B) in

  out(a, PK_A);
  out(a, PK_B);

  new fib1: skey;
  new fib2: skey;
  let k_A = choice [ SK_A, fib1 ] in
  let k_B = choice [ SK_B, fib2 ] in

  event start();
  ( (PeerA(SK_B, PK_A, pk(k_B))) |
    (PeerB(k_B, pk(k_B), PK_A)) | 
    out(a, m1))