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

(*
 * ==============
 * 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 *)
type encrypted. (* to avoid unifying endlessly
                 * used only for the encrypted, authenticated server state sent in one packet.
                 * without this proverif tries to unify all bitstrings
                 * while it should be impossible.
                 *)

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

(* various stuff that should remain private *)
const Auth:      nonce     [private].
const prS:       privKey   [private]. (* service private key *)
const prF:       privKey   [private].
const prC:       privKey   [private].
const prF_dir:   privKey   [private].
const OTP:       sKey      [private].
const f_key:     sKey      [private].
free csKey:      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
 * ==============
 *)

(* any to bitstring conversion *)
fun fromKey(sKey) : bitstring [data, typeConverter].
reduc forall a : sKey; toKey(fromKey(a)) = a.
fun fromNonce(nonce) : bitstring [data, typeConverter].
reduc forall a : nonce; toNonce(fromNonce(a)) = a.
fun toEncrypted(bitstring) : encrypted [data, typeConverter].
reduc forall a :bitstring; fromEncrypted(toEncrypted(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 *)
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 downgrade().
event acceptedFenrir(sKey).
event clientConnect(sKey, sKey).
event serviceConnect(sKey).
event connection_full().
event connection_state().
event connection_dir().


(* NOTE: in multiple places we have an if-else branch over a nonce.
 * and the else branch start with an "if" that is the opposite of the first "if".
 * This "if" after the else seems unnecessary but actually hugely speeds up proverif.
 * reason: proverif does not have to check for all the possible nonces. It seems
 * it doesn't notice that the nonce can have only few vales, since it actually is an enum *)

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


set ignoreTypes = false.
set expandIfTermsToTerms = true. (* slower ? *)

let client_full(pubF: pubKey, Auth: nonce, supported_enc: algorithm, supported_auth: algorithm, OTP: sKey) =
    new cn1: nonce; (* Client Nonce 1 *)

    (* 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, (cn1, supported_enc));
    in  (cf_full, (sn1: nonce, selected_enc : algorithm, srv_supported_auth : algorithm, s1: bitstring, s2: bitstring));
    if ver((cn1, supported_enc, sn1, selected_enc, srv_supported_auth), s1, pubF) = true then
    if ver((sn1, selected_enc), 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_enc = alg_bad && (supported_enc = alg_both || supported_enc = alg_bad) then
    (
    event downgrade()
    )
    else
    (
        if selected_enc = alg_good && (supported_enc = alg_both || supported_enc = alg_good) then
        out (cf_full, (sn1, selected_enc, s2, cn2, genPub(prC)));
        (* s_auth: server supported 1: contains supported authentication algorithms
         * unused here, it's the same mechanism as the "selected" one
         *)
        in  (cf_full, (ephF: pubKey, srv_key : encrypted, s3: bitstring));
        if ver((ephF, srv_key, cn2), s3, pubF) = true then
        let (cfKey) = exchange(prC, ephF) in
(* RTT 2 Completed *)
        if srv_supported_auth = alg_bad && (supported_auth = alg_both || supported_auth = alg_bad) then
        (
            (* authentication somehow leaks info through encryption
             * are we being a bit paranoid?
             *)
            event downgrade()
        )
        else
        (
            if (srv_supported_auth = alg_both || srv_supported_auth = alg_good) && (supported_auth = alg_both || supported_auth = alg_good) then
            out (cf_full, (srv_key, sEnc(fromNonce(Auth), cfKey)));
            in  (cf_full, (se2: bitstring));
            let (chan: channel, xorKey: sKey) = sDec(se2, cfKey) in (* TYPE ERROR? *)

(* RTT 3 completed, can now connect to service *)

            let cs_Key : sKey = unxor(xorKey, hash(OTP)) in
            event clientConnect(cfKey, cs_Key);
            out (chan, sEnc(fromKey(OTP), cs_Key));
            event connection_full()
        )
    ).


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

let fenrir_full(privF: privKey, Auth: nonce, supported_enc: algorithm, supported_auth: algorithm, sec_key : sKey) =
    (* Nonce exchange *)
    in (cf_full, (c_n1: nonce, client_support_enc: algorithm));
    new s_nonce: nonce;
    (* triggers "event downgrade()" in the client, no need to go further *)
        (* bad only if both support bad *)
    if client_support_enc = alg_bad && (supported_enc = alg_bad || supported_enc = alg_both) then
    (
        out (cf_full, (s_nonce, alg_bad, supported_auth, sign((c_n1, client_support_enc, s_nonce, alg_bad, supported_auth), privF),
                                                         sign((s_nonce, alg_bad), privF)))
    )
    else
    (
        if client_support_enc = alg_good || client_support_enc = alg_both then
        out (cf_full, (s_nonce, alg_good, supported_auth,    sign((c_n1, client_support_enc, s_nonce, alg_good, supported_auth), privF),
                                                             sign((s_nonce, alg_good), privF)));
(* RTT 1 finished *)
        in (cf_full, (=s_nonce, =alg_good, signed: bitstring, c_n2: nonce, pubC: pubKey));
        if ver((s_nonce, alg_good), signed, genPub(privF)) = true then
        new prF2: privKey;
        let (cfKey) = exchange(prF2, pubC) in
        let enc_srv_key : bitstring = sEnc(fromKey(cfKey), sec_key) in
        out (cf_full, (genPub(prF2), toEncrypted(enc_srv_key), sign((genPub(prF2), enc_srv_key, c_n2), privF)));
(* RTT 2 finished, now we have a state *)
        in (cf_full, (srv_en : encrypted, ce1: bitstring));
        let keystring : bitstring = sDec(fromEncrypted(srv_en), sec_key) in
        let datastring : bitstring = sDec(ce1, toKey(keystring)) in
        if toNonce(datastring) = Auth then

        new user_info : nonce;
        out (sf, user_info);
        in  (sf, key : sKey);
        event acceptedFenrir(toKey(keystring));
        out (cf_full, (sEnc((cs, key), toKey(keystring))))
(* RT3 finished *)
    ).

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

let service(OTP : sKey) =
    (* sf channel is secret, thus trusted. do not encrypt to reduce
     * proverif running time *)
    in (sf, rnd : nonce); (* user info. useless in our model *)
    out (sf, xor(csKey, hash(OTP)));
    in (cs, enc2 : bitstring);
    let is_OTP : bitstring = sDec(enc2, csKey) in
    if OTP = toKey(is_OTP) then
    event serviceConnect(csKey).

(*
 * ======================================================================
 * Client Definition, Stateful handshake, with good and broken algorithms
 * ======================================================================
 *)
let client_state (pubF: pubKey, Auth: nonce, supported_enc: algorithm, supported_auth: algorithm, OTP: sKey) =
    new cn1: nonce; (* Client Nonce 1 *)

    (* 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, supported_enc));
    in  (cf_state, (selected_alg: algorithm, srv_supported_auth: algorithm, ephF: pubKey, s1: bitstring));
    if ver((cn1, supported_enc, selected_alg, srv_supported_auth, ephF), s1, pubF) = true then

(* RTT 1 completed *)

    if selected_alg = alg_bad then
    (
        if supported_enc = alg_bad || supported_enc = alg_both then
        (* bad algorithm exposes authentication data *)
        event downgrade()
    )
    else
    (
        if selected_alg = alg_good && (supported_enc = alg_good || supported_enc = alg_both) then
        if srv_supported_auth = alg_bad && (supported_auth = alg_both || supported_auth = alg_bad) then
        (
            event downgrade()
        )
        else
        (
            if (srv_supported_auth = alg_both || srv_supported_auth = alg_good) && (supported_auth = alg_both || supported_auth = alg_good) then
            let (cfKey) = exchange(prC, ephF) in
            out (cf_state, (genPub(prC), sEnc(fromNonce(Auth), cfKey)));
            in  (cf_state, enc: bitstring);
    
(* RTT 2 completed, can now connect to service *)

            let (chan: channel, xorKey: sKey) = sDec(enc, cfKey) in
            let cs_Key = unxor(xorKey, hash(OTP)) in
            event clientConnect(cfKey, cs_Key);
            out (chan, sEnc(fromKey(OTP), cs_Key));
            event connection_state()
        )
    ).



(*
 * ===========================================================================
 * Fenrir definition, stateful handshake, with good and broken algorithms
 * ===========================================================================
 *)
let fenrir_state (privF: privKey, Auth: nonce, supported_enc: algorithm, supported_auth: algorithm) =
    (* Nonce exchange *)
    new prF2 : privKey;
    new s_nonce: nonce;
    in (cf_state, (c_n1: nonce, client_supported_enc: algorithm));
    if client_supported_enc = alg_bad && (supported_enc = alg_bad || supported_enc = alg_both) then
    (
        out(cf_state, (alg_bad, supported_auth, genPub(prF2), sign((c_n1, client_supported_enc, alg_bad, supported_auth, genPub(prF2)), privF)))
    )
    else
    (
        if (client_supported_enc = alg_good || client_supported_enc = alg_both) && (supported_enc = alg_good || supported_enc = alg_both) then
        out(cf_state, (alg_good, supported_auth, genPub(prF2), sign((c_n1, client_supported_enc, alg_good, supported_auth, genPub(prF2)), privF)));
(* RTT 1 finished *)
        in (cf_state, (pubC: pubKey, enc: bitstring));
        let (cfKey) = exchange(prF2, pubC) in
        let datastring : bitstring = sDec(enc, cfKey) in
        if toNonce(datastring) = Auth then
        new user_info : nonce;
        out (sf, (user_info));
        in (sf, key : sKey);
        event acceptedFenrir(cfKey);
        out (cf_state, sEnc((cs, key), cfKey))
(* RTT 2 finished *)    
    ).




(*
 * ===========================================================================
 * Client definition, directory synchronized handshake
 * ===========================================================================
 *)

let client_dir (pubF: pubKey, Auth: nonce, OTP: sKey) =
    new cn : nonce;
    let (cfKey) = exchange(prC, pubF) in
    out (cf_dir, (genPub(prC), sEnc((Auth,cn), cfKey)));
    in  (cf_dir, enc: bitstring);
(* RTT 1 finished, now connect to service *)
    let (=cn, chan: channel, xorKey: sKey) = sDec(enc, cfKey) in
    let cs_Key = unxor(xorKey, hash(OTP)) in
    event clientConnect(cfKey, cs_Key);
    out (chan, sEnc(fromKey(OTP), cs_Key));
    event connection_dir().


(*
 * ===========================================================================
 * Fenrir definition, directory synchronized handshake
 * ===========================================================================
 *)
let fenrir_dir (privF: privKey, Auth: nonce) =
    in (cf_dir, (pubC: pubKey, enc: bitstring));
    let (cfKey) = exchange(privF, pubC) in
    let (=Auth, cn: nonce) = sDec (enc, cfKey) in

    new user_info : nonce;
    out (sf, user_info);
    in (sf, key : sKey);
    event acceptedFenrir(cfKey);
    out (cf_dir, sEnc((cn, cs, key), cfKey)).



(*
 * ==============
 * Event correlation:
 * ==============
 *)

query k1 : sKey, k2 : sKey; event(serviceConnect(k2)) ==> event(clientConnect(k1, k2)).
query k1 : sKey, k2 : sKey; event(clientConnect(k1, k2)) ==> event(acceptedFenrir(k1)).

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

query event(downgrade()).
query attacker(OTP).	(* client-service OTP data. *)
query attacker(Auth).	(* client auth data.  *)
(*
 * Event connection() HAS to be triggered
 * we use it as a proof that we didn't just make a protocol that will never compete a handshake.
 *)
query event(connection_full()).
query event(connection_state()).
query event(connection_dir()).


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


process
    let pbF     = genPub(prF)     in
    let pbF_dir = genPub(prF_dir) in
    (
(* Perfect forward secrecy test. Note that the _dir methods work with non-leaked keys, as there
 * is no master key
 *)
(* these tests alone needs about 26k to 46k rules in proverif
 *  phase 0: both parts support good algorithms.
 *  phase 1: client supports only bad algorithms
 *  phase 2: auth-server supports only bad algorithms
 *  phase 3: leak long term secret to test perfect forward secrecy,
 *)
    (!service(OTP)) 
        | (!client_full (pbF, Auth, alg_both, alg_both, OTP))  | (!client_full (pbF, Auth, alg_good, alg_both, OTP))
        | (!client_full (pbF, Auth, alg_both, alg_good, OTP))  | (!client_full (pbF, Auth, alg_good, alg_good, OTP))
        | (!fenrir_full (prF, Auth, alg_both, alg_both, f_key))| (!fenrir_full (prF, Auth, alg_good, alg_both, f_key))
        | (!fenrir_full (prF, Auth, alg_both, alg_good, f_key))| (!fenrir_full (prF, Auth, alg_good, alg_good, f_key))
(*
    (!service(OTP)) 
        | (!client_full (pbF, Auth, alg_both, alg_both, OTP))  | (!client_full (pbF, Auth, alg_good, alg_both, OTP))
        | (!client_full (pbF, Auth, alg_both, alg_good, OTP))  | (!client_full (pbF, Auth, alg_good, alg_good, OTP))
        | (!fenrir_full (prF, Auth, alg_both, alg_both, f_key))| (!fenrir_full (prF, Auth, alg_good, alg_both, f_key))
        | (!fenrir_full (prF, Auth, alg_both, alg_good, f_key))| (!fenrir_full (prF, Auth, alg_good, alg_good, f_key))
        | (!client_state(pbF, Auth, alg_both, alg_both, OTP))  | (!client_state(pbF, Auth, alg_good, alg_both, OTP))
        | (!client_state(pbF, Auth, alg_both, alg_good, OTP))  | (!client_state(pbF, Auth, alg_good, alg_good, OTP))
        | (!fenrir_state(prF, Auth, alg_both, alg_both))       | (!fenrir_state(prF, Auth, alg_good, alg_both))
        | (!fenrir_state(prF, Auth, alg_both, alg_good))       | (!fenrir_state(prF, Auth, alg_good, alg_good))
*)
(*
    (!service(OTP))
        | (!client_full (pbF, Auth, alg_both, alg_both, OTP)) | (!client_full (pbF, Auth, alg_bad, alg_both, OTP))
        | (!client_full (pbF, Auth, alg_both, alg_bad, OTP))  | (!client_full (pbF, Auth, alg_bad, alg_bad, OTP))
        | (!fenrir_full (prF, Auth, alg_good, alg_good, f_key))
        | (!client_state(pbF, Auth, alg_both, alg_both, OTP)) | (!client_state(pbF, Auth, alg_bad, alg_both, OTP))
        | (!client_state(pbF, Auth, alg_both, alg_bad, OTP))  | (!client_state(pbF, Auth, alg_bad, alg_bad, OTP))
        | (!fenrir_state(prF, Auth, alg_good, alg_good))
*)
(*
    (!service(OTP))
        | (!client_full (pbF, Auth, alg_good, alg_good, OTP))
        | (!fenrir_full (prF, Auth, alg_both, alg_both))      | (!fenrir_full (prF, Auth, alg_bad, alg_both))
        | (!fenrir_full (prF, Auth, alg_both, alg_bad, f_key))| (!fenrir_full (prF, Auth, alg_bad, alg_bad, f_key))
        | (!client_state(pbF, Auth, alg_good, alg_good, OTP))
        | (!fenrir_state(prF, Auth, alg_both, alg_both))      | (!fenrir_state(prF, Auth, alg_bad, alg_both))
        | (!fenrir_state(prF, Auth, alg_both, alg_bad))       | (!fenrir_state(prF, Auth, alg_bad, alg_bad))
*)
(*
    | 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, so wen can't leak its private key.
     *)
(* these next tests alone needs about 37k to 55k rules in proverif
 * the previous and the next tests together are way too much, as proverif seems to have a huge slow down for every new phase,
 *  even when empty. Therefore activate either the previous or the next tests, they are independent anyway.
 *  pahse 0-2: like previous phase 0-2, except we add the directory synchronized handshake
 *             and do NOT leak the key at the end. This way we can test the interaction
 *             of different handshakes with the same public key.
 *)
(*
    (!service(OTP))
        | (!client_full (pbF_dir, Auth, alg_both, alg_both, OTP))  | (!client_full (pbF_dir, Auth, alg_good, alg_both, OTP))
        | (!client_full (pbF_dir, Auth, alg_both, alg_good, OTP))  | (!client_full (pbF_dir, Auth, alg_good, alg_good, OTP))
        | (!fenrir_full (prF_dir, Auth, alg_both, alg_both, f_key))| (!fenrir_full (prF_dir, Auth, alg_good, alg_both, f_key))
        | (!fenrir_full (prF_dir, Auth, alg_both, alg_good, f_key))| (!fenrir_full (prF_dir, Auth, alg_good, alg_good, f_key))
        | (!client_state(pbF_dir, Auth, alg_both, alg_both, OTP))  | (!client_state(pbF_dir, Auth, alg_good, alg_both, OTP))
        | (!client_state(pbF_dir, Auth, alg_both, alg_good, OTP))  | (!client_state(pbF_dir, Auth, alg_good, alg_good, OTP))
        | (!fenrir_state(prF_dir, Auth, alg_both, alg_both))       | (!fenrir_state(prF_dir, Auth, alg_good, alg_both))
        | (!fenrir_state(prF_dir, Auth, alg_both, alg_good))       | (!fenrir_state(prF_dir, Auth, alg_good, alg_good))
        | (!client_dir  (pbF_dir, Auth, OTP))                      | (!fenrir_dir  (prF_dir, Auth))
*)
(*
    (!service(OTP))
        | (!client_full (pbF_dir, Auth, alg_both, alg_both, OTP))  | (!client_full (pbF_dir, Auth, alg_bad, alg_both, OTP))
        | (!client_full (pbF_dir, Auth, alg_both, alg_bad,  OTP))  | (!client_full (pbF_dir, Auth, alg_bad, alg_bad,  OTP))
        | (!fenrir_full (prF_dir, Auth, alg_good, alg_good, f_key))
        | (!client_state(pbF_dir, Auth, alg_both, alg_both, OTP))  | (!client_state(pbF_dir, Auth, alg_bad, alg_both, OTP))
        | (!client_state(pbF_dir, Auth, alg_both, alg_bad,  OTP))  | (!client_state(pbF_dir, Auth, alg_bad, alg_bad,  OTP))
        | (!fenrir_state(prF_dir, Auth, alg_good, alg_good))
        | (!client_dir  (pbF_dir, Auth, OTP))                     | (!fenrir_dir  (prF_dir, Auth))
*)
(*
    (!service(OTP))
        | (!client_full (pbF_dir, Auth, alg_good, alg_good, OTP))
        | (!fenrir_full (prF_dir, Auth, alg_both, alg_both, f_key))| (!fenrir_full (prF_dir, Auth, alg_bad, alg_both, f_key))
        | (!fenrir_full (prF_dir, Auth, alg_both, alg_bad,  f_key))| (!fenrir_full (prF_dir, Auth, alg_bad, alg_bad,  f_key))
        | (!client_state(pbF_dir, Auth, alg_good, alg_good, OTP))
        | (!fenrir_state(prF_dir, Auth, alg_both, alg_both))       | (!fenrir_state(prF_dir, Auth, alg_bad, alg_both))
        | (!fenrir_state(prF_dir, Auth, alg_both, alg_bad))        | (!fenrir_state(prF_dir, Auth, alg_bad, alg_bad))
        | (!client_dir  (pbF_dir, Auth, OTP))                      | (!fenrir_dir  (prF_dir, Auth))
*)
    )