(*
 * Formal definition to verify the Fenrir protocol.
 * to be used with ProVerif
 *
 * This is to verify the correctness of the full 3-RTT handshake.
 * DNSSEC is NOT verified, as it is assumed to be correct.
 *
 * The test *WILL* take a while... proverif says it has inserted more than 23k rules, and has a rule base of more than 12k rules.
 * just leave it to work...
 *)

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


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

const leak: channel. (* to leak private material *)
const cf_full: channel. (* client-fenrir, full-security handshake  *)
const cf_state: channel. (* client-fenrir, stateful handshake  *)
const cf_dir: channel. (* client-fenrir, directory-synchronized handshake *)
const cs: channel. (* client-service *)
const sf: channel [private]. (* service-fenrir: since it is managed as the client-fenrir channel, this is not checked *)
const C, F, S: host. (* Client, Fenrir, Service *)

(* various stuff that should remain private *)
const leakCheck: bitstring [private].
const Auth:      nonce     [private].
const prF:       privKey   [private].
const prF_dir:   privKey   [private].
free fsKey:      sKey      [private].

free Rekey:    bitstring. (* rekey message *)
type algorithm.
const alg_bad:  algorithm. (* broken key exchange algorithm *)
const alg_good: algorithm. (* good key exchange algorithm *)
const alg_both: algorithm. (* both good and bad algorithms support*)

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

(* 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 *)
fun aEnc(bitstring, pubKey): bitstring. (* encrypt with asymmetric public key *)
reduc forall c: bitstring, k: privKey; aDec(aEnc(c,genPub(k)),k) = c. (* decrypt with private key *)
(* public key signing *)
fun sign(bitstring, privKey): bitstring.
reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *)
(* integrity for encrypt then mac *)
fun int(bitstring, sKey): bitstring.
reduc forall c: bitstring, k: sKey; verint(c, int(c, k), k) = true.

(* 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)).



(*
 * ==============
 * Events -- used for correlation
 * ==============
 *)
event downgrade().
event acceptedClient(host, sKey).
event acceptedFenrir(host, sKey).
event acceptedClientState(host, sKey).
event acceptedFenrirState(host, sKey).
event clientConnect(host, host, sKey).
event serviceConnect(host, host, sKey).



(* Deactivated because the complexity explodes...
let client_rekey (key: sKey, chan: channel) =
	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) = sDec(enc, key) in
	let (new_Key) = exchange(rekey_p1, srv_eph) in 
	out (chan, sEnc((Auth, Auth), new_Key))
	.

let server_rekey (key: sKey, chan: channel) =
	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)), key));
	let (new_Key) = exchange(rekey_s_p, client_p) in 
	in (chan, enc2: bitstring);
	let (=Auth, =Auth) = sDec(enc2, new_Key)
	.
*)

(*
 * ==========================================================================
 * Client definition, Full-security handshake with good and broken algorithms
 * ==========================================================================
 *)

let client_full(pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce, supported: algorithm) =
	new cn1: nonce; (* Client Nonce 1 *)
	new prC: privKey;

	(* Note: this nonce is technically useless, but prevents amplification/DoS attack
	 * also: the nonce should include a timer, but proverif doesn't check for DoS,
	 * and doesn't play nicely with timers, so we don't really care...
	 *)
(* start cookie exchange *)
	out (cf_full, (client, cn1, supported));
	in  (cf_full, (sn1: nonce, selected: algorithm, s1: bitstring, s2: bitstring));
	if ver((sn1, cn1, supported, selected), s1, pubF) = true then
	if ver((sn1, selected), s2, pubF) = true then

(* RTT 1 completed *)

	(* start algorithm agreement *)
	new cn2: nonce;
	(* out: nonces and signature, supported_algorithms *)
	(* bad algorithm somehow exposes authentication data *)
	if selected = alg_bad && (supported = alg_both || supported = alg_bad) then
	(
		event downgrade()
	)
	else
	(
		if selected = alg_good then
		out (cf_full, (sn1, selected, s2, cn2, genPub(prC)));
		(* se1: server encrypt 1: contains supported authentication algorithms
		 * unused here, it's the same mechanism as the "selected" one
		 *)
		in  (cf_full, (ephF: pubKey, se1: bitstring, s3: bitstring));
		if ver((ephF, se1), s3, pubF) = true then
		let (cfKey) = exchange(prC, ephF) in
(* RTT 2 Completed *)
		out (cf_full, (sEnc((Auth, Auth), cfKey)));
		in  (cf_full, (se2: bitstring));
		let (chan: channel, csKey: sKey) = sDec(se2, cfKey) in
		event acceptedClient(client, cfKey);

(* RTT 3 completed, can now connect to service *)
(* also send private data to test secrecy *)

		event clientConnect(service, client, csKey);
		out (chan, sEnc((Auth, Auth), csKey))
	).

