(* Diffie-Hellman *)

free c : channel.		(* kanál *)
free s : bitstring [private].	(* tajná správa s *)

(* pasívny útočník *)
(* set attacker = passive. *)

(* symetrická kryptografia; konštruktor a deštruktor *)
type key.
fun enc(key, bitstring): bitstring.
reduc forall x: key, y: bitstring ; dec(x, enc(x,y)) = y.

(* funkcie pre DH výpočet a súvisiaca rovnosť *)
type privkey.
type pubkey.
fun dh(privkey, pubkey): key.
fun pk(privkey): pubkey.
equation forall x: privkey, y: privkey ; dh(x,pk(y)) = dh(y,pk(x)).

(* Dozvie sa útočník s? *)
query attacker(s).

(* proces *)

let A = new a: privkey; 
	out(c,pk(a));
	in(c,x1: pubkey);
	let k = dh(a,x1) in out(c,enc(k,s)).

let B = new b: privkey; 
	out(c,pk(b));
	in(c,x0: pubkey); 
	let k = dh(b,x0) in in(c,m: bitstring); 
	let s2 = dec(k,m) in 0.

process A | B