Commit eba99104 authored by Andrew's avatar Andrew

Finished Denning-Sacco.

parent a2cc83e4
......@@ -15,35 +15,38 @@ 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 .
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 .
1 . A -> S : ANAME ; BNAME |- AS ; BS .
2 . S -> A : e(ksa, BS ; kab ; ts ; e(ksb, AS ; kab ; ts))
|- e(kas, B ; SKA ; TS ; M) .
|- 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) .
=> 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
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