(* now rekey *)

(*
 * ===========================================================================
 * Fenrir definition, full security handshake, with good and broken algorithms
 * ===========================================================================
 *)

let fenrir_full(privF: privKey, fenrir: host, service: host, Auth: nonce, supported: algorithm) =
	(*
	 * NOTE: we do not model the service <-> fenrir authentication, as that is just the same
	 * as the fenrir <-> client full security  authentication. We assume fenrir and service already share a key
	 *)

	(* Nonce exchange *)
	in (cf_full, (client: host, fin1: nonce, client_alg: algorithm));
	new s_nonce: nonce;
	(* triggers "event downgrade()" in the client, no need to go further *)
		(* bad only if both support bad *)
	if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then
	(
		out (cf_full, (s_nonce, alg_bad, sign((s_nonce, fin1, client_alg, alg_bad), privF),
										 sign((s_nonce, alg_bad), privF)))
	)
	else
	(
		if client_alg = alg_good || client_alg = alg_both then
		out (cf_full, (s_nonce, alg_good, sign((s_nonce, fin1, client_alg, alg_good), privF),
										 sign((s_nonce, alg_good), privF)));
(* RTT 1 finished *)
		in (cf_full, (=s_nonce, =alg_good, signed: bitstring, fin2: nonce, pubC: pubKey));
		if ver((s_nonce, alg_good), signed, genPub(privF)) = true then
		new prF2: privKey;
		let (cfKey) = exchange(prF2, pubC) in
		out (cf_full, (genPub(prF2), sEnc((supported, supported), cfKey), sign((genPub(prF2), sEnc((s_nonce, s_nonce), cfKey)), privF)));
(* RTT 2 finished, now we have a state *)
		in (cf_full, (ce1: bitstring));
		let (data: nonce, data2: nonce) = sDec(ce1, cfKey) in
		if data = Auth && data2 = Auth then
		new csKey: sKey;
		out (sf, (client, csKey)); (* inform service of new client *)
		event acceptedFenrir(client, cfKey);
		let (se1) = sEnc((cs, csKey), cfKey) in
		out (cf_full, (sEnc((cs, csKey), cfKey)))
(* RT3 finished *)
	).

(*
 * ==================================
 * Service definition, common for all
 * ==================================
 *)

let service(service: host) =
	in (sf, (cli: host, csKey:sKey));
	in (cs, enc2 : bitstring);
	let (Auth1 : nonce, Auth2 : nonce) = sDec(enc2, csKey) in
	event serviceConnect(service, cli, csKey).


(*
 * ======================================================================
 * Client Definition, Stateful handshake, with good and broken algorithms
 * ======================================================================
 *)

let client_state (pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce, supported: algorithm) =
	new cn1: nonce; (* Client Nonce 1 *)
	new prC: privKey;

	(* Note: this nonce is technically useless, but prevents amplification/DoS attack
	 * also: the nonce should include a timer, but proverif doesn't check for DoS,
	 * and doesn't play nicely with timers, so we don't really care...
	 *)
(* start cookie exchange *)
	out (cf_state, (cn1, client, supported));
	in  (cf_state, (alg: algorithm, ephF: pubKey, s1: bitstring));
	if ver((cn1, client, supported, alg, ephF), s1, pubF) = true then

(* RTT 1 completed *)

	if alg = alg_bad then
	(
		if supported = alg_bad || supported = alg_both then
		(* bad algorithm exposes authentication data *)
		event downgrade()
	)
	else
	(
		if alg = alg_good then
		if supported = alg_good || supported = alg_both then

		let (cfKey) = exchange(prC, ephF) in
		out (cf_state, (genPub(prC), sEnc((Auth,Auth), cfKey)));
		in  (cf_state, enc: bitstring);
		let (chan : channel, csKey : sKey) = sDec(enc, cfKey) in
		event acceptedClientState(client, csKey);
	
(* RTT 2 completed, can now connect to service *)
(* also send private data to test secrecy *)

		event clientConnect(service, client, csKey);
		out (chan, sEnc((Auth, Auth), csKey))
	).

(*
 * ===========================================================================
 * Fenrir definition, stateful handshake, with good and broken algorithms
 * ===========================================================================
 *)

