Commit cfa87aab authored by Andrew's avatar Andrew

Finished Kao-Chow

parent eba99104
......@@ -14,9 +14,11 @@ Theory
op e : Key Msg -> Msg .
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 .
/*
A -> S : A , B , na
......@@ -25,8 +27,8 @@ Theory
A -> B : E(kab:nb)
*/
Protocol
vars A B : UName .
var S : SName .
vars ANAME BNAME : UName .
var SNAME : SName .
vars MA M N : Msg .
vars r r1 r2 : Fresh .
var NAB : Nonce .
......@@ -34,24 +36,26 @@ Protocol
var NAS NBS : Nonce .
var NBA : Nonce .
Def(A) = na := n(A, r), kas := mkey(A, s) .
In(A) = A, B, S .
roles A B S .
Def(B) = nb := n(A, r1), kbs := mkey(B, s) .
In(B) = A, B, S .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
Def(S) = kas := mkey(A, s), kbs := mkey(B, s), kab := seskey(A,B,n(s,r2)) .
In(S) = A, B, S .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .
Def(B) = nb := n(ANAME, r1), kbs := mkey(BNAME, s) .
Def(S) = kas := mkey(ANAME, s), kbs := mkey(BNAME, s),
kab := seskey(ANAME,BNAME,n(s,r2)) .
1 . A -> S : A ; B ; na
|- A ; B ; NAS .
1 . A -> S : ANAME ; BNAME ; na
|- ANAME ; BNAME ; NAS .
2 . S -> B : e(kas, A ; B ; NAS ; kab) ; e(kbs, A ; B ; NAS ; kab)
|- MA ; e(kbs, A ; B ; NAB ; SKB) .
2 . S -> B : e(kas, ANAME ; BNAME ; NAS ; kab) ; e(kbs, ANAME ; BNAME ; NAS ; kab)
|- MA ; e(kbs, ANAME ; BNAME ; NAB ; SKB) .
3 . B -> A : MA ; e(SKB, NAB) ; nb
|- e(kas, A ; B ; na ; SKA) ; e(SKA, na) ; NBA .
3 . B -> A : MA ; e(SKB, NAB) ; nb
|- e(kas, ANAME ; BNAME ; na ; SKA) ; e(SKA, na) ; NBA .
4 . A -> B : e(SKA, NBA)
|- e(SKB, nb) .
......@@ -67,35 +71,25 @@ Intruder
var K : Key .
vars M N : Msg .
=> D, n(i, r), mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
=> D, n(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 .
var NBA : Nonce .
var r : Fresh .
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 .
without:
In(A) = A |-> a, B |-> b, S |-> s .
A executes protocol .
Out(A) = NBA |-> n(b, r), ditto .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
without:
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
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