1.1 --- a/src/HOL/Auth/Event.thy Thu Jul 11 15:28:10 1996 +0200
1.2 +++ b/src/HOL/Auth/Event.thy Thu Jul 11 15:30:22 1996 +0200
1.3 @@ -6,6 +6,8 @@
1.4 Datatype of events;
1.5 inductive relation "traces" for Needham-Schroeder (shared keys)
1.6
1.7 +INTERLEAVING? See defn of "traces"
1.8 +
1.9 WHAT ABOUT ASYMMETRIC KEYS? NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
1.10 PUBLIC KEY...
1.11 *)
1.12 @@ -14,16 +16,16 @@
1.13
1.14 consts
1.15 publicKey :: agent => key
1.16 - serverKey :: agent => key (*symmetric keys*)
1.17 + serverKey :: agent => key (*symmetric keys*)
1.18
1.19 rules
1.20 isSym_serverKey "isSymKey (serverKey A)"
1.21
1.22 -consts (*Initial states of agents -- parameter of the construction*)
1.23 +consts (*Initial states of agents -- parameter of the construction*)
1.24 initState :: agent => msg set
1.25
1.26 primrec initState agent
1.27 - (*Server knows all keys; other agents know only their own*)
1.28 + (*Server knows all keys; other agents know only their own*)
1.29 initState_Server "initState Server = range (Key o serverKey)"
1.30 initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}"
1.31 initState_Enemy "initState Enemy = {Key (serverKey Enemy)}"
1.32 @@ -51,7 +53,7 @@
1.33 sees :: [agent, event list] => msg set
1.34
1.35 primrec sees list
1.36 - (*Initial knowledge includes all public keys and own private key*)
1.37 + (*Initial knowledge includes all public keys and own private key*)
1.38 sees_Nil "sees A [] = initState A"
1.39 sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
1.40
1.41 @@ -61,25 +63,29 @@
1.42 "knownBy evs X == {A. X: analyze (sees A evs)}"
1.43
1.44
1.45 -(*Agents generate "random" nonces. Different agents always generate
1.46 - different nonces. Different traces also yield different nonces. Same
1.47 - applies for keys.*)
1.48 -(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS. REMOVE AGENT ARGUMENT?
1.49 +(*Agents generate "random" nonces. Different traces always yield
1.50 + different nonces. Same applies for keys.*)
1.51 +(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
1.52 NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
1.53 consts
1.54 - newN :: "agent * event list => nat"
1.55 - newK :: "agent * event list => key"
1.56 + newN :: "event list => nat"
1.57 + newK :: "event list => key"
1.58
1.59 rules
1.60 inj_serverKey "inj serverKey"
1.61
1.62 inj_newN "inj(newN)"
1.63 - fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)"
1.64 + fresh_newN "Nonce (newN evs) ~: parts (initState B)"
1.65
1.66 inj_newK "inj(newK)"
1.67 - fresh_newK "Key (newK(A,evs)) ~: parts (initState B)"
1.68 - isSym_newK "isSymKey (newK(A,evs))"
1.69 + fresh_newK "Key (newK evs) ~: parts (initState B)"
1.70 + isSym_newK "isSymKey (newK evs)"
1.71 +
1.72
1.73 +(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
1.74 + MOST RECENT message. Does this mean we can't model middleperson attacks?
1.75 + We don't need the most recent restriction in order to handle interception
1.76 + by the Enemy, as agents are not forced to respond anyway.*)
1.77
1.78 consts traces :: "event list set"
1.79 inductive traces
1.80 @@ -88,17 +94,39 @@
1.81
1.82 (*The enemy MAY say anything he CAN say. We do not expect him to
1.83 invent new nonces here, but he can also use NS1.*)
1.84 - Fake "[| evs: traces; X: synthesize(analyze(sees Enemy evs))
1.85 + Fake "[| evs: traces; B ~= Enemy;
1.86 + X: synthesize(analyze(sees Enemy evs))
1.87 |] ==> (Says Enemy B X) # evs : traces"
1.88
1.89 NS1 "[| evs: traces; A ~= Server
1.90 - |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|})
1.91 + |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|})
1.92 # evs : traces"
1.93
1.94 - NS2 "[| evs: traces;
1.95 + (*We can't trust the sender field: change that A to A'? *)
1.96 + NS2 "[| evs: traces; A ~= B;
1.97 evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
1.98 |] ==> (Says Server A
1.99 - (Crypt {|Agent A, Agent B,
1.100 - Key (newK(Server,evs)), Nonce NA|}
1.101 - (serverKey A))) # evs : traces"
1.102 + (Crypt {|Nonce NA, Agent B, Key (newK evs),
1.103 + (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
1.104 + (serverKey A))) # evs : traces"
1.105 +
1.106 + (*We can't assume S=Server. Agent A "remembers" her nonce.
1.107 + May assume WLOG that she is NOT the Enemy, as the Fake rule.
1.108 + covers this case. Can inductively show A ~= Server*)
1.109 + NS3 "[| evs: traces; A ~= B;
1.110 + evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
1.111 + (serverKey A)))
1.112 + # evs';
1.113 + A = Friend i;
1.114 + (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
1.115 + |] ==> (Says A B X) # evs : traces"
1.116 +
1.117 +(*Initial version of NS2 had
1.118 +
1.119 + {|Agent A, Agent B, Key (newK evs), Nonce NA|}
1.120 +
1.121 + for the encrypted part; the version above is LESS transparent, hence
1.122 + maybe HARDER to prove. Also it is precisely as in the BAN paper.
1.123 +*)
1.124 +
1.125 end