Commit fc709c75 authored by acholewa's avatar acholewa

Added db.psl to our done examples.

parent a5a7df1d
...@@ -19,17 +19,19 @@ Theory ...@@ -19,17 +19,19 @@ Theory
Protocol Protocol
vars A B : Name . vars ANAME BNAME : Name .
vars N NA : Nonce . vars N NA : Nonce .
var r : Fresh . var r : Fresh .
In(A) = A, B, N . roles A B .
In(B) = A, B, N .
1 . A -> B : n(A, r) |- NA . In(A) = ANAME, BNAME, N .
2 . B -> A : N * NA |- N * n(A, r) . In(B) = ANAME, BNAME, N .
Out(A) = n(A, r), N * n(A, r) . 1 . A -> B : n(ANAME, r) |- NA .
2 . B -> A : N * NA |- N * n(ANAME, r) .
Out(A) = n(ANAME, r), N * n(ANAME, r) .
Out(B) = NA, N * NA . Out(B) = NA, N * NA .
Intruder Intruder
...@@ -41,9 +43,8 @@ Intruder ...@@ -41,9 +43,8 @@ Intruder
X, Y => X * Y . X, Y => X * Y .
Attacks Attacks
vars A B : Name .
0 . 0 .
B executes protocol . B executes protocol .
Subst(B) = A |-> a, B |-> b . Subst(B) = ANAME |-> a, BNAME |-> b .
ends ends
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment