Adding many examples

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

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

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

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

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

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

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