Moved ISO5.psl into the done_examples folder, and the Carlsen-SK.psl specification.

4625b0ca · acholewa · c02a13db · 4625b0ca · 4625b0ca
Commit 4625b0ca authored May 14, 2015 by acholewa
Hide whitespace changes
Inline Side-by-side

Showing with 100 additions and 4 deletions

examples/done_examples/Carlsen-SK.psl examples/done_examples/Carlsen-SK.psl +96 -0

examples/done_examples/ISO5.psl examples/done_examples/ISO5.psl +4 -4

No files found.
--- a/examples/Carlsen-SK.psl
+++ b/examples/Carlsen-SK.psl
 spec Carlse-SK is
 Theory
-  types Uname Sname name Key Nonce Masterkey Sessionkey .
+  types Uname Sname Name Key Nonce Masterkey Sessionkey .
  subtype Masterkey Sessionkey < Key .
-  subtype Sname Uname < name .
-  subtype name < Public . 
+  subtype Sname Uname < Name .
+  subtype Name < Public . 

-  op n : name Fresh -> Nonce  .
+  op n : Name Fresh -> Nonce  .
  ops a b i : -> Uname [ctor] .
  op s : ->  Sname [ctor] . 
-  op mkey : name name -> Masterkey [comm] .
-  op seskey : name name Nonce -> Sessionkey .
+  op mkey : Name Name -> Masterkey [comm] .
+  op seskey : Name Name Nonce -> Sessionkey .
  op e  : Key Msg -> Msg .
  op d : Key Msg -> Msg .
  op _;_ : Msg Msg -> Msg [gather (e E)] .

+  var K : Key .
+  var Z : Msg .
  eq d(K:Key, e (K:Key, Z:Msg )) = Z:Msg .
  eq e(K:Key, d (K:Key, Z:Msg )) = Z:Msg . 

@@ -25,35 +27,37 @@ Theory
       A -> B : E(kab:nb')
    */
 Protocol
-    vars A B A1 A2 B1 : Uname .
-    var S S1 S2 : Sname .
+    vars ANAME BNAME ANAME1 ANAME2 BNAME1 : Uname .
+    var SNAME : Sname .
    vars M N MA : Msg .
    vars NA NA1 NB NB1 : Nonce .
    var K : Key .
    var SKA SKB : Sessionkey .
-    vars r r1 : Fresh .
+    vars r r1 r2 : Fresh .

-    Def(A) = na := n(A, r), kas := mkey(A, s) .
-    In(A) = A, B, S .
+    roles A B S .

-    Def(B) = nb := n(B, r), kbs := mkey(B, s), nb1 := n(B, r1) .
-    In(B) = B, S .
+    Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .
+    Def(B) = nb := n(BNAME, r), kbs := mkey(BNAME, s), 
+            nb1 := n(BNAME, r1) .
+    Def(S) = ns := n(SNAME, r2),        kab := seskey(ANAME2, BNAME1, ns),
+            ksa := mkey(ANAME2, SNAME), ksb := mkey(BNAME1, SNAME) . 

-    Def(S) = ns := n(s, r),     kab := seskey(A, B, n(s,r)),
-            ksa := mkey(A2, s), ksb := mkey(B1, s) . 
-    In(S) = S .
+    In(A) = ANAME, BNAME, SNAME .
+    In(B) = BNAME, SNAME .
+    In(S) = SNAME .

-    1 . A -> B : A  ; na
-              |- A1 ; NA  .
+    1 . A -> B : ANAME  ; na
+              |- ANAME1 ; NA  .

-    2 . B -> S : A1 ; NA  ; B  ; nb
-              |- A2 ; NA1 ; B1 ; NB .
+    2 . B -> S : ANAME1 ; NA  ; BNAME  ; nb
+              |- ANAME2 ; NA1 ; BNAME1 ; NB .

-    3 . S -> B : e(ksb, kab  ; NB ; A2)  ; e(ksa, NA1 ; B1 ; kab)
-              |- e(ks, SKB   ; nb ; A)   ; MA .
+    3 . S -> B : e(ksb, kab   ; NB ; ANAME2)   ; e(ksa, NA1 ; BNAME1 ; kab)
+              |- e(kbs, SKB   ; nb ; ANAME1)   ; MA .

-    4 . B -> A : MA                   ; e(SKB, NA) ; nb1
-              |- e(kas, na ; B ; SKA) ; e(SKA, na) ; NB1 .
+    4 . B -> A : MA                       ; e(SKB, NA) ; nb1
+              |- e(kas, na ; BNAME ; SKA) ; e(SKA, na) ; NB1 .

    5 . A -> B : e(SKA, NB1) 
              |- e(SKB, nb1) .
@@ -63,36 +67,30 @@ Protocol
    Out(S) = kab, NB, NA1 . 

 Intruder
-    vars A B : Uname .
+    vars ANAME : Uname .
    var r : Fresh .
    vars M N : Msg .
    var K : Key .

-    => A, s, n(i, r), mkey(i, s), mkey(i, A) . 
+    => ANAME, s, mkey(i, s), mkey(i, ANAME) . 
    K, M => d(K, M), e(K, M) .
    M, N <=> M ; N .

 Attacks
-    vars A B : Uname .
-    var S : Sname .
-    var SK : Sessionkey .
-    var NB1 : Nonce .
-    var r1 : Fresh .
-
    0 . 
       B executes protocol .
-       Subst(B) = A1 |-> a , B |-> b, S |-> s .
+       Subst(B) = ANAME1 |-> a , BNAME |-> b, SNAME |-> s .

    1 .
      B executes protocol .
-      Subst(B) = A1 |-> a, B |-> b, S |-> s .
-      Intruder learns SK .
+      Subst(B) = ANAME1 |-> a, BNAME |-> b, SNAME |-> s .
+      Intruder learns SKB .

    2 .
      B executes protocol .
-      Subst(B) = A1 |-> a, B |-> b, S |-> s .
+      Subst(B) = ANAME1 |-> a, BNAME |-> b, SNAME |-> s .
      without:
          A executes protocol .
-          Subst(A) = A |-> a, B |-> b, S |-> s, NB1 |-> n(b, r1) .
+          Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s, NB1 |-> n(b, r1) .

 ends
--- a/examples/ISO5.psl
+++ b/examples/ISO5.psl
@@ -39,14 +39,14 @@ Protocol

  roles A B S .

-  Def(A) = na := n(ANAME, r), kas := mkey(ANAME, SNAME) .
+  Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .

  In(A)  = ANAME, BNAME, SNAME .

-  Def(B) = nb := n(BNAME, r), nb1 := n(BNAME, r'), kbs := mkey(BNAME,SNAME) .
+  Def(B) = nb := n(BNAME, r), nb1 := n(BNAME, r'), kbs := mkey(BNAME,s) .
  In(B)  = BNAME, SNAME .

-  Def(S) = ksa := mkey(AS,SNAME), ksb := mkey(BS,SNAME), 
+  Def(S) = ksa := mkey(AS, s), ksb := mkey(BS, s), 
           kab := seskey(AS, BS, n(s,r)) .
  In(S) = SNAME .

@@ -75,7 +75,7 @@ Intruder
   vars M N : Msg .
   var r : Fresh .

-   => C, s, mkey(i, D), mkey(i, s), n(i, r) .
+   => C, s, mkey(i, D), mkey(i, s) .
   K, M => d(K, M), e(K, M) .
   M, N <=> M ; N .