Commit 190208ef authored by acholewa's avatar acholewa

Initial commit to the public repository. Contains all the files needed to run...

Initial commit to the public repository. Contains all the files needed to run Maude-PSL, as well as an examples directory, and a directory of the original npa-examples for use of comparisions with the Maude-PSL examples. Also contains a pdf file containing a description of the language.
parents
This diff is collapsed.
This diff is collapsed.
Usage: ./psl.py <FILENAME>.psl
The program will generate two files:
<FILENAME>.pslmaude, <FILENAME>.maude.
<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
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
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.
To load <FILENAME>.maude into the Maude-NPA, type:
./maude96c -no-prelude prelude.maude maude-npa.maude <FILENAME>.maude
Dependent Python libraries:
fuzzywuzzy
load psl.maude
select COMP-TRANSLATION-TO-MAUDE-NPA .
rew [comp(1, 2) |->
nsl-A ;1 db-B : A |-> B, B |-> A, NO |-> n(A, r:Fresh) .[3]
nsl-B ;1 db-A : B |-> A1, A |-> B, NO |-> NA1 .[3]
]
[mt]
---Only here for purposes of debugging.
---Note: This should be added by Python if there are no attacks.
[$emptyAttackData]
translate(1,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(nsl-A) = A, B .[1]
In(nsl-B) = B .[1]
1 . nsl-A -> nsl-B : pk(B, n(A, r:Fresh) ; A) |-
pk(B, NA1 ; A1) .[1]
2 . nsl-B -> nsl-A : pk(A1, NA1 ; n(B, r1:Fresh) ; B) |-
pk(A , n(A, r:Fresh) ; NB ; B) .[1]
3 . nsl-A -> nsl-B : pk(B, NB) |-
pk(B, n(B, r1:Fresh)) .[1]
Out(nsl-A) = A, B, n(A, r:Fresh), NB, h(n(A, r:Fresh) ; NB) .[1]
Out(nsl-B) = A1, B, NA1, n(B, r1:Fresh), h(NA1 ; n(B, r1:Fresh)) .[1]
}
Intruder
{
=> C .[1]
X, Y <=> X ; Y .[1]
X => sk(i, X) .[1]
K, X => pk(K, X) .[1]
}
Attacks
{
0 .
{
nsl-B executes protocol .[1]
Intruder learns n(B, r1:Fresh) .[1]
Subst(nsl-B) = B |-> b, A1 |-> a .[1]
}
}
}
)
translate(2,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(db-A) = A, B, NO .[2]
In(db-B) = A, B, NO .[2]
1 . db-A -> db-B : n(A, r:Fresh) |- NA .[2]
2 . db-B -> db-A : NO * NA |- NO * n(A, r:Fresh) .[2]
Out(db-A) = n(A, r:Fresh), NO * n(A, r:Fresh) .[2]
Out(db-B) = NA, NO * NA .[2]
}
Intruder
{
=> C, n(i, r:Fresh) .[2]
X, Y => X * Y .[2]
}
Attacks
{
0 .
{
db-B executes protocol .[2]
Subst(db-B) = A |-> a, B |-> b .[2]
}
}
}
) .
---Only for debugging.
load psl.maude
select COMP-TRANSLATION-TO-MAUDE-NPA .
set print attribute off .
rew
[comp(1, 2) |->
nsl-A ;* kd-B : A |-> B, B |-> A, K |-> h(n(A, r) ; NB) .[3]
nsl-B ;* kd-A : A |-> B, B |-> A1, K |-> h(NA1 ; n(B, r1)) .[3]
nsl-A ;* kd-A : A |-> A, B |-> B, K |-> h(n(A, r) ; NB) .[3]
nsl-B ;* kd-B : A |-> A1, B |-> B, K |-> h(NA1 ; n(B, r1)) .[3]
]
[mt]
---Only here for purposes of debugging.
---Note: This should be added by Python if there are no attacks.
[$emptyAttackData]
translate(1,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(nsl-A) = A, B .[1]
In(nsl-B) = B .[1]
1 . nsl-A -> nsl-B : pk(B, n(A, r:Fresh) ; A) |-
pk(B, NA1 ; A1) .[1]
2 . nsl-B -> nsl-A : pk(A1, NA1 ; n(B, r1:Fresh) ; B) |-
pk(A , n(A, r:Fresh) ; NB ; B) .[1]
3 . nsl-A -> nsl-B : pk(B, NB) |-
pk(B, n(B, r1:Fresh)) .[1]
Out(nsl-A) = A, B, n(A, r:Fresh), NB, h(n(A, r:Fresh) ; NB) .[1]
Out(nsl-B) = A1, B, NA1, n(B, r1:Fresh), h(NA1 ; n(B, r1:Fresh)) .[1]
}
Intruder
{
=> C .[1]
X, Y <=> X ; Y .[1]
X => sk(i, X) .[1]
K, X => pk(K, X) .[1]
}
Attacks
{
0 .
{
nsl-B executes protocol .[1]
Intruder learns n(B, r1:Fresh) .[1]
Subst(nsl-B) = B |-> b, A1 |-> a .[1]
}
}
}
)
translate(2,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(kd-A) = A, B, K .[2]
In(kd-B) = A, B, K .[2]
1 . kd-A -> kd-B : e(K, skey(A, r)) |-
e(K, SK) .[2]
2 . kd-B -> kd-A : e(K, SK ; n(B, r1)) |-
e(K, skey(A, r) ; NB) .[2]
3 . kd-A -> kd-B : e(K, NB) |-
e(K, n(B, r1)) .[2]
Out(kd-A) = K, skey(A, r), NB .[2]
Out(kd-B) = A, B, K, SK, n(B, r1) .[2]
}
Intruder
{
=> C, n(i, r), skey(i, r) .[2]
K, X => e(K, X), d(K, X) .[2]
X, Y <=> X ; Y .[2]
}
Attacks
{
0 .
{
kd-B executes protocol .[2]
Subst(kd-B) = A |-> a, B |-> b .[2]
}
}
}
) .
q
Specification{
Protocol{
In(kd-A)= K,A,B .[2] .
In(kd-B)= K,A,B .[2]
1 . kd-A -> kd-B : e(K,skey(A, r)) |- e(K,SK) .[2] .
q
2 . kd-B -> kd-A : e(K,SK ; n(B, r1)) |- e(K,skey(A, r) ; NB) .[2]
3 . kd-A -> kd-B : e(K,NB) |- e(K,n(B, r1)) .[2]
Out(kd-A)= K,NB,skey(A, r) .[2]
Out(kd-B)= K,SK,A,B,n(B, r1) .[2]
}
Intruder{
emptyMsgSet => C .[2]
emptyMsgSet => skey(i, r) .[2]
emptyMsgSet => n(i, r) .[2]
K,X => e(K,X),d(K,X) .[2]
X,Y => X ; Y .[2]
X ; Y => X .[2]
X ; Y => Y .[2]
}
Attacks{
0 .{kd-B executes protocol .[2] Subst(kd-B)= A |-> a,B |-> b .[
2]}
}}
.
--- Direct Composition
--- NSL-Distance Bounding protocol
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Synchronization for composition
subsort Role < Msg .
--- Roles
ops init-nsl resp-nsl : -> Role .
ops init-db resp-db : -> Role .
--- Sort Information
sorts Name Nonce NonceSet Enc .
subsort Name NonceSet Enc < Msg .
subsort Nonce < NonceSet .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Name Msg -> Enc [frozen] .
op sk : Name Msg -> Enc [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Concatenation operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
--- Exclusive-or operator
op _*_ : NonceSet NonceSet -> NonceSet [assoc comm frozen] .
op null : -> NonceSet .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
--- Variables
vars X Y Z : Msg .
vars A B : Name .
vars XN YN : NonceSet .
*** Encryption/Decryption Cancellation
eq pk(A,sk(A,Z)) = Z [variant] .
eq sk(A,pk(A,Z)) = Z [variant] .
*** Exclusive or properties
eq null * XN = XN [variant] .
eq XN * XN = null [variant] .
eq XN * XN * YN = YN [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
vars r r' r'' r# : Fresh .
vars A B C : Name .
vars NA NB N N' : Nonce .
vars NS NS' : NonceSet .
vars X Y Z H : Msg .
vars P Q : Name .
eq STRANDS-DOLEVYAO
=
:: nil :: [ nil | -(NS), -(NS'), +(NS * NS'), nil ] &
:: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(A,X)), nil ] &
:: nil :: [ nil | +(A) , nil ] &
:: r :: [ nil | +(n(i,r)), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r :: --- NSL-Alice
[ nil | +(pk(B, n(A,r) ; A)) ,
-(pk(A, n(A,r) ; NB ; B )),
+(pk(B, NB)),
{init-nsl -> resp-db ;; 1-1 ;; A ; B ; n(A,r)},
nil ] &
:: r :: --- NSL-Bob
[ nil | -(pk(B,NA ; A)),
+(pk(A, NA ; n(B,r) ; B)),
-(pk(B,n(B,r))),
{resp-nsl -> init-db ;; 1-1 ;; A ; B ; NA},
nil ] &
:: r' ::
[ nil | {resp-nsl -> init-db ;; 1-1 ;; A ; B ; NA},
+(n(B,r')),
-(NA * n(B,r')), nil] &
:: nil ::
[ nil | {init-nsl -> resp-db ;; 1-1 ;; A ; B ; NA },
-(N),
+(NA * N), nil ]
[nonexec] .
var NC : Nonce .
--- Attack pattern to find Distance Hijacking attack
eq ATTACK-STATE(0)
= :: r ::
[ nil , +(pk(C,n(a,r) ; a)),
-(pk(a, n(a,r) ; NC ; C )),
+(pk(C, NC)) |
{init-nsl -> resp-db ;; 1-1 ;; a ; C ; n(a,r)},
nil] &
:: r' ::
[ nil, {resp-nsl -> init-db ;; 1-1 ;; P ; b ; n(a,r)},
+(n(b,r')), -(n(a,r) * n(b,r')) | nil]
|| (a != P) , (C != b )
|| nil
|| nil
|| nil
[nonexec] .
--- Attack pattern to find Simpler attack
eq ATTACK-STATE(1)
= :: r ::
[ nil , +(pk(C,n(a,r) ; a)) |
-(pk(a, n(a,r) ; NC ; C )),
+(pk(C, NC)),
{init-nsl -> resp-db ;; 1-1 ;; a ; C ; n(a,r)},
nil] &
:: r' ::
[ nil, {resp-nsl -> init-db ;; 1-1 ;; P ; b ; n(a,r)},
+(n(b,r')), -(n(a,r) * n(b,r')) | nil]
|| (a != P) , (C != b )
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . --- -1
sorts Name Nonce Key .
subsort Name < Key .
subsort Name < Public .
subsorts Name Nonce Key < Msg .
ops pk sk : Key Msg -> Msg .
op n : Name Fresh -> Nonce .
ops a b i : -> Name . --- Alice Bob Intruder
op _;_ : Msg Msg -> Msg [gather (e E)] .
op h : Msg -> Key .
op _*_ : Msg Msg -> Msg [assoc comm] .
op 0 : -> Msg .
---------------Automatically generated and added by Python------------
ops nsl-A nsl-B : -> Role .
ops db-A db-B : -> Role .
---Used for building the message for the synchronization message.
op _$;_ : Msg Msg -> Msg [gather(E e)] .
----------End Automatically generated and added by Python-------------------
endfm
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . --- -1
sorts Name Nonce Key .
subsort Name < Key .
subsort Name < Public .
ops pk sk : Key Msg -> Msg [frozen] .
op n : Name Fresh -> Nonce [frozen] .
ops a b i : -> Name . --- Alice Bob Intruder
op _;_ : Msg Msg -> Msg [frozen gather (e E)] .
op h : Msg -> Key [frozen] .
var Z : Msg .
var K : Key .
op 0 : -> Msg .
op n : Name Fresh -> Nonce [frozen] .
op _*_ : Msg Msg -> Msg [assoc comm frozen] .
---------------Automatically generated and added by Python------------
subsorts Name Nonce Key < Msg .
ops NSL-init NSL-resp : -> Role .
ops DB-init DB-resp : -> Role .
---Used for building the message for the synchronization message.
---op _$;_ : Msg Msg -> Msg [gather(E e) frozen] .
----------End Automatically generated and added by Python-------------------
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
var Z : Msg .
var K : Key .
---Encryption/Decryption Cancellation
eq pk(K,sk(K,Z)) = Z [variant] .
eq sk(K,pk(K,Z)) = Z [variant] .
vars X Y : Msg .
eq X * X = 0 [variant] .
eq X * 0 = X [variant] .
eq X * X * Y = Y [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS . protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
vars A B A1 : Name .
vars NA1 NB : Nonce .
var C : Name .
vars X Y : Msg .
var K : Key .
var NA : Nonce .
var NO : Nonce .
eq STRANDS-DOLEVYAO =
:: nil ::
[ nil |
+(C), nil] &
:: nil ::
[ nil |
-(X),
+(sk(i, X)), nil] &
:: nil ::
[ nil |
-(X),
-(K),
+(pk(K, X)), nil] &
:: nil ::
[ nil |
-(Y),
-(X),
+(X ; Y), nil] &
:: nil ::
[ nil |
-(Y),
-(X),
+(X * Y), nil] &
:: nil ::
[ nil |
-(X ; Y),
+(X), nil] &
:: nil ::
[ nil |
-(X ; Y),
+(Y), nil] &
:: r:Fresh ::
[ nil |
+(n(i, r:Fresh)), nil] [nonexec] .
vars r r' : Fresh .
var N : Nonce .
eq STRANDS-PROTOCOL =
:: r :: [nil | +(pk(B, n(A, r) ; A)),
-(pk(A, n(A, r) ; NB ; B)),
+(pk(B, NB)),
{NSL-init -> DB-resp ;; 1-1 ;; A ; B ; n(A, r)}, nil] &
:: r :: [nil | -(pk(B, NA ; A)),
+(pk(A, NA ; n(B, r) ; B)),
-(pk(B, n(B,r))),
{NSL-resp -> DB-init ;; 1-1 ;; A ; B ; NA}, nil] &
:: r' :: [nil | {NSL-resp -> DB-init ;; 1-1 ;; A ; B ; NA},
+(n(B, r')),
-(NA * n(B, r')), nil] &
:: nil :: [nil | {NSL-init -> DB-resp ;; 1-1 ;; A ; B ; NA },
-(N),
+(NA * N), nil] [nonexec] .
var NC : Nonce .
var D : Name .
eq ATTACK-STATE(0) =
:: r ::
[nil, +(pk(C, n(a, r) ; a)) |
-(pk(a, n(a, r) ; NC ; C)),
+(pk(C, NC)),
{NSL-init -> DB-resp ;; 1-1 ;; a ; C ; n(a, r)}, nil] &
:: r' ::
[nil, {NSL-resp -> DB-init ;; 1-1 ;; D ; b ; n(a, r)},
+(n(b, r')), -(n(a, r) * n(b, r')) | nil]
|| (a != D), (C != b)
|| nil
|| nil
|| nil
[nonexec] .
eq ATTACK-STATE(1) =
:: r ::
[nil, +(pk(b, n(a, r) ; a)),
-(pk(a, n(a, r) ; NC ; b)),
+(pk(b, NC)),
{NSL-init -> DB-resp ;; 1-1 ;; a ; b ; n(a, r)} | nil] &
:: r' ::
[nil, {NSL-resp -> DB-init ;; 1-1 ;; a ; b ; n(a, r)},
+(n(b, r')), -(n(a, r) * n(b, r')) | nil]
|| empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
select MAUDE-NPA .
red genGrammars .
---red run(1, unbounded) .
---red run(0, 13) .
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . --- -1
sorts Name Nonce Key .
subsort Name < Key .
subsort Name < Public .
subsorts Name Nonce Key < Msg .
ops pk sk : Key Msg -> Msg [frozen] .
op n : Name Fresh -> Nonce [frozen] .
ops a b i : -> Name . --- Alice Bob Intruder
op _;_ : Msg Msg -> Msg [gather frozen (e E)] .
op h : Msg -> Key [frozen] .
var Z : Msg .
var K : Key .
ops a b i : -> Name .
op 0 : -> Msg .
op n : Name Fresh -> Nonce .