Commit 0bcfb8d4 authored by acholewa's avatar acholewa

Moved Amended-Needham Schroeder into done_examples (temporary measure until...

Moved Amended-Needham Schroeder into done_examples (temporary measure until all of the example theories have been properly converted into the latest Maude-PSL version). Also removed Amended-NS which was just a differently named file of the same protocol as Amended-Needham-Schroeder, and therefore not necessary.
parent 190208ef
spec Amended-NS is
Theory
types SName Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype SName < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
ops a b i : -> Name [ctor] .
op s : -> SName [ctor] .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op dec : Nonce -> 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 .
/*
A -> B : A
B -> A : E(Kbs:A,Nb0)
A -> S : A,B,Na,E(Kbs:A,Nb0)
S -> A : E(Kas:Na,B,Kab,E(Kbs:Kab,Nb0,A))
A -> B : E(Kbs:Kab,Nb0,A)
B -> A : E(Kab:Nb)
A -> B : E(Kab:Nb-1)
*/
Protocol
vars A B : Name .
var S : SName .
vars r r0 r1 : Fresh .
vars NA NB NB0 : Nonce .
var K : Key .
var X Y Z MB MB' : Msg .
var SK : Sessionkey .
Def(A) = na := n(A, r) , kas := mkey(A,s) .
In(A) = A, B, S .
Def(B) = nb0 := n(B, r0), nb := n(B, r1) , kbs := mkey(B,s) .
In(B) = A, B, S .
Def(S) = kas := mkey(A,S), kbs := mkey(B,S), kab := seskey(A,B,n(S,r)) .
In(S) = A, B, S .
1 . A -> B : A |- A .
2 . B -> A : e(kbs, A ; nb0 ) |- MB .
3 . A -> S : A ; B ; na ; MB
|- A ; B ; NA ; e(kbs, A ; NB0) .
4 . S -> A : e(kas , NA ; B ; kab ; e(kbs, kab ; NB0 ; A))
|- e(kas , na ; B ; SK ; MB') .
5 . A -> B : MB' |- e(kbs, SK ; nb0 ; A) .
6 . B -> A : e(SK, nb)
|- e(SK, NB) .
7 . A -> B : e(SK, dec(NB))
|- e(SK, dec(nb)) .
Out(A) = na, NB0 , NB, SK .
Out(B) = NA, nb0, nb, SK .
Out(S) = NA, NB0, kab .
Intruder
vars A B : Name .
var K : Key .
vars X Y : Msg .
var NA : Nonce .
var r : Fresh .
=> A, mkey(i, A), mkey(A, i), n(i, r) .
X ; Y <=> X , Y .
X, K => d(K, X), e(K, X) .
NA => dec(NA) .
Attacks
vars A B : Name .
var S : SName .
0 .
In(B) = A |-> a , B |-> b , S |-> s .
B executes protocol .
Out(B) = ditto .
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