From 54e9e8f6064a201193e238f28848783896595911 Mon Sep 17 00:00:00 2001
From: Vincent Cheval <vincent.cheval@icloud.com>
Date: Mon, 20 Jan 2020 18:03:00 +0100
Subject: [PATCH] Adding many examples

---
 .../session_equivalence/BAC-2sessions.dps     |  61 +++++++++
 .../session_equivalence/BAC-3sessions.dps     |  52 ++++++++
 .../trace_equivalence/AA-bug.dps              | 116 ++++++++++++++++++
 .../trace_equivalence/LAK06-UK3-pair.dps      |  54 ++++++++
 .../trace_equivalence/WMF-bug.dps             |  48 ++++++++
 .../trace_equivalence/bug_itsaka.dps          |  14 +++
 .../trace_equivalence/bug_itsaka2.dps         |  14 +++
 .../trace_equivalence/equivalent.dps          |  36 ++++++
 .../trace_equivalence/equivalent2.dps         |  34 +++++
 .../trace_equivalence/equivalent3.dps         |  11 ++
 .../example_stackOverflow.dps                 |  84 +++++++++++++
 .../trace_equivalence/loli_destroyer.dps      |  13 ++
 .../trace_equivalence/loli_destroyer2.dps     |  13 ++
 .../trace_equivalence/non-equivalent.dps      |  35 ++++++
 .../trace_equivalence/tuple.dps               |  12 ++
 .../trace_equivalence/warning.dps             |  17 +++
 .../trace_equivalence/warning_and_error.dps   |  15 +++
 .../trace_equivalence/yahalom-paulson-bug.dps |  83 +++++++++++++
 18 files changed, 712 insertions(+)
 create mode 100644 Examples/toys_and_tests/session_equivalence/BAC-2sessions.dps
 create mode 100644 Examples/toys_and_tests/session_equivalence/BAC-3sessions.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/AA-bug.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/LAK06-UK3-pair.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/WMF-bug.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/bug_itsaka.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/bug_itsaka2.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/equivalent.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/equivalent2.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/equivalent3.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/example_stackOverflow.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/loli_destroyer.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/loli_destroyer2.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/non-equivalent.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/tuple.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/warning.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/warning_and_error.dps
 create mode 100644 Examples/toys_and_tests/trace_equivalence/yahalom-paulson-bug.dps

