Commit 47c9a669 authored by Andrew's avatar Andrew

Now that I've finished updating all the PSL files, I've moved all the PSL...

Now that I've finished updating all the PSL files, I've moved all the PSL files back into the normal examples folder.
parent 14f94e10
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
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 |
-(K:Key),
-(M:Msg),
+(e(K:Key, M:Msg)), nil] &
:: nil ::
[ nil |
-(K:Key),
-(M:Msg),
+(d(K:Key, M:Msg)), nil] &
:: nil ::
[ nil |
-(dec(N:Nonce)),
+(N:Nonce), nil] &
:: nil ::
[ nil |
-(M:Msg ; M1:Msg),
+(M:Msg), nil] &
:: nil ::
[ nil |
-(M:Msg ; M1:Msg),
+(M1:Msg), nil] &
:: r:Fresh ::
[ nil |
+(n(i, r:Fresh)), nil] [nonexec].
eq STRANDS-PROTOCOL =
:: r:Fresh ::
[ nil |
+(ANAME:Name),
-(M1:Msg),
+(ANAME:Name ; BNAME:Name ; n(ANAME:Name, r:Fresh) ; M1:Msg),
-(e(mkey(ANAME:Name, SNAME:Name), n(ANAME:Name, r:Fresh) ; BNAME:Name ; KA:Key ; M2:Msg)),
+(M2:Msg),
-(e(KA:Key, NB:Nonce)),
+(e(KA:Key, dec(NB:Nonce))), nil] &
:: r1:Fresh ::
[ nil |
-(A2NAME:Name ; B2NAME:Name ; NA2:Nonce ; e(mkey(B2NAME:Name, SNAME:Name), A2NAME:Name ; NB2:Nonce)),
+(e(mkey(A2NAME:Name, SNAME:Name), NA2:Nonce ; B2NAME:Name ; seskey(A2NAME:Name, B2NAME:Name, n(SNAME:Name, r1:Fresh)) ; e(mkey(B2NAME:Name, SNAME:Name), seskey(A2NAME:Name, B2NAME:Name, n(SNAME:Name, r1:Fresh)) ; NB2:Nonce ; A2NAME:Name))), nil] &
:: r2:Fresh,r0:Fresh ::
[ nil |
-(A1NAME:Name),
+(e(mkey(BNAME:Name, SNAME:Name), A1NAME:Name ; n(BNAME:Name, r0:Fresh))),
-(e(mkey(BNAME:Name, SNAME:Name), KB:Key ; n(BNAME:Name, r0:Fresh) ; A1NAME:Name)),
+(e(KB:Key, n(BNAME:Name, r2:Fresh))),
-(e(KB:Key, dec(n(BNAME:Name, r2:Fresh)))), nil] [nonexec].
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)=
:: r2:Fresh,r0:Fresh ::
[ nil,
-(a),
+(e(mkey(b, s), a ; n(b, r0:Fresh))),
-(e(mkey(b, s), KB:Key ; n(b, r0:Fresh) ; a)),
+(e(KB:Key, n(b, r2:Fresh))),
-(e(KB:Key, dec(n(b, r2:Fresh)))) | nil]
|| empty
||
nil
||
nil
||
nil[nonexec].
endfm
select MAUDE-NPA .
\ No newline at end of file
date
#!/bin/bash
./maude27 -no-prelude prelude.maude <<EOF
load maude-npa.maude
load examples/Otway-Rees.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red initials(4) .
EOF
date
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES .
sorts UName SName Name Key Nonce Masterkey Sessionkey .
subsorts Masterkey Sessionkey < Key .
subsorts SName UName < Name < Public .
op n : Name Fresh -> Nonce [ frozen ] .
ops a b i : -> UName .
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 _;_ : Msg Msg -> Msg [ gather ( e E ) frozen ] .
subsorts UName 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 |
+(P:UName), nil] &
:: nil ::
[ nil |
+(mkey(i, s)), nil] &
:: nil ::
[ nil |
-(M:Msg),
-(N:Msg),
+(M:Msg ; N:Msg), nil] &
:: nil ::
[ nil |
-(P:UName),
+(mkey(i, P:UName)), nil] &
:: nil ::
[ nil |
-(P:UName),
+(mkey(P:UName, i)), nil] &
:: nil ::
[ nil |
-(K:Key),
-(M:Msg),
+(e(K:Key, M:Msg)), nil] &
:: nil ::
[ nil |
-(K:Key),
-(M:Msg),
+(d(K:Key, M:Msg)), nil] &
:: nil ::
[ nil |
-(M:Msg ; N:Msg),
+(N:Msg), nil] &
:: nil ::
[ nil |
-(M:Msg ; N:Msg),
+(M:Msg), nil] [nonexec].
eq STRANDS-PROTOCOL =
:: r':Fresh ::
[ nil |
-(CB:Nonce ; ANAME:UName ; BNAME:UName ; M1:Msg),
+(CB:Nonce ; ANAME:UName ; BNAME:UName ; M1:Msg ; e(mkey(BNAME:UName, SNAME:SName), n(BNAME:UName, r':Fresh) ; CB:Nonce ; ANAME:UName ; BNAME:UName)),
-(CB:Nonce ; MA:Msg ; e(mkey(BNAME:UName, SNAME:SName), n(BNAME:UName, r':Fresh) ; KCB:Sessionkey)),
+(CB:Nonce ; MA:Msg), nil] &
:: r'':Fresh ::
[ nil |
-(CS:Nonce ; ANAME:UName ; BNAME:UName ; e(mkey(ANAME:UName, SNAME:SName), RA:Nonce ; CS:Nonce ; ANAME:UName ; BNAME:UName) ; e(mkey(BNAME:UName, SNAME:SName), RB:Nonce ; CS:Nonce ; ANAME:UName ; BNAME:UName)),
+(CS:Nonce ; e(mkey(ANAME:UName, SNAME:SName), RA:Nonce ; seskey(ANAME:UName, BNAME:UName, n(SNAME:SName, r'':Fresh))) ; e(mkey(BNAME:UName, SNAME:SName), RB:Nonce ; seskey(ANAME:UName, BNAME:UName, n(SNAME:SName, r'':Fresh)))), nil] &
:: r:Fresh,rM:Fresh ::
[ nil |
+(n(ANAME:UName, rM:Fresh) ; ANAME:UName ; BNAME:UName ; e(mkey(ANAME:UName, SNAME:SName), n(ANAME:UName, r:Fresh) ; n(ANAME:UName, rM:Fresh) ; ANAME:UName ; BNAME:UName)),
-(n(ANAME:UName, rM:Fresh) ; e(mkey(ANAME:UName, SNAME:SName), n(ANAME:UName, r:Fresh) ; KCA:Sessionkey)), nil] [nonexec].
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)=
:: r:Fresh,rM:Fresh ::
[ nil,
+(n(a, rM:Fresh) ; a ; b ; e(mkey(a, s), n(a, r:Fresh) ; n(a, rM:Fresh) ; a ; b)),
-(n(a, rM:Fresh) ; e(mkey(a, s), n(a, r:Fresh) ; KCA:Sessionkey)) | nil]
|| empty
||
nil
||
nil
||
nil[nonexec].
eq ATTACK-STATE(1)=
:: r:Fresh,rM:Fresh ::
[ nil,
+(n(a, rM:Fresh) ; a ; b ; e(mkey(a, s), n(a, r:Fresh) ; n(a, rM:Fresh) ; a ; b)),
-(n(a, rM:Fresh) ; e(mkey(a, s), n(a, r:Fresh) ; KCA:Sessionkey)) | nil]
||
KCA:Sessionkey inI
||
nil
||
nil
||
nil[nonexec].
eq ATTACK-STATE(2)=
:: r:Fresh,rM:Fresh ::
[ nil,
+(n(a, rM:Fresh) ; a ; b ; e(mkey(a, s), n(a, r:Fresh) ; n(a, rM:Fresh) ; a ; b)),
-(n(a, rM:Fresh) ; e(mkey(a, s), n(a, r:Fresh) ; KCA:Sessionkey)) | nil]
|| empty
||
nil
||
nil
|| never((S &
:: r':Fresh ::
[ nil,
-(CB:Nonce ; a ; b ; e(mkey(a, s), n(a, rM:Fresh) ; n(a, r:Fresh) ; a ; b)),
+(CB:Nonce ; a ; b ; e(mkey(a, s), n(a, rM:Fresh) ; n(a, r:Fresh) ; a ; b) ; e(mkey(b, s), n(b, r':Fresh) ; CB:Nonce ; a ; b)),
-(CB:Nonce ; MA:Msg ; e(mkey(b, s), n(b, r':Fresh) ; KCB:Sessionkey)),
+(CB:Nonce ; MA:Msg) | nil] ) || K)[nonexec].
endfm
select MAUDE-NPA .
\ No newline at end of file
date
#!/bin/bash
./maude27 -no-prelude prelude.maude <<EOF
load maude-npa.maude
load examples/nspk.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red summary(10) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
red run(10) .
EOF
date
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES .
sorts Name Nonce Enc .
subsorts Name < Public .
op pk : Name Msg -> Enc [ frozen ] .
op sk : Name Msg -> Enc [ frozen ] .
op n : Name Fresh -> Nonce [ frozen ] .
op _;_ : Msg Msg -> Msg [ ctor gather ( e E ) frozen ] .
ops a b i : -> Name [ ctor ] .
subsorts Name Nonce Enc < Msg .
op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen].
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
eq sk(X:Name, pk(X:Name, Z:Msg)) = Z:Msg [ variant ] .
eq pk(X:Name, sk(X:Name, 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 |
-(X:Msg),
+(sk(i, X:Msg)), nil] &
:: nil ::
[ nil |
-(Y:Msg),
-(X:Msg),
+(X:Msg ; Y:Msg), nil] &
:: nil ::
[ nil |
-(A:Name),
-(X:Msg),
+(pk(A:Name, X:Msg)), nil] &
:: nil ::
[ nil |
-(X:Msg ; Y:Msg),
+(X:Msg), nil] &
:: nil ::
[ nil |
-(X:Msg ; Y:Msg),
+(Y:Msg), nil] &
:: r1:Fresh ::
[ nil |
+(n(i, r1:Fresh)), nil] [nonexec].
eq STRANDS-PROTOCOL =
:: r1:Fresh ::
[ nil |
+(pk(BName:Name, AName:Name ; n(AName:Name, r1:Fresh))),
-(pk(AName:Name, n(AName:Name, r1:Fresh) ; N2:Nonce)),
+(pk(BName:Name, N2:Nonce)), nil] &
:: r2:Fresh ::
[ nil |
-(pk(BName:Name, AName:Name ; N1:Nonce)),
+(pk(AName:Name, N1:Nonce ; n(BName:Name, r2:Fresh))),
-(pk(BName:Name, n(BName:Name, r2:Fresh))), nil] [nonexec].
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)=
:: r2:Fresh ::
[ nil,
-(pk(b, a ; N1:Nonce)),
+(pk(a, N1:Nonce ; n(b, r2:Fresh))),
-(pk(b, n(b, r2:Fresh))) | nil]
||
n(b, r2:Fresh) inI
||
nil
||
nil
||
nil[nonexec].
eq ATTACK-STATE(1)=
:: r2:Fresh ::
[ nil,
-(pk(b, a ; N1:Nonce)),
+(pk(a, N1:Nonce ; n(b, r2:Fresh))),
-(pk(b, n(b, r2:Fresh))) | nil]
||
n(b, r2:Fresh) inI
||
nil
||
nil
|| never((S &
:: r1:Fresh ::
[ nil,
+(pk(b, a ; n(a, r1:Fresh))),
-(pk(a, n(a, r1:Fresh) ; N2:Nonce)),
+(pk(b, N2:Nonce)) | nil] ) || K)[nonexec].
endfm
select MAUDE-NPA .
\ No newline at end of file
mod nspk is
protecting TRANSLATION-TO-MAUDE-NPA .
protecting PROTOCOL-EXAMPLE-SYMBOLS .
op pk : Msg Msg -> Enc [frozen] .
op sk : Msg Msg -> Enc [frozen] .
op n : Msg Msg -> Nonce [frozen] .
op _;_ : Msg Msg -> Msg [ctor gather ( e E ) frozen ] .
op a : -> Name [ctor] .
op b : -> Name [ctor] .
op c : -> Name [ctor] .
op i : -> Name [ctor] .
op na : -> Msg .
op nb : -> Msg .
endm
rew
(
Specification {
Protocol
{
In ( A:Name ) = A:Name , B:Name .[53]
In ( B:Name ) = A:Name , B:Name .[67]
1 . A:Name -> B:Name : pk ( B:Name , A:Name ; na ) |- pk ( B:Name , A:Name ; N1:Nonce ) .[70]
2 . B:Name -> A:Name : pk ( A:Name , N1:Nonce ; nb ) |- pk ( A:Name , na ; N2:Nonce ) .[71]
3 . A:Name -> B:Name : pk ( B:Name , N2:Nonce ) |- pk ( B:Name , nb ) .[72]
Out ( A:Name ) = na , N2:Nonce .[74]
Out ( B:Name ) = nb , N1:Nonce .[75]
}
Intruder
{
=> n ( i , r1:Fresh ) .[93]
X:Msg ; Y:Msg <=> X:Msg , Y:Msg .[94]
X:Msg => sk ( i , X:Msg ) .[95]
X:Msg , A:Name => pk ( A:Name , X:Msg ) .[96]
}
Attacks
{
{ In ( B:Name ) = A:Name |-> a , B:Name |-> b .[112]
B:Name executes protocol .[116]
Intruder learns nb .[120]
Out ( B:Name ) = ditto .[139]
{ In ( B:Name ) = A:Name |-> a , B:Name |-> b .[141]
B:Name executes protocol .[142]
Intruder learns nb .[143]
Out ( B:Name ) = ditto .[144]
without: In ( A:Name ) = A:Name |-> a , B:Name |-> b .[157]
A:Name executes protocol .[159]
Out ( A:Name ) = ditto .[160]
}
}
[na := n ( A:Name , r1:Fresh ), nb := n ( B:Name , r2:Fresh ), $noDefs]
[(mt).StrandData]
[(empty).StrandSet]
{##K##:IntruderKnowledge}
{##S##:StrandSet}) .
q
\ No newline at end of file
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