equal
deleted
inserted
replaced
80 inj_newK "inj(newK)" |
80 inj_newK "inj(newK)" |
81 fresh_newK "Key (newK evs) ~: parts (initState B)" |
81 fresh_newK "Key (newK evs) ~: parts (initState B)" |
82 isSym_newK "isSymKey (newK evs)" |
82 isSym_newK "isSymKey (newK evs)" |
83 |
83 |
84 |
84 |
85 (*NS3 DOESN'T ALLOW INTERLEAVING -- that is, it only responds to the |
|
86 MOST RECENT message.*) |
|
87 |
|
88 (*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*) |
85 (*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*) |
89 consts traces :: "event list set" |
86 consts traces :: "event list set" |
90 inductive traces |
87 inductive traces |
91 intrs |
88 intrs |
92 (*Initial trace is empty*) |
89 (*Initial trace is empty*) |
103 |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) |
100 |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) |
104 # evs : traces" |
101 # evs : traces" |
105 |
102 |
106 (*Server's response to Alice's message. |
103 (*Server's response to Alice's message. |
107 !! It may respond more than once to A's request !! |
104 !! It may respond more than once to A's request !! |
108 We can't trust the sender field, hence the A' in it.*) |
105 Server doesn't know who the true sender is, hence the A' in |
|
106 the sender field.*) |
109 NS2 "[| evs: traces; A ~= B; A ~= Server; |
107 NS2 "[| evs: traces; A ~= B; A ~= Server; |
110 (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs |
108 (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs |
111 |] ==> (Says Server A |
109 |] ==> (Says Server A |
112 (Crypt {|Nonce NA, Agent B, Key (newK evs), |
110 (Crypt {|Nonce NA, Agent B, Key (newK evs), |
113 (Crypt {|Key (newK evs), Agent A|} (serverKey B))|} |
111 (Crypt {|Key (newK evs), Agent A|} (serverKey B))|} |
121 : set_of_list evs; |
119 : set_of_list evs; |
122 A = Friend i; |
120 A = Friend i; |
123 (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs |
121 (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs |
124 |] ==> (Says A B X) # evs : traces" |
122 |] ==> (Says A B X) # evs : traces" |
125 |
123 |
|
124 (*Bob's nonce exchange. He does not know who the message came |
|
125 from, but responds to A because she is mentioned inside.*) |
126 NS4 "[| evs: traces; A ~= B; |
126 NS4 "[| evs: traces; A ~= B; |
127 (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) |
127 (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) |
128 : set_of_list evs |
128 : set_of_list evs |
129 |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces" |
129 |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces" |
|
130 |
|
131 (*Alice responds with (Suc N), if she has seen the key before.*) |
|
132 NS5 "[| evs: traces; A ~= B; |
|
133 (Says B' A (Crypt (Nonce N) K)) : set_of_list evs; |
|
134 (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) |
|
135 : set_of_list evs |
|
136 |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces" |
|
137 |
130 end |
138 end |