Skip to content
GitLab
Commit 7d45bd99 authored by acholewa's avatar acholewa
Browse files

Merge branch 'master' of https://github.com/archolewa/Maude-PSL

parents 3014b25a e3c0bcc9
Hide whitespace changes
Inline Side-by-side
PSL-Syntax.maude
View file @ 7d45bd99
......@@ -381,6 +381,7 @@ fmod ATTACK-SYNTAX is
op _|->_ : Msg MsgNumSet -> MsgPair [prec 30] .
op $none : -> MsgPairs .
op __ : MsgPairs MsgPairs -> MsgPairs [ctor assoc comm id: $none] .
op _$$$;;;$$$_ : [MsgPairs] [MsgPairs] -> [MsgPairs] [ctor assoc comm id: $none] .
---Stores the information on an invalid substitution. The Python code
---invoking this Maude code then scans the output for the presence of
---this term. If the Python code finds this term, then it extracts the
......
README.txt
View file @ 7d45bd99
Usage: ./psl.py <FILENAME>.psl
The program will generate two files:
<FILENAME>.pslmaude, <FILENAME>.maude.
or
<FILENAME>.pslmaude is a transitionary file that is loaded into Maude, and can be
ignored
by the user (unless they need to investigate an error message). <FILENAME>.maude
./psl.sh <FILENAME>.sh
The difference is that the second command also automatically loads the
generated Maude file into Maude-NPA, along with all the other files that
Maude-NPA needs to run properly, using the version of Maude included in the
repository (maude27 as of May 14 2015). Note that if you invoke the shell
script, then Maude-NPA will be loaded whether or not the PSL script
successfully executes. So invoking psl.py is recommended until the
specification is well-formed.
The program will generate one files:
<FILENAME>.maude.
<FILENAME>.maude
contains the Maude-NPA modules that can be loaded into the Maude-NPA.
Note that although the translation program itself works with Maude 2.6, the Maude-NPA
Note that although the translation program itself works with Maude 2.6, the
Maude-NPA
version
that the generated modules are compatible with relies on a version of Maude that is
not-quite-ready for release. Therefore, in addition to the translation code, included
are experimental versions of Maude, the Maude prelude, and the Maude-NPA that these
modules are compatible with.
that the generated modules are compatible with relies on a version of Maude
that is
not-quite-ready for release. Therefore, in addition to the translation code,
included
is an experimental version of Maude, the Maude prelude, and the Maude-NPA that
these modules are compatible with.
To load <FILENAME>.maude into the Maude-NPA, type:
./maude96c -no-prelude prelude.maude maude-npa.maude <FILENAME>.maude
./maude27 -no-prelude prelude.maude maude-npa.maude <FILENAME>.maude
For more details about PSL, see psl_description.pdf (a draft of Andrew Cholewa's
Spring 2015 Masters Thesis at University of Illinois at Urbana-Champaign),
included with this repository.
Dependent Python libraries:
fuzzywuzzy
examples/Denning-Sacco.psl
View file @ 7d45bd99
......@@ -14,36 +14,39 @@ Theory
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg .
eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
Protocol
vars A B AS BS AB : UName .
var S : SName .
var D : Name .
vars ANAME BNAME AS BS AB : UName .
var SNAME : SName .
vars r r' : Fresh .
vars TS TSB : Nonce .
vars TSA TSB : Nonce .
var K : Key .
vars SK SK1 SKA SKB : Sessionkey .
vars M N X Y : Msg .
Def(A) = kas := mkey(A, S) .
In(A) = A, B, S .
roles A B S .
Def(B) = kbs := mkey(B, S) .
In(B) = B, S .
In(A) = ANAME, BNAME, SNAME .
In(B) = BNAME, SNAME .
In(S) = SNAME .
Def(S) = kab := seskey(A, B, n(S,r)), ts := t(S, r'),
ksa := mkey(AS, S), ksb := mkey(BS, S) .
In(S) = S .
Def(A) = kas := mkey(ANAME, SNAME) .
Def(B) = kbs := mkey(BNAME, SNAME) .
Def(S) = kab := seskey(AS, BS, n(SNAME,r)), ts := t(SNAME, r'),
ksa := mkey(AS, SNAME), ksb := mkey(BS, SNAME) .
1 . A -> S : A ; B |- AS ; BS .
2 . S -> A : e(ksa, BS ; kab ; ts ; e(ksb, AS ; kab ; ts))
|- e(kas, B ; SKA ; TS ; M) .
1 . A -> S : ANAME ; BNAME |- AS ; BS .
2 . S -> A : e(ksa, BS ; kab ; ts ; e(ksb, AS ; kab ; ts))
|- e(kas, BNAME ; SKA ; TSA ; M) .
3 . A -> B : M |- e(kbs, AB ; SKB ; TSB) .
......@@ -58,26 +61,23 @@ Intruder
var K : Key .
vars M N : Msg .
=> D, n(i, r), t(i, r), mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
=> D, n(i, r), t(i, r) .
=> mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
M, N <=> M ; N .
Attacks
vars A B : UName .
var S : SName .
var SK : Sessionkey .
0 .
A executes protocol .
Subst(A) = A |-> a , B |-> b, S |-> s .
Subst(A) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
1 .
A executes protocol .
Subst(A) = A |-> a , B |-> b, S |-> s .
Subst(A) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
Intruder learns SKA .
2 .
S executes protocol .
Subst(S) = AS |-> a, BS |-> b, S |-> s .
Subst(S) = AS |-> a, BS |-> b, SNAME |-> s .
Intruder learns kab .
ends
examples/Kao-Chow.psl
View file @ 7d45bd99
......@@ -14,9 +14,11 @@ Theory
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg .
eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
/*
A -> S : A , B , na
......@@ -25,8 +27,8 @@ Theory
A -> B : E(kab:nb)
*/
Protocol
vars A B : UName .
var S : SName .
vars ANAME BNAME : UName .
var SNAME : SName .
vars MA M N : Msg .
vars r r1 r2 : Fresh .
var NAB : Nonce .
......@@ -34,24 +36,26 @@ Protocol
var NAS NBS : Nonce .
var NBA : Nonce .
Def(A) = na := n(A, r), kas := mkey(A, s) .
In(A) = A, B, S .
roles A B S .
Def(B) = nb := n(A, r1), kbs := mkey(B, s) .
In(B) = A, B, S .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
Def(S) = kas := mkey(A, s), kbs := mkey(B, s), kab := seskey(A,B,n(s,r2)) .
In(S) = A, B, S .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .
Def(B) = nb := n(ANAME, r1), kbs := mkey(BNAME, s) .
Def(S) = kas := mkey(ANAME, s), kbs := mkey(BNAME, s),
kab := seskey(ANAME,BNAME,n(s,r2)) .
1 . A -> S : A ; B ; na
|- A ; B ; NAS .
1 . A -> S : ANAME ; BNAME ; na
|- ANAME ; BNAME ; NAS .
2 . S -> B : e(kas, A ; B ; NAS ; kab) ; e(kbs, A ; B ; NAS ; kab)
|- MA ; e(kbs, A ; B ; NAB ; SKB) .
2 . S -> B : e(kas, ANAME ; BNAME ; NAS ; kab) ; e(kbs, ANAME ; BNAME ; NAS ; kab)
|- MA ; e(kbs, ANAME ; BNAME ; NAB ; SKB) .
3 . B -> A : MA ; e(SKB, NAB) ; nb
|- e(kas, A ; B ; na ; SKA) ; e(SKA, na) ; NBA .
3 . B -> A : MA ; e(SKB, NAB) ; nb
|- e(kas, ANAME ; BNAME ; na ; SKA) ; e(SKA, na) ; NBA .
4 . A -> B : e(SKA, NBA)
|- e(SKB, nb) .
......@@ -67,35 +71,25 @@ Intruder
var K : Key .
vars M N : Msg .
=> D, n(i, r), mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
=> D, n(i, r), mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
M ; N <=> M, N .
Attacks
vars A B : UName .
var S : SName .
var SK : Sessionkey .
var NBA : Nonce .
var r : Fresh .
0 .
In(B) = A |-> a, B |-> b, S |-> s .
B executes protocol .
Out(B) = ditto .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
1 .
In(B) = A |-> a, B |-> b, S |-> s .
B executes protocol .
Intruder learns SK .
Out(B) = ditto .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
Intruder learns SKB .
2 .
In(B) = A |-> a, B |-> b, S |-> s .
B executes protocol .
Out(B) = ditto .
without:
In(A) = A |-> a, B |-> b, S |-> s .
A executes protocol .
Out(A) = NBA |-> n(b, r), ditto .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
without:
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
ends
examples/Woolam.psl
View file @ 7d45bd99
......@@ -14,8 +14,10 @@ Theory
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
eq d(K:Key, e(K:Key, Z:Msg )) = Z:Msg .
eq e(K:Key, d(K:Key, Z:Msg )) = Z:Msg .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
/*
......@@ -27,36 +29,35 @@ Theory
*/
Protocol
vars A B : UName .
var S : SName .
vars NB : Nonce .
vars ANAME BNAME : UName .
var SNAME : SName .
vars NB NBS : Nonce .
vars MA M N : Msg .
var r : Fresh .
var K : Key .
var D : Name .
Def(A) = kas := mkey(A, s) .
In(A) = A, B, S .
roles A B S .
Def(B) = nb := n(B,r), kbs := mkey(B, s) .
In(B) = A, B, S .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
Def(S) = kas := mkey(A,s), kbs := mkey(B,s) .
In(S) = A, B, S .
Def(A) = kas := mkey(ANAME, s) .
Def(B) = nb := n(BNAME,r), kbs := mkey(BNAME, s) .
Def(S) = kas := mkey(ANAME,s), kbs := mkey(BNAME,s) .
1 . A -> B : A |- A .
1 . A -> B : ANAME |- ANAME .
//This is very very prone to typos. We need to come up with a better naming convention for macros. I'm thinking all lower-case. It might clash a little bit with
//constants, but constants are rarely used in the protocol declaration.
2 . B -> A : nb |- NB .
3 . A -> B : e(kas, NB) |- MA .
4 . B -> S : e(kbs, A ; MA)
|- e(kbs, A ; e(kas, NB)) .
4 . B -> S : e(kbs, ANAME ; MA)
|- e(kbs, ANAME ; e(kas, NBS)) .
5 . S -> B : e(kbs, NB)
|- e(kbs, nb) .
5 . S -> B : e(kbs, NBS)
|- e(kbs, nb) .
Out(A) = NB .
Out(B) = nb .
......@@ -64,20 +65,19 @@ Protocol
Intruder
=> D:Name, n(i, r:Fresh), mkey(D:Name, i), mkey(i, D:Name) .
K:Key, M:Msg => d(K:Key, M:Msg), e(K:Key, M:Msg) .
M:Msg, N:Msg <=> M:Msg ; N:Msg .
var D : Name .
var r : Fresh .
var K : Key .
vars M N : Msg .
=> D, n(i, r), mkey(D, i), mkey(i, D) .
K, M => d(K, M), e(K, M) .
M, N <=> M ; N .
Attacks
vars A B : UName .
var S : SName .
//Empty attack for debugging purposes. If an "attack" isn't found, then there's something wrong with the specification.
//Empty attack for debugging purposes. If an "attack" isn't found, then
//there's something wrong with the specification.
0 .
In(B) = A |-> a , B |-> b, S |-> s .
B executes protocol .
Out(B) = ditto .
Subst(B) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
ends
examples/Yahalom.psl
View file @ 7d45bd99
spec Yahalom 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 .
op seskey : name name Nonce -> Sessionkey .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
......@@ -25,74 +25,68 @@ Theory
A -> B : E(kbs:A,kab),E(kab:nb)
*/
/*
Note: The variable scoping here makes no sense. Ostensibly, the SK in Protocol, and the SK in Attacks should be different values. However, they're meant to represent the same
value. So, it seems like we should allow global variable declarations. Of course, the way the code is currently structured, implementing that won't exactly be trivial.
*/
Protocol
vars A B : Uname .
var S : Sname .
vars NA NB : Nonce .
vars ANAME BNAME : Uname .
var SNAME : Sname .
vars NA NBA NAS NBS : Nonce .
var r : Fresh .
var M N MB : Msg .
var SK : Sessionkey .
var D : name .
var SKA SKB : Sessionkey .
var D : Name .
var K : Key .
Def(A) = na := n(A, r), kas := mkey(A,s) .
In(A) = A, B, S .
roles A B S .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME,s) .
Def(B) = nb := n(B, r), kbs := mkey(B,s) .
In(B) = A, B, S .
Def(B) = nb := n(BNAME, r), kbs := mkey(BNAME,s) .
Def(S) = kas := mkey(A, s), kbs := mkey(B, s), kab := seskey(A , B , n(s,r)) .
In(S) = A, B, S .
Def(S) = kas := mkey(ANAME, s), kbs := mkey(BNAME, s),
kab := seskey(ANAME , BNAME , n(s,r)) .
1 . A -> B : A ; na
|- A ; NA .
1 . A -> B : ANAME ; na
|- ANAME ; NA .
2 . B -> S : B ; e(kbs, A ; NA ; nb)
|- B ; e(kbs, A ; NA ; NB) .
2 . B -> S : BNAME ; e(kbs, ANAME ; NA ; nb)
|- BNAME ; e(kbs, ANAME ; NAS ; NBS) .
3 . S -> A : e(kas, B ; kab ; NA ; NB) ; e(kbs, A ; kab)
|- e(kas, B ; SK ; na ; NB) ; MB .
3 . S -> A : e(kas, BNAME ; kab ; NAS ; NBS) ; e(kbs, ANAME ; kab)
|- e(kas, BNAME ; SKA ; na ; NBA) ; MB .
4 . A -> B : MB ; e(SK, NB)
|- e(kbs, A ; SK) ; e(SK, nb) .
4 . A -> B : MB ; e(SKA, NBA)
|- e(kbs, ANAME ; SKB) ; e(SKB, nb) .
Out(A) = na, NB, SK .
Out(B) = NA, nb, SK .
Out(S) = NA, NB, kab .
Out(A) = na, NBA, SKA .
Out(B) = NA, nb, SKB .
Out(S) = NA, NBS, kab .
Intruder
=> D:Name, n(i, r:Fresh), mkey(i, A:Name), mkey(A:Name, i), mkey(i, s) .
K:Key, M:Msg => d(K:Key, M:Msg), e(K:Key, M:Msg) .
M:Msg ; N:Msg <=> M:Msg, N:Msg .
vars C D : Name .
var r : Fresh .
var K : Key .
vars M N : Msg .
=> D, n(i, r), mkey(i, C), mkey(C, i), mkey(i, s) .
K, M => d(K, M), e(K, M) .
M ; N <=> M, N .
Attacks
vars A B : UName .
var S : SName .
var SK : Sessionkey .
0 .
In(B) = A |-> a , B |-> b, S |-> s .
B executes protocol .
Out(B) = ditto .
Subst(B) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
1 .
In(B) = A |-> a , B |-> b, S |-> s .
B executes protocol .
Intruder learns SK .
Out(B) = ditto .
Subst(B) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
Intruder learns SKB .
2 .
In(B) = A |-> a, B |-> b, S |-> s .
B executes protocol .
Out(B) = ditto .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
without:
In(A) = A |-> a, B |-> b, S |-> s .
A executes protocol .
Out(A) = NB |-> n(b, r), ditto .
Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s, NBA |-> n(b, r) .
ends
examples/dh.psl
View file @ 7d45bd99
......@@ -29,26 +29,32 @@ Theory
op _;_ : Msg Msg -> Msg [gather (e E)] .
eq exp(exp(W:Gen,Y:NeNonceSet),Z:NeNonceSet) = exp(W:Gen, Y:NeNonceSet * Z:NeNonceSet) .
eq e(K:Key,d(K:Key,M:Msg)) = M:Msg .
eq d(K:Key,e(K:Key,M:Msg)) = M:Msg .
var W : Gen .
vars Y Z : NeNonceSet .
var K : Key .
var M : Msg .
eq exp(exp(W,Y),Z) = exp(W, Y * Z) .
eq e(K,d(K,M)) = M .
eq d(K,e(K,M)) = M .
Protocol
vars ANAME BNAME : Name .
vars ANAME BNAME ANAME1 : Name .
vars r r' r1 : Fresh .
vars XEA XEB : Exp .
var S : Secret .
roles A B .
In(A) = ANAME, BNAME .
In(B) = B .
In(B) = BNAME .
Def(A) = na := n(ANAME, r), secret := sec(ANAME, r') .
Def(B) = nb := n(BNAME, r1) .
1 . A -> B : A ; B ; exp(g, na)
|- A1 ; B ; XEB .
2 . B -> A : A1 ; B ; exp(g, nb)
|- A ; B ; XEA .
1 . A -> B : ANAME ; BNAME ; exp(g, na)
|- ANAME1 ; BNAME ; XEB .
2 . B -> A : ANAME1 ; BNAME ; exp(g, nb)
|- ANAME ; BNAME ; XEA .
3 . A -> B : e(exp(XEA, na), secret)
|- e(exp(XEB, nb), S) .
......@@ -56,17 +62,17 @@ Protocol
Out(B) = nb, exp(g, nb), XEA, S .
Intruder
vars A : Name .
vars NAME : Name .
var K : Key .
vars M M1 M2 : Msg .
vars NS1 NS2 : NeNonceSet .
var GE : GenvExp .
var r : Fresh .
=> n(i, r), g, A .
=> n(i, r), g, NAME .
M1 ; M2 <=> M1, M2 .
K, M => e(K, M), d(K, M) .
NS1, NS2 => NS1 * NS2 .
GE, NS1 => exp(GE, NS1) .
K, M => e(K, M), d(K, M) .
NS1, NS2 => NS1 * NS2 .
GE, NS1 => exp(GE, NS1) .
Attacks
/*
......@@ -74,26 +80,15 @@ Attacks
properly. If this "attack" does not find an initial state, then this
protocol was implemented incorrectly.
*/
vars A B : Name
var S : Secret .
0 .
B executes protocol .
Subst(B) = A1 |-> a, B |-> b, S |-> sec(a, r') .
Subst(B) = ANAME1 |-> a, BNAME |-> b, S |-> sec(a, r') .
without:
Subst(A) = A |-> a, B |-> b .
Subst(A) = ANAME |-> a, BNAME |-> b .
A executes protocol .
1 .
B executes protocol .
Subst(B) = A1 |-> a, B |-> b, S |-> sec(a, r') .
Subst(B) = ANAME1 |-> a, BNAME |-> b, S |-> sec(a, r') .
Intruder learns sec(a, r') .
/*
Note: Attack 2 in the dh.maude example is identical to attack 1 above,
except that it includes never patterns for avoiding unreachable states.
This language isn't expressive enough for that kind of optimization.
However, that's an optimization that should probably be performed at the
lower Maude-NPA strand level, because optimizations run the risk of losing
completenes, in which case you should only perform them if you *really*
know what you're doing.
*/
ends
examples/done_examples/Amended-Needham-Schroeder.maude deleted 100644 → 0
View file @ 3014b25a
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES .
sorts SName Name Key Nonce Masterkey Sessionkey .
subsorts Masterkey Sessionkey < Key .
subsorts SName < Name .
subsorts Name < Public .
op n : Name Fresh -> Nonce [ frozen ] .
op a : -> Name .
op b : -> Name .
op i : -> Name .
op s : -> SName .
op mkey : Name Name -> Masterkey [ frozen ] .
op seskey : Name Name Nonce -> Sessionkey [ frozen ] .
op e : Key Msg -> Msg [ frozen ] .
op d : Key Msg -> Msg [ frozen ] .
op dec : Nonce -> Msg [ frozen ] .
op null : -> Msg .
op _;_ : Msg Msg -> Msg [ gather ( e E ) frozen ] .
op t : -> Msg .
subsorts SName Name Key Nonce Masterkey Sessionkey < Msg .
op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen].
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg [ variant ] .
eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg [ variant ] .
endfm
fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
eq STRANDS-DOLEVYAO =
:: nil ::
[ nil |
+(s), nil] &
:: nil ::
[ nil |
+(A:Name), nil] &
:: nil ::
[ nil |
+(mkey(i, s)), nil] &
:: nil ::
[ nil |
+(mkey(i, A:Name)), nil] &
:: nil ::
[ nil |
+(mkey(s, i)), nil] &
:: nil ::
[ nil |
+(mkey(A:Name, i)), nil] &
:: nil ::
[ nil |
-(M1:Msg),
-(M:Msg),
+(M:Msg ; M1:Msg), nil] &
:: nil ::
[ nil |
-(N:Nonce),
+(dec(N:Nonce)), nil] &
:: nil ::
[ nil |