Commit 13c634dc authored by acholewa's avatar acholewa

Adjusted the ISO5 specification to line up with the current version of Maude-PSL.

parent 1852506c
......@@ -14,10 +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 .
/* I think there is a typo in the Maude-NPA example */
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
/*
......@@ -29,35 +29,38 @@ Theory
*/
Protocol
vars A B AB AS BS : UName .
var S : SName .
vars ANAME BNAME AB AS BS : UName .
var SNAME : SName .
vars K : Key .
vars SKA SKB : Sessionkey .
vars r r' : Fresh .
vars NAB NAS NBA NBS : Nonce .
var MA : Msg .
Def(A) = na := n(A, r), kas := mkey(A,S) .
In(A) = A, B, S .
roles A B S .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME, SNAME) .
Def(B) = nb := n(B, r), nb1 := n(B, r'), kbs := mkey(B,S) .
In(B) = B, S .
In(A) = ANAME, BNAME, SNAME .
Def(S) = ksa := mkey(AS,S), ksb := mkey(BS,S) ,
Def(B) = nb := n(BNAME, r), nb1 := n(BNAME, r'), kbs := mkey(BNAME,SNAME) .
In(B) = BNAME, SNAME .
Def(S) = ksa := mkey(AS,SNAME), ksb := mkey(BS,SNAME),
kab := seskey(AS, BS, n(s,r)) .
In(S) = S .
In(S) = SNAME .
1 . A -> B : A ; na
|- AB ; NAB .
1 . A -> B : ANAME ; na
|- AB ; NAB .
2 . B -> S : AB ; NAB ; B ; nb1
|- AS ; NAS ; BS ; NBS .
2 . B -> S : AB ; NAB ; BNAME ; nb1
|- AS ; NAS ; BS ; NBS .
3 . S -> B : e(ksb, NBS ; kab ; A) ; e(ksa, NAS ; kab ; BS)
|- e(kbs, nb1 ; SKB ; AB) ; MA .
3 . S -> B : e(ksb, NBS ; kab ; AS) ; e(ksa, NAS ; kab ; BS)
|- e(kbs, nb1 ; SKB ; AB) ; MA .
4 . B -> A : MA ; e(SKB, nb ; NAB)
|- e(kas, na ; SKA ; B ) ; e(SKA, NBA ; na) .
4 . B -> A : MA ; e(SKB, nb ; NAB)
|- e(kas, na ; SKA ; BNAME ) ; e(SKA, NBA ; na) .
5 . A -> B : e(SKA, na ; NBA)
|- e(SKB, NAB ; nb) .
......@@ -77,26 +80,20 @@ Intruder
M, N <=> M ; N .
Attacks
vars A B : UName .
var S : SName .
var SK : Sessionkey .
var NBA : Nonce .
var r : Fresh .
0 .
B executes protocol .
Subst(B) = AB |-> a , B |-> b, S |-> s .
Subst(B) = AB |-> a , BNAME |-> b, SNAME |-> s .
1 .
B executes protocol .
Subst(B) = AB |-> a , B |-> b , S |-> s .
Subst(B) = AB |-> a , BNAME |-> b , SNAME |-> s .
Intruder learns SKB .
2 .
B executes protocol .
Subst(B) = AB |-> a , B |-> b , S |-> s .
Subst(B) = AB |-> a , BNAME |-> b , SNAME |-> s .
without:
A executes protocol .
Subst(A) = A |-> a, B |-> b , S |-> s, NBA |-> n(b, r) .
Subst(A) = ANAME |-> a, BNAME |-> b , SNAME |-> s, NBA |-> n(b, r) .
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