Commit fdfa41b9 authored by Andrew's avatar Andrew

Did wmf.

parent 7282c235
...@@ -38,66 +38,70 @@ Theory ...@@ -38,66 +38,70 @@ Theory
// Concatenation // Concatenation
op _;_ : Msg Msg -> Msg [gather (e E)] . op _;_ : Msg Msg -> Msg [gather (e E)] .
eq d(K:Key, e(K:Key, Z:Msg )) = Z:Msg . var K : Key .
eq e(K:Key, d(K:Key, Z:Msg )) = Z:Msg . var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
Protocol Protocol
vars A B S : Name . vars ANAME BNAME SNAME : Name .
vars KAS KBS KAB : Key . vars KAS KBS KAB KBA : Key .
vars r1 r2 r3 : Fresh . vars r1 r2 r3 : Fresh .
vars TA TS : TimeStamp . vars MA MB : Msg .
Def(A) = KeyAS := mkey(A, S), KeyAB := seskey(A, B, n(A, r2)) . roles A B S .
Def(S) = KeyAS := mkey(A, S), KeyBS := mkey(B, S) .
Def(B) = KeyBS := mkey(B, S) .
In(A) = A, B, S . Def(A) = keyAS := mkey(ANAME, SNAME),
In(B) = A, B, S . keyAB := seskey(ANAME, BNAME, n(ANAME, r2)) .
In(S) = A, B, S . Def(B) = keyBS := mkey(BNAME, SNAME) .
Def(S) = keyAS := mkey(ANAME, SNAME),
keyBS := mkey(BNAME, SNAME) .
1 . A -> S : A ; e(KeyAS, B ; KeyAB) In(A) = ANAME, BNAME, SNAME, MA .
- A ; e(KeyAS, B ; KAB) . In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
2 . S -> B : e(KeyBS, A ; KAB) 1 . A -> S : ANAME ; e(keyAS, BNAME ; keyAB)
|- e(KeyBS, A ; KAB) . |- ANAME ; e(keyAS, BNAME ; KAB) .
3 . A -> B : A ; e(KeyAB, M) 2 . S -> B : e(keyBS, ANAME ; KAB)
|- A ; e(KAB, M) . |- e(keyBS, ANAME ; KBA) .
Out(A) = KeyAB . 3 . A -> B : ANAME ; e(keyAB, MA)
|- ANAME ; e(KBA, MB) .
Out(A) = keyAB .
Out(S) = KAB . Out(S) = KAB .
Out(B) = KAB . Out(B) = KBA .
Intruder Intruder
=> N:Name, t(i, r:Fresh), k(i, r:Fresh) . var r : Fresh .
X:Msg, Y:Msg <=> X:Msg ; Y:Msg . vars X Y : Msg .
K:Key, X:Msg => enc(K:Key, X:Msg), dec(K:Key, X:Msg) . var K : Key .
var N : Name .
var S : SName .
=> N, seskey(i, N, n(i, r)), mkey(i, S) .
X, Y <=> X ; Y .
K, X => e(K, X), d(K, X) .
Attacks Attacks
vars A B S : Name .
vars KAS KBS : Key .
//An empty attack for debugging purposes. //An empty attack for debugging purposes.
0 . 0 .
In(A) = A |-> a, B |-> b, S |-> s, KAS |-> KAS .
A executes protocol . A executes protocol .
Out(A) = ditto . Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
1 . 1 .
In(A) = A |-> a, B |-> b, S |-> s, KAS |-> KAS .
A executes protocol . A executes protocol .
Intruder learns KeyAB . Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
Out(A) = ditto . Intruder learns keyAB .
2 . 2 .
In(A) = A |-> a, B |-> b, S |-> s, KAS |-> KAS .
A executes protocol . A executes protocol .
Out(A) = ditto . Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
without: without:
In(B) = A |-> a, B |-> b, S |-> s, KBS |-> KBS .
B executes protocol . B executes protocol .
Out(B) = ditto . Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
ends 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