69 Unique :: "[event, event list] => bool" ("Unique _ on _") |
69 Unique :: "[event, event list] => bool" ("Unique _ on _") |
70 "Unique ev on evs == |
70 "Unique ev on evs == |
71 ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))" |
71 ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))" |
72 |
72 |
73 |
73 |
74 consts bankerberos :: "event list set" |
74 inductive_set bankerberos :: "event list set" |
75 inductive "bankerberos" |
75 where |
76 intros |
|
77 |
76 |
78 Nil: "[] \<in> bankerberos" |
77 Nil: "[] \<in> bankerberos" |
79 |
78 |
80 Fake: "\<lbrakk> evsf \<in> bankerberos; X \<in> synth (analz (spies evsf)) \<rbrakk> |
79 | Fake: "\<lbrakk> evsf \<in> bankerberos; X \<in> synth (analz (spies evsf)) \<rbrakk> |
81 \<Longrightarrow> Says Spy B X # evsf \<in> bankerberos" |
80 \<Longrightarrow> Says Spy B X # evsf \<in> bankerberos" |
82 |
81 |
83 |
82 |
84 BK1: "\<lbrakk> evs1 \<in> bankerberos \<rbrakk> |
83 | BK1: "\<lbrakk> evs1 \<in> bankerberos \<rbrakk> |
85 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1 |
84 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1 |
86 \<in> bankerberos" |
85 \<in> bankerberos" |
87 |
86 |
88 |
87 |
89 BK2: "\<lbrakk> evs2 \<in> bankerberos; Key K \<notin> used evs2; K \<in> symKeys; |
88 | BK2: "\<lbrakk> evs2 \<in> bankerberos; Key K \<notin> used evs2; K \<in> symKeys; |
90 Says A' Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
89 Says A' Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
91 \<Longrightarrow> Says Server A |
90 \<Longrightarrow> Says Server A |
92 (Crypt (shrK A) |
91 (Crypt (shrK A) |
93 \<lbrace>Number (CT evs2), Agent B, Key K, |
92 \<lbrace>Number (CT evs2), Agent B, Key K, |
94 (Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>) |
93 (Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>) |
95 # evs2 \<in> bankerberos" |
94 # evs2 \<in> bankerberos" |
96 |
95 |
97 |
96 |
98 BK3: "\<lbrakk> evs3 \<in> bankerberos; |
97 | BK3: "\<lbrakk> evs3 \<in> bankerberos; |
99 Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
98 Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
100 \<in> set evs3; |
99 \<in> set evs3; |
101 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
100 Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
102 \<not> expiredK Tk evs3 \<rbrakk> |
101 \<not> expiredK Tk evs3 \<rbrakk> |
103 \<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace> |
102 \<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace> |
104 # evs3 \<in> bankerberos" |
103 # evs3 \<in> bankerberos" |
105 |
104 |
106 |
105 |
107 BK4: "\<lbrakk> evs4 \<in> bankerberos; |
106 | BK4: "\<lbrakk> evs4 \<in> bankerberos; |
108 Says A' B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>), |
107 Says A' B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>), |
109 (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4; |
108 (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4; |
110 \<not> expiredK Tk evs4; \<not> expiredA Ta evs4 \<rbrakk> |
109 \<not> expiredK Tk evs4; \<not> expiredA Ta evs4 \<rbrakk> |
111 \<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4 |
110 \<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4 |
112 \<in> bankerberos" |
111 \<in> bankerberos" |
113 |
112 |
114 (*Old session keys may become compromised*) |
113 (*Old session keys may become compromised*) |
115 Oops: "\<lbrakk> evso \<in> bankerberos; |
114 | Oops: "\<lbrakk> evso \<in> bankerberos; |
116 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
115 Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
117 \<in> set evso; |
116 \<in> set evso; |
118 expiredK Tk evso \<rbrakk> |
117 expiredK Tk evso \<rbrakk> |
119 \<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerberos" |
118 \<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerberos" |
120 |
119 |