diff --git a/Examples/toys_and_tests/session_equivalence/BAC-2sessions.dps b/Examples/toys_and_tests/session_equivalence/BAC-2sessions.dps
new file mode 100644
index 0000000..9ce23a5
--- /dev/null
+++ b/Examples/toys_and_tests/session_equivalence/BAC-2sessions.dps
@@ -0,0 +1,61 @@
+// Unlinkability
+
+fun mac/2.
+
+free c.
+
+free Error_6300.
+free get_challenge.
+
+fun senc/2.
+
+reduc sdec(senc(x,y),y) -> x.
+
+// Description of the reader role
+
+let reader(k_e,k_m) =
+  out(c,get_challenge);
+  in(c,xn_t);
+  new n_r;
+  new k_r;
+  let xm = senc((n_r,xn_t,k_r),k_e) in
+  out(c,(xm,mac(xm,k_m)));
+  in(c,y).
+
+// Description of the passport role
+
+let passport(k_e,k_m) =
+  in(c,x);
+  if x = get_challenge
+  then
+    new n_t;
+    out(c,n_t);
+    in(c,y);
+    let (xm_e,xm_m) = y in
+    if xm_m = mac(xm_e,k_m)
+    then
+      let (xn_r,xn_t,xk_r) = sdec(xm_e,k_e) in
+        if xn_t = n_t
+        then (
+        	new k_t;
+        	let z = senc((n_t,xn_r,k_t),k_e) in
+        	out(c,(z,mac(z,k_m)))
+        ) else out(c,Error_6300)
+      else out(c,Error_6300)
+    else out(c,Error_6300).
+
+// Unlinkability
+
+let system1 =
+  (new k_e; new k_m; (passport(k_e,k_m) | reader(k_e,k_m))) |
+  (new k_e; new k_m; (passport(k_e,k_m) | reader(k_e,k_m))).
+
+let system2 =
+  new k_e; new k_m;
+  (
+    passport(k_e,k_m) | reader(k_e,k_m) |
+    passport(k_e,k_m) | reader(k_e,k_m)
+  ).
+
+
+query session_equiv(system1,system2).
diff --git a/Examples/toys_and_tests/session_equivalence/BAC-3sessions.dps b/Examples/toys_and_tests/session_equivalence/BAC-3sessions.dps
new file mode 100644
index 0000000..623e188
--- /dev/null
+++ b/Examples/toys_and_tests/session_equivalence/BAC-3sessions.dps
@@ -0,0 +1,52 @@
+// Unlinkability
+
+fun mac/2.
+
+free c.
+
+free Error_6300.
+free get_challenge.
+
+fun senc/2.
+
+reduc sdec(senc(x,y),y) -> x.
+
+// Description of the reader role
+
+let reader(k_e,k_m) =
+  out(c,get_challenge);
+  in(c,xn_t);
+  new n_r;
+  new k_r;
+  let xm = senc((n_r,xn_t,k_r),k_e) in
+  out(c,(xm,mac(xm,k_m)));
+  in(c,y).
+
+// Description of the passport role
+
+let passport(k_e,k_m) =
+  in(c,x);
+  if x = get_challenge
+  then
+    new n_t;
+    out(c,n_t);
+    in(c,y);
+    let (xm_e,xm_m) = y in
+    let (=xm_m,(xn_r,=n_t,xk_r)) = (mac(xm_e,k_m),sdec(xm_e,k_e)) in
+      new k_t;
+      let z = senc((n_t,xn_r,k_t),k_e) in
+        out(c,(z,mac(z,k_m)))
+      else 0
+    else out(c,Error_6300).
+
+// Unlinkability
+
+let system1 =
+  !^3 (new k_e; new k_m; (passport(k_e,k_m) | reader(k_e,k_m))).
+
+let system2 =
+    (new k_e; new k_m; !^2 (passport(k_e,k_m) | reader(k_e,k_m)))
+  | (new k_e; new k_m; (passport(k_e,k_m) | reader(k_e,k_m))).
+
+
+query session_equiv(system1,system2).
diff --git a/Examples/toys_and_tests/trace_equivalence/AA-bug.dps b/Examples/toys_and_tests/trace_equivalence/AA-bug.dps
new file mode 100644
index 0000000..86fd11e
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/AA-bug.dps
@@ -0,0 +1,116 @@
+// Passive Authentication Protocol between a passport (P) and a reader (R)
+// We test the anonymity of the passport
+// SHOULD BE TRUE
+
+// channels
+free c.
+free chP1,chR1,chP2,chR2,chP3,chR3,chP4,chR4,chP5,chR5.
+
+// constants
+free ok.
+free ini.
+free m1, m2.
+
+free ksenci, ksmaci.
+
+// functions
+fun hash/1.
+fun senc/2.
+fun sign/2.
+fun vk/1.
+
+
+reduc sdec(senc(x,y),y) -> x.
+reduc checksign(sign(x,y),vk(y)) -> ok.
+reduc getmsg(sign(x,y)) -> x.
+
+/*
+Description of the passport role:
+*/
+
+let passport(sk,ksenc,ksmac,ch) =
+  in(ch, x);
+  let (xenc, xmac) = x in
+  if xmac = hash((xenc, ksmac)) then
+  let (=ini,xr1) = sdec(xenc,ksenc) in
+  new n0;
+  let ysign = sign((n0,xr1),sk) in
+  let ysenc = senc(ysign,ksenc) in
+  let ymac  = hash((ysenc,ksmac))  in
+  out(ch,(ysenc,ymac)).
+
+/*
+Description of the Reader role
+*/
+
+let reader(vk,ksenc,ksmac,ch) =
+  new r1 ;
+  let menc = senc((ini,r1),ksenc) in
+  let mmac = hash((menc,ksmac)) in
+  out(ch, (menc, mmac));
+  in(ch,x);
+  let (xenc, xmac) = x in
+  if xmac = hash((xenc,xmac)) then
+  let xsign = sdec(xenc,ksenc) in
+  if ok = checksign(xsign,vk) then
+  let (xn1,=r1) = getmsg(xsign) in
+  out(ch,ok).
+
+let readerP(vk,ksenc,ksmac,ch) =
+  new r1 ;
+  let menc = senc((ini,r1),ksenc) in
+  let mmac = hash((menc,ksmac)) in
+  out(ch, (menc, mmac));
+  in(ch,x);
+  let (xenc, xmac) = x in
+  if xmac = hash((xenc,xmac)) then
+  let xsign = sdec(xenc,ksenc) in
+  if ok = checksign(xsign,vk) then
+  let (xn1,=r1) = getmsg(xsign) in
+  out(ch,senc(m1,xn1)).
+
+let readerQ(vk,ksenc,ksmac,ch) =
+  new r1 ;
+  let menc = senc((ini,r1),ksenc) in
+  let mmac = hash((menc,ksmac)) in
+  out(ch, (menc, mmac));
+  in(ch,x);
+  let (xenc, xmac) = x in
+  if xmac = hash((xenc,xmac)) then
+  let xsign = sdec(xenc,ksenc) in
+  if ok = checksign(xsign,vk) then
+  let (xn1,=r1) = getmsg(xsign) in
+  new k ;
+  out(ch,senc(m2,k)).
+
+
+
+/*
+Passport and Reader in parallel
+*/
+
+let OneSessionPassportP(sk,chP,chR) =
+  (readerP(vk(sk),ksenci,ksmaci,chR) | passport(sk,ksenci,ksmaci,chP)).
+
+let OneSessionPassportQ(sk,chP,chR) =
+  (readerQ(vk(sk),ksenci,ksmaci,chR) | passport(sk,ksenci,ksmaci,chP)).
+
+let Process1 =
+  new sk;
+  out(c, ok);
+  out(c, ini);
+  out(c, vk(sk));
+  (
+    OneSessionPassportP(sk,chP1,chR1)
+  ).
+
+let Process2 =
+  new sk;
+  out(c, ok);
+  out(c, ini);
+  out(c, vk(sk));
+  (
+    OneSessionPassportQ(sk,chP1,chR1)
+  ).
+
+query trace_equiv(Process1,Process2).
diff --git a/Examples/toys_and_tests/trace_equivalence/LAK06-UK3-pair.dps b/Examples/toys_and_tests/trace_equivalence/LAK06-UK3-pair.dps
new file mode 100644
index 0000000..12ecc26
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/LAK06-UK3-pair.dps
@@ -0,0 +1,54 @@
+// Unlinkability LAK with pairs - 2 sessions
+// In the CSF'18 paper about Tamarin/XOR, they studied the version with XOR,
+// and replacing the XOR with pair lead to a file on which Tamarin establish the equivalence.
+// Si success visible avec out(ok) alors non-equivalent
+// Si success non visible avec then 0 alors equivalent.
+//
+//  R -> T: r0
+//  T -> R: r1, h(r0 XOR r1 XOR k)
+//  R -> T: h(h(r0 XOR r1 XOR k) XOR k XOR r0)
+//
+
+
+
+fun h/3.
+
+free cr.
+free ct.
+free ok.
+free ko.
+
+// Description of the reader role
+
+let reader(k) =
+  new r0;
+  out(cr,r0);
+  in(cr,xr);
+  let (xr1, xh) = xr in
+  if xh = h(r0,xr1,k) then
+  out(cr,h(xh,k,r0)).
+
+// Description of tag role
+
+let tag(k) =
+  in(ct,xr0);
+  new r1;
+  out(ct,(r1,h(xr0,r1,k)));
+  in(ct,y);
+  if y = h(h(xr0,r1,k),k,xr0) then out(ct,ok).
+
+// Unlinkability
+
+let system1 =
+  (new k1; (tag(k1) | reader(k1))) |
+  (new k2; (tag(k2) | reader(k2))).
+
+let system2 =
+  new k;
+  (
+    tag(k) | reader(k) |
+    tag(k) | reader(k)
+  ).
+
+
+query trace_equiv(system1,system2).
diff --git a/Examples/toys_and_tests/trace_equivalence/WMF-bug.dps b/Examples/toys_and_tests/trace_equivalence/WMF-bug.dps
new file mode 100644
index 0000000..89aae15
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/WMF-bug.dps
@@ -0,0 +1,48 @@
+free a.
+free b.
+free i.
+free kis.
+free m1.
+free m2.
+free ca.
+free cb.
+free cs.
+
+fun senc/2.
+reduc sdec(senc(x,y),y) -> x.
+
+let processA(ca,a,kas,b) =
+ new kab;
+ in(ca,z);
+ out(ca, (a, senc((b,kab),kas))).
+
+let processS(cs,a,b,kas,kbs) =
+ in(cs, x);
+ let (xa,xenc) = x in
+ if xa = a then
+ let (xb,xk) = sdec(xenc,kas) in
+ if xb = b
+ then out(cs, senc((a,xk),kbs)).
+
+let processB1(cb,b,a,kbs) =
+ in(cb,y);
+ let (ya,yk) = sdec(y,kbs) in
+ if ya = a then out(cb,senc(m1,yk)).
+
+let processB2(cb,b,a,kbs) =
+ in(cb,y);
+ let (ya,yk) = sdec(y,kbs) in
+ if ya = a then new k; out(cb,senc(m2,k)).
+
+
+let P =
+ new kas; new kbs; 
+ ( processS(cs,i,b,kis,kbs) | processB1(cb,b,i,kbs)).
+
+
+let Q =
+ new kas; new kbs; 
+ ( processS(cs,i,b,kis,kbs) | processB2(cb,b,i,kbs)).
+
+
+query trace_equiv(P,Q).
diff --git a/Examples/toys_and_tests/trace_equivalence/bug_itsaka.dps b/Examples/toys_and_tests/trace_equivalence/bug_itsaka.dps
new file mode 100644
index 0000000..d505810
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/bug_itsaka.dps
@@ -0,0 +1,14 @@
+free c.
+fun mac/2.
+
+let A =
+  new n_t;
+  out(c,n_t).
+
+let B(k) =
+  in(c,n_t);
+  out(c,mac(n_t,k)).
+
+let sys = !^2 A | new k; !^2 B(k).
+
+query trace_equiv(sys,sys).
diff --git a/Examples/toys_and_tests/trace_equivalence/bug_itsaka2.dps b/Examples/toys_and_tests/trace_equivalence/bug_itsaka2.dps
new file mode 100644
index 0000000..7b98f8b
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/bug_itsaka2.dps
@@ -0,0 +1,14 @@
+free c.
+fun mac/2.
+
+let A =
+  new n_t;
+  out(c,n_t).
+
+let B(k) =
+  in(c,n_t);
+  out(c,mac(n_t,k)).
+
+let sys = A | A | new k; (B(k) | B(k)).
+
+query trace_equiv(sys,sys).
diff --git a/Examples/toys_and_tests/trace_equivalence/equivalent.dps b/Examples/toys_and_tests/trace_equivalence/equivalent.dps
new file mode 100644
index 0000000..507d219
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/equivalent.dps
@@ -0,0 +1,36 @@
+free i.
+free kis.
+free cb, cs.
+
+fun senc/2.
+reduc sdec(senc(x,y),y) -> x.
+
+let processS(cs,kbs) =
+ in(cs,x);
+ out(cs, senc(i,kbs)).
+
+
+let processB1(cb,kbs) =
+ in(cb,y);
+ let yk = sdec(y,kbs) in
+ out(cb,yk).
+
+let processB2(cb,kbs) =
+ in(cb,y);
+ let yk = sdec(y,kbs) in
+ new k; out(cb,k).
+
+
+let P =
+ new kbs;
+( processS(cs,kbs)
+| processB1(cb,kbs)).
+
+
+let Q =
+ new kbs;
+( processS(cs,kbs)
+| processB2(cb,kbs)).
+
+
+query trace_equiv(P,Q).
diff --git a/Examples/toys_and_tests/trace_equivalence/equivalent2.dps b/Examples/toys_and_tests/trace_equivalence/equivalent2.dps
new file mode 100644
index 0000000..2109792
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/equivalent2.dps
@@ -0,0 +1,34 @@
+free i.
+free kis.
+free cb, cs.
+
+fun senc/2.
+reduc sdec(senc(x,y),y) -> x.
+
+let processS(cs,kbs) =
+ in(cs,x);
+ out(cs, senc(i,kbs)).
+
+
+let processB1(cb,kbs) =
+ in(cb,y);
+ out(cb,y).
+
+let processB2(cb,kbs) =
+ in(cb,y);
+ new k; out(cb,k).
+
+
+let P =
+new kbs ;
+( processS(cs,kbs) 
+| processB1(cb,kbs)).
+
+
+let Q =
+new kbs ;
+( processS(cs,kbs) 
+| processB2(cb,kbs)).
+
+
+query trace_equiv(P,Q).
diff --git a/Examples/toys_and_tests/trace_equivalence/equivalent3.dps b/Examples/toys_and_tests/trace_equivalence/equivalent3.dps
new file mode 100644
index 0000000..e674f85
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/equivalent3.dps
@@ -0,0 +1,11 @@
+free i.
+free kis, kis1.
+free cb, cs, c.
+
+
+let P = in(cs,x); (in(c,y); out(c,i) | in(cs,z); out(cs,kis)).
+
+let Q = in(cs,x); (in(c,y); out(c,i) | in(cs,z); out(cs,kis1)).
+
+
+query trace_equiv(P,Q).
diff --git a/Examples/toys_and_tests/trace_equivalence/example_stackOverflow.dps b/Examples/toys_and_tests/trace_equivalence/example_stackOverflow.dps
new file mode 100644
index 0000000..32b9759
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/example_stackOverflow.dps
@@ -0,0 +1,84 @@
+free c.
+fun qubit/2.
+fun bs/5.
+
+const two.
+const one.
+const zero.
+const bases.
+const bit.
+const d.
+const Alice.
+const Bob.
+const ok.
+const cheat.
+
+reduc bsEqu( bs(k1,bitstring1,position1,role1,value1),
+             bs(k1,bitstring1,position1,role2,value1))
+      -> ok.
+reduc measure((pos, qubit(bit, bs(s, bases,  pos2, role, val))), (pos, bs(s, bases, pos3, roleX, val)), pos) -> bit.
+
+
+let Bob_proc(val,cqRead,cqWrite,cqMeasure,cp,sampling) =
+  let b   = bs(sampling, bases,  one, Alice, zero) in (* bit revealed to the atatcker *)
+  let b_c = bs(sampling, bases,  one, Alice, one ) in (* cheat bit, revealed later *)
+  let b1_ = bs(sampling, bases,  one, Bob,   zero) in (* Bases used by Bob *)
+  let b2_ = bs(sampling, bases,  one, Bob,   one) in
+( out(c, b);
+(* Bob receives and measures qubits in <b1_,b2_> *)
+ (out(cqRead, (one, b1_))  |
+  out(cqRead, (two, b2_))) |
+(* Bob gets the measures bits *)
+( in(cqMeasure, x1);
+  let (=one, bit1) = x1 in
+  in(cqMeasure, x2);  (* would be better to have those two in parallel, can we do that? TODO*)
+  let (=two, bit2) = x2 in
+(* The attacker is given the base he was supposed to commit on in the first place *)
+  out(c, b_c);
+  let baseCommit = b_c in
+(* Bob receives the commit base and the verification bits from the network *)
+  in(c, x3);
+  let (=b_c, (bitV1, bitV2)) = x3 in
+  if val = cheat then
+  if bitV1 = bit1 then
+  out(c,cheat))).
+
+let quantumAttacker(cqRead,cqWrite,cqMeasure,cp,sampling) =
+(* attacker can send qubits *)
+( in(c,req);
+  let (xbit, base) = req in
+  out(cqWrite, qubit(xbit, base) )) |
+(* attacker can intercept and measure qubits *)
+( in(cqWrite, write); (* pos, qubit(bit, bs(s,   bases,  pos, role,   val))); *)
+  in(c, read);  (*  (=pos,     bs(=s, =bases, =pos, roleX, =val))); *)
+  let (pos, base) = read in
+  let bitm = measure(write,read,pos) in
+  out(c, bitm) ).
+
+let quantumChannel(cqRead,cqWrite,cqMeasure,cp,sampling) =
+(* Measure in appropriate base *)
+( in(cqWrite, write); (*    pos, qubit(bit, bs(s,   bases,  pos, role,   val)) *)
+  in(cqRead,  read); (* (=pos,     bs(=s, =bases, =pos, roleX, =val))*)
+  let (pos, base) = read in
+  let bitm = measure(write,read,pos) in
+  out(cqMeasure, (pos, bitm)) ) |
+(* Measure in inappropriate base *)
+( in(cqRead, read); (*  (=pos,     bs(=s, =bases, =pos, roleX, =val))); *)
+  let (pos, base) = read in
+  new n;
+  out(cqMeasure, (pos, n)) ).
+
+
+let process(val) =
+  new cqRead;
+  new cqWrite;
+  new cqMeasure;
+  new cp;
+  new sampling;
+  (
+    Bob_proc(val,cqRead,cqWrite,cqMeasure,cp,sampling) |
+    !^2 quantumChannel(cqRead,cqWrite,cqMeasure,cp,sampling) |
+    quantumAttacker(cqRead,cqWrite,cqMeasure,cp,sampling)
+  ).
+
+query trace_equiv(process(cheat), process(ok)).
diff --git a/Examples/toys_and_tests/trace_equivalence/loli_destroyer.dps b/Examples/toys_and_tests/trace_equivalence/loli_destroyer.dps
new file mode 100644
index 0000000..401a083
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/loli_destroyer.dps
@@ -0,0 +1,13 @@
+free c.
+fun h/2.
+
+let P = in(c,x); in(c,y); out(c,h(x,y)).
+
+let Q = !^4 P.
+
+query trace_equiv(Q,Q).
+
+/* Experiments (4 sessions)
+DEEPSEC: 11min
+Akiss: instant
+ProVerif: instant */
diff --git a/Examples/toys_and_tests/trace_equivalence/loli_destroyer2.dps b/Examples/toys_and_tests/trace_equivalence/loli_destroyer2.dps
new file mode 100644
index 0000000..87c9a39
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/loli_destroyer2.dps
@@ -0,0 +1,13 @@
+free c.
+fun h/2.
+
+let P = in(c,x); out(c,x).
+
+let Q = !^2 P.
+
+query trace_equiv(Q,Q).
+
+/* Experiments (4 sessions)
+DEEPSEC: 11min
+Akiss: instant
+ProVerif: instant */
diff --git a/Examples/toys_and_tests/trace_equivalence/non-equivalent.dps b/Examples/toys_and_tests/trace_equivalence/non-equivalent.dps
new file mode 100644
index 0000000..b8d35fe
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/non-equivalent.dps
@@ -0,0 +1,35 @@
+free i.
+free kis.
+free cb, cs.
+
+fun senc/2.
+reduc sdec(senc(x,y),y) -> x.
+
+let processS(cs,kbs) =
+ out(cs, senc(i,kbs)).
+
+
+let processB1(cb,kbs) =
+ in(cb,y);
+ let yk = sdec(y,kbs) in
+ out(cb,yk).
+
+let processB2(cb,kbs) =
+ in(cb,y);
+ let yk = sdec(y,kbs) in
+ new k; out(cb,k).
+
+
+let P =
+ new kbs; 
+( processS(cs,kbs) 
+| processB1(cb,kbs)).
+
+
+let Q =
+ new kbs; 
+( processS(cs,kbs) 
+| processB2(cb,kbs)).
+
+
+query trace_equiv(P,Q).
diff --git a/Examples/toys_and_tests/trace_equivalence/tuple.dps b/Examples/toys_and_tests/trace_equivalence/tuple.dps
new file mode 100644
index 0000000..48575e3
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/tuple.dps
@@ -0,0 +1,12 @@
+free c.
+free a,b.
+
+let P = in(c,x); out(c,x); if x = (a,b) then out(c,a).
+
+let Q = in(c,x); out(c,(a,b)).
+
+let Q1 = in(c,x); out(c,(a,b)); if x = (a,b) then out(c,a).
+
+query trace_equiv(P+Q,Q1+P).
+
+(* Should be equivalent ! *)
diff --git a/Examples/toys_and_tests/trace_equivalence/warning.dps b/Examples/toys_and_tests/trace_equivalence/warning.dps
new file mode 100644
index 0000000..7eb8ee4
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/warning.dps
@@ -0,0 +1,17 @@
+free c.
+fun mac/2.
+free a,b.
+
+let A =
+  in(c,x);
+  (
+    new k;
+    new k;
+    new kb;
+    new kb;
+    !^2 in(c,y); if y = x then out(c,k) else out(c,b)
+  ).
+
+let sys = A.
+
+query session_equiv(sys,sys). // equivalent
diff --git a/Examples/toys_and_tests/trace_equivalence/warning_and_error.dps b/Examples/toys_and_tests/trace_equivalence/warning_and_error.dps
new file mode 100644
index 0000000..e38605a
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/warning_and_error.dps
@@ -0,0 +1,15 @@
+free c.
+fun mac/2.
+free a,b.
+
+let A =
+  in(c,x);
+  (
+    new k;
+    new k;
+    !^2 in(c,y); if y = x then out(c,ka) else out(c,b)
+  ).
+
+let sys = A.
+
+query session_equiv(sys,sys). // equivalent
diff --git a/Examples/toys_and_tests/trace_equivalence/yahalom-paulson-bug.dps b/Examples/toys_and_tests/trace_equivalence/yahalom-paulson-bug.dps
new file mode 100644
index 0000000..04dda53
--- /dev/null
+++ b/Examples/toys_and_tests/trace_equivalence/yahalom-paulson-bug.dps
@@ -0,0 +1,83 @@
+
+free ca.
+free cb.
+free cs.
+
+free a.
+free b.
+free i.
+free s.
+free m1.
+free m2.
+
+free kis.
+
+free c1.
+free c2.
+free c3.
+free c4.
+
+fun senc/2.
+reduc sdec(senc(x,y),y) -> x.
+
+let A(ca,a,b,kas)=
+ in(ca,xinit);
+ new na;
+ out(ca,(a,na));
+ in(ca,x0);
+ let (xnb,x1,x2) = x0 in
+ let (xc2,xb,xkab,xna) = sdec(x1,kas) in
+ if (xc2,xb,xna) = (c2,b,na) then
+ out(ca,(x2,senc((c4,xnb),xkab))).
+
+
+let BP(cb,b,a,kbs)=
+ in(cb,y0);
+ let (ya,yna) = y0 in
+ if ya = a then
+ new nb;
+ out(cb,(b,nb,senc((c1,a,yna),kbs)));
+ in(cb,y1);
+ let (y2,y3) = y1 in
+ let (yc3,yaa,ybb,ykab,ynb) = sdec(y2,kbs) in
+ if (yc3,yaa,ybb,ynb) = (c3,a,b,nb) then
+ let (yc4,yynb) = sdec(y3,ykab) in
+ if (yc4,yynb) = (c4,nb) then
+ out(cb,senc(m1,ykab)).
+
+let BQ(cb,b,a,kbs)=
+ in(cb,y0);
+ let (ya,yna) = y0 in
+ if ya = a then
+ new nb;
+ out(cb,(b,nb,senc((c1,a,yna),kbs)));
+ in(cb,y1);
+ let (y2,y3) = y1 in
+ let (yc3,yaa,ybb,ykab,ynb) = sdec(y2,kbs) in
+ if (yc3,yaa,ybb,ynb) = (c3,a,b,nb) then
+ let (yc4,yynb) = sdec(y3,ykab) in
+ if (yc4,yynb) = (c4,nb) then
+ new k;
+ out(cb,senc(m2,k)).
+
+let S(cs,a,b,kas,kbs)=
+ in(cs,z0);
+ let (zb,znb,z1) = z0 in
+ let (zc1,za,zna) = sdec(z1,kbs) in
+ if (zc1,za,zb) = (c1,a,b) then
+ new kab;
+ out(cs,(znb, senc((c2,b,kab,zna),kas),senc((c3,a,b,kab,znb),kbs)) ).
+
+
+
+let P =
+ new kas; new kbs;
+ ( S(cs,i,b,kis,kbs) |  BP(cb,b,i,kbs)).
+
+
+let Q =
+ new kas; new kbs;
+ ( S(cs,i,b,kis,kbs) |  BQ(cb,b,i,kbs)).
+
+
+query trace_equiv(P,Q).