(*
 * Formal definition to verify the Fenrir protocol.
 * to be used with ProVerif
 *
 * quick test to show that proverif can find xor keys
 * even without associativity.
 *)

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

type sKey.	(* symmetric key *)

const cs: channel.

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


const plain1: sKey [private].
const plain2: sKey [private].
(* keep the secret secret, or not?
free secret: sKey [private].
free secret: sKey .
*)
free secret: sKey.

let client1 (pl: sKey, sec: sKey) =
    let xored = xor(pl, sec) in
    out (cs, (xored)).
let client2 (pl: sKey, sec: sKey) =
    let xored = xor(sec, pl) in
    out (cs, (xored)).
 

query attacker(plain1).
query attacker(plain2).

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


process
    (!client1(plain1, secret)) | (!client2(plain2, secret))