(*
 * Formal definition to verify the Fenrir protocol.
 * to be used with ProVerif
 *
 * Here we check the security of the connection between client
 * and service in the case of a compromised authentication server
 *)

(*
 * ==============
 * Type definition
 * ==============
 *)

type pubKey.    (* public  key for asymmetric key encryption *)
type privKey.   (* private key for asymmetric key encryption *)
type sKey.	(* symmetric key *)
type nonce.	(* just a nonce *)

const cs: channel. (* simulates service-fenrir channel for authentication *)

(* various stuff that should remain private *)
const prS:       privKey   [private]. (* service private key *)
free csKey:      sKey      [private].
free shared:      sKey      [private].


(*
 * ==============
 * Function definition
 * ==============
 *)

(* key to bitstring conversion *)
fun fromKey(sKey) : bitstring.
reduc forall a : sKey; toKey(fromKey(a)) = a.


(* symmetric key encription *)
fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *)
reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *)

(* public key definition *)
fun genPub(privKey): pubKey.    (* public keys are generated from private ones *)
(* public key signing *)
fun sign(bitstring, privKey): bitstring.
reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *)

(* some key exchange based on public keys *)
fun exchange(privKey, pubKey) : sKey.
equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)).

(* hash used by OTP, sKey based *)
fun hash(sKey) : sKey.

(* xor function *)
(* note: this xor function doe not handle associativity as proverif would loop,
 * so we pay attention to use it in a way that does not require associativity
 *)
fun xor(sKey, sKey) : sKey.
reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a.
reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *)


(*
 * ==============
 * Events -- used for correlation
 * ==============
 *)
event clientConnect(sKey).
event serviceConnect(sKey).


(* rekeying algorithm *)

let client_rekey (key: sKey, chan: channel, pb : pubKey) =
    new rekey_p1: privKey;
    new rekey_n1: nonce;
    out (chan, sEnc((rekey_n1, genPub(rekey_p1)), key));
    in  (chan, enc: bitstring);
    let (=rekey_n1, srv_eph : pubKey, signed : bitstring) = sDec(enc, key) in
    if ver((rekey_n1, srv_eph), signed, pb) then
    let (new_Key) = exchange(rekey_p1, srv_eph) in
    out (chan, sEnc((shared, shared), new_Key)) (* test secrecy *)
    .

let server_rekey (key: sKey, chan: channel, pr : privKey) =
    new rekey_s_p: privKey;
    in  (chan, enc: bitstring);
    let (client_n1: nonce, client_p: pubKey) = sDec (enc, key) in
    out (chan, sEnc((client_n1, genPub(rekey_s_p), sign((client_n1, genPub(rekey_s_p)), pr)), key));
    let (new_Key) = exchange(rekey_s_p, client_p) in
    in (chan, enc2: bitstring);
    let (=shared, =shared) = sDec(enc2, new_Key)
    .


(* test the connection between the service and client. Assume that the authentication server
 * has been compromised. *)


let service_shared() =
    let xored = xor(csKey, shared) in
    out (cs, xored);
	in (cs, enc : bitstring);
	let data = sDec(enc, csKey) in
    if data = fromKey(shared) then
	event clientConnect(csKey);
    server_rekey(csKey, cs, prS).

let client_shared(pbS: pubKey) =
    in (cs, xored : sKey);
    let xorKey = unxor(xored, shared) in
	event serviceConnect(xorKey);
    out (cs, sEnc(fromKey(shared), xorKey)); (* test 'shared' secrecy *)
    client_rekey(xorKey, cs, pbS).


(* assume that the client and service have not yet setup a shared secret *)
(* DATA is the secret data *)

let service_no_shared() =
    in (cs, pbC : pubKey);
    let shared2 = exchange(prS, pbC) in
    let xored = xor(csKey, shared2) in
    out (cs, xored);
	in (cs, enc : bitstring);
	let data = sDec(enc, csKey) in
    if data = fromKey(shared) then
	event clientConnect(csKey);
    server_rekey(csKey, cs, prS).

let client_no_shared(pbS: pubKey) =
    new prC : privKey;
    out (cs, genPub(prC));
    let shared2 = exchange(prC, pbS) in
    in (cs, xored : sKey);
    let xorKey = unxor(xored, shared2) in
	event serviceConnect(xorKey);
    out (cs, sEnc(fromKey(shared), xorKey)); (* test 'shared' secrecy *)
    client_rekey(xorKey, cs, pbS).


(* assume that the client and service have not yet setup a shared secret *)
(* DATA is the secret data *)

(*
 * Event correlation:
 *)
query k : sKey; event(clientConnect(k)) ==> event(serviceConnect(k)).

(*
 * ==============
 * What should be secret?
 * ==============
 *)

query attacker(shared).	(* client-service shared key. *)
query attacker(csKey).	(* client-service key. *)

(*
 * ==============
 * Run the verification
 * ==============
 *)

(* make it easy to deactivate single parts, like the 2-RTT login, which has unproven events problems *)

process
    (!service_no_shared()) | (!client_no_shared(genPub(prS)))
      | phase 1; (!service_shared()) | (!client_shared(genPub(prS)))