let fenrir_state (privF: privKey, fenrir: host, service: host, Auth: nonce, supported: algorithm) =
	(*
	 * NOTE: we do not model the service <-> fenrir authentication, as that is just the same
	 * as the fenrir <-> client full-securoty authentication. We assume fenrir and service already share a key
	 *)

	(* Nonce exchange *)
	new prF2 : privKey;
	new s_nonce: nonce;
	in (cf_state, (fin1: nonce, client: host, client_alg: algorithm));
	if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then
	(
		out(cf_state, (alg_bad, genPub(prF2), sign((fin1, client, client_alg, alg_bad, genPub(prF2)), privF)))
	)
	else
	(
		if (client_alg = alg_good || client_alg = alg_both) && (supported = alg_good || supported = alg_both) then
		out(cf_state, (alg_good, genPub(prF2), sign((fin1, client, client_alg, alg_good, genPub(prF2)), privF)));
(* RTT 1 finished *)
		new csKey: sKey;
		in (cf_state, (pubC: pubKey, enc: bitstring));
		let (cfKey) = exchange(prF2, pubC) in
		let (data: nonce, data2: nonce) = sDec(enc, cfKey) in
		if data = Auth && data2 = Auth then
		out (sf, (client, csKey)); (* inform service of new client *)
		event acceptedFenrirState(client, csKey);
		out (cf_state, sEnc((cs, csKey), cfKey))
(* RTT 2 finished *)	
	).


(*
 * ===========================================================================
 * Client definition, directory synchronized handshake
 * ===========================================================================
 *)
let client_dir (pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce) =
	new prC : privKey;
	new cn : nonce;
	let (cfKey) = exchange(prC, pubF) in
	out (cf_dir, (genPub(prC), sEnc((client, Auth,cn), cfKey)));
	in  (cf_dir, enc: bitstring);
	let (=cn, chan: channel, csKey: sKey) = sDec(enc, cfKey) in
(* RTT 1 finished, now connect to service *)
	out (chan, sEnc((Auth, Auth), csKey)).
(*
 * ===========================================================================
 * Fenrir definition, directory synchronized handshake
 * ===========================================================================
 *)

let fenrir_dir (privF: privKey, fenrir: host, service: host, Auth: nonce) =
	in (cf_dir, (pubC: pubKey, enc: bitstring));
	let (cfKey) = exchange(privF, pubC) in
	let (cname: host, =Auth, cn: nonce) = sDec (enc, cfKey) in

	new csKey : sKey;
	out (sf, sEnc((cname, csKey), fsKey)); (* inform service of new client *)
	out (cf_dir, sEnc((cn, cs, csKey), cfKey)).
(*
 * Event correlation:
 *)
(* query h: host, k: sKey; event(acceptedFenrir(h, k)) ==> event(acceptedClient(h, k)). *)
(* *)
query h: host, k: sKey; event(acceptedClientState(h, k)) ==> event(acceptedFenrirState(h, k)).
query h1: host, h2 : host, k: sKey, t: nonce; event(serviceConnect(h1, h2, k)) ==> event(clientConnect(h1, h2, k)).


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

(*query attacker(prF). do NOT check this as we volountarly leak it after the process *)
(*query attacker(prF_dir).*) (* the private key in the directory-synchronized case must be secret *)
query attacker(Auth).	(* client auth data.  *)
query event(downgrade()).
(*
 * ==============
 * Run the verification
 * ==============
 *)

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

(* TODO: fix PFS: must leak both server and client public key *)
process
	let pbF     = genPub(prF)     in
	let pbF_dir = genPub(prF_dir) in
	( (!service(S)) 
		| (!client_full (pbF, C, S, F, Auth, alg_both)) | (!client_full (pbF, C, S, F, Auth, alg_good))
		| (!fenrir_full (prF, F, S, Auth, alg_both)) | (!fenrir_full (prF, F, S, Auth, alg_good))
		| (!client_state(pbF, C, S, F, Auth, alg_both)) | (!client_state(pbF, C, S, F, Auth, alg_good))
		| (!fenrir_state(prF, F, S, Auth, alg_both)) | (!fenrir_state(prF, F, S, Auth, alg_good))
		| (!client_dir  (pbF_dir, C, S, F, Auth)) | (!fenrir_dir  (prF, F, S, Auth))
		| phase 1; out(leak, prF) (* PFS: leaking of the long-term secret will NOT affect previous communications *)
	(* Now do everything again, WITHOUT leaking. Everything must be done again since
	 * we leaked the previous private key. If we didn't do everything again we could not prove
	 * that the interaction of the handshakes is secure.
	 * This is because the 1-RTT handshake does NOT have long-term secret
	 *)

		; (!client_full (pbF_dir, C, S, F, Auth, alg_both)) | (!client_full (pbF_dir, C, S, F, Auth, alg_good))
		| (!fenrir_full (prF_dir, F, S, Auth, alg_both)) | (!fenrir_full (prF_dir, F, S, Auth, alg_good))
		| (!client_state(pbF_dir, C, S, F, Auth, alg_both)) | (!client_state(pbF_dir, C, S, F, Auth, alg_good))
		| (!fenrir_state(prF_dir, F, S, Auth, alg_both)) | (!fenrir_state(prF_dir, F, S, Auth, alg_good))
		| (!client_dir  (pbF_dir, C, S, F, Auth)) | (!fenrir_dir  (prF_dir, F, S, Auth))

	)