|
1 (****************************************************************************** |
|
2 lemmas on guarded messages for public protocols |
|
3 |
|
4 date: march 2002 |
|
5 author: Frederic Blanqui |
|
6 email: blanqui@lri.fr |
|
7 webpage: http://www.lri.fr/~blanqui/ |
|
8 |
|
9 University of Cambridge, Computer Laboratory |
|
10 William Gates Building, JJ Thomson Avenue |
|
11 Cambridge CB3 0FD, United Kingdom |
|
12 ******************************************************************************) |
|
13 |
|
14 theory Guard_Public = Guard + Public + Extensions: |
|
15 |
|
16 subsection{*Extensions to Theory @{text Public}*} |
|
17 |
|
18 declare initState.simps [simp del] |
|
19 |
|
20 subsubsection{*signature*} |
|
21 |
|
22 constdefs sign :: "agent => msg => msg" |
|
23 "sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}" |
|
24 |
|
25 lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')" |
|
26 by (auto simp: sign_def) |
|
27 |
|
28 subsubsection{*agent associated to a key*} |
|
29 |
|
30 constdefs agt :: "key => agent" |
|
31 "agt K == @A. K = priK A | K = pubK A" |
|
32 |
|
33 lemma agt_priK [simp]: "agt (priK A) = A" |
|
34 by (simp add: agt_def) |
|
35 |
|
36 lemma agt_pubK [simp]: "agt (pubK A) = A" |
|
37 by (simp add: agt_def) |
|
38 |
|
39 subsubsection{*basic facts about @{term initState}*} |
|
40 |
|
41 lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)" |
|
42 by (cases A, auto simp: initState.simps) |
|
43 |
|
44 lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)" |
|
45 by auto |
|
46 |
|
47 lemma no_priK_in_analz_init [simp]: "A ~:bad |
|
48 ==> Key (priK A) ~:analz (initState Spy)" |
|
49 by (auto simp: initState.simps) |
|
50 |
|
51 lemma priK_notin_initState_Friend [simp]: "A ~= Friend C |
|
52 ==> Key (priK A) ~: parts (initState (Friend C))" |
|
53 by (auto simp: initState.simps) |
|
54 |
|
55 lemma keyset_init [iff]: "keyset (initState A)" |
|
56 by (cases A, auto simp: keyset_def initState.simps) |
|
57 |
|
58 subsubsection{*sets of private keys*} |
|
59 |
|
60 constdefs priK_set :: "key set => bool" |
|
61 "priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)" |
|
62 |
|
63 lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A" |
|
64 by (simp add: priK_set_def) |
|
65 |
|
66 lemma priK_set1 [iff]: "priK_set {priK A}" |
|
67 by (simp add: priK_set_def) |
|
68 |
|
69 lemma priK_set2 [iff]: "priK_set {priK A, priK B}" |
|
70 by (simp add: priK_set_def) |
|
71 |
|
72 subsubsection{*sets of good keys*} |
|
73 |
|
74 constdefs good :: "key set => bool" |
|
75 "good Ks == ALL K. K:Ks --> agt K ~:bad" |
|
76 |
|
77 lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad" |
|
78 by (simp add: good_def) |
|
79 |
|
80 lemma good1 [simp]: "A ~:bad ==> good {priK A}" |
|
81 by (simp add: good_def) |
|
82 |
|
83 lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {priK A, priK B}" |
|
84 by (simp add: good_def) |
|
85 |
|
86 subsubsection{*greatest nonce used in a trace, 0 if there is no nonce*} |
|
87 |
|
88 consts greatest :: "event list => nat" |
|
89 |
|
90 recdef greatest "measure size" |
|
91 "greatest [] = 0" |
|
92 "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)" |
|
93 |
|
94 lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs" |
|
95 apply (induct evs, auto simp: initState.simps) |
|
96 apply (drule used_sub_parts_used, safe) |
|
97 apply (drule greatest_msg_is_greatest, arith) |
|
98 by (simp, arith) |
|
99 |
|
100 subsubsection{*function giving a new nonce*} |
|
101 |
|
102 constdefs new :: "event list => nat" |
|
103 "new evs == Suc (greatest evs)" |
|
104 |
|
105 lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs" |
|
106 by (clarify, drule greatest_is_greatest, auto simp: new_def) |
|
107 |
|
108 subsection{*Proofs About Guarded Messages*} |
|
109 |
|
110 subsubsection{*small hack necessary because priK is defined as the inverse of pubK*} |
|
111 |
|
112 lemma pubK_is_invKey_priK: "pubK A = invKey (priK A)" |
|
113 by simp |
|
114 |
|
115 lemmas pubK_is_invKey_priK_substI = pubK_is_invKey_priK [THEN ssubst] |
|
116 |
|
117 lemmas invKey_invKey_substI = invKey [THEN ssubst] |
|
118 |
|
119 lemma "Nonce n:parts {X} ==> Crypt (pubK A) X:guard n {priK A}" |
|
120 apply (rule pubK_is_invKey_priK_substI, rule invKey_invKey_substI) |
|
121 by (rule Guard_Nonce, simp+) |
|
122 |
|
123 subsubsection{*guardedness results*} |
|
124 |
|
125 lemma sign_guard [intro]: "X:guard n Ks ==> sign A X:guard n Ks" |
|
126 by (auto simp: sign_def) |
|
127 |
|
128 lemma Guard_init [iff]: "Guard n Ks (initState B)" |
|
129 by (induct B, auto simp: Guard_def initState.simps) |
|
130 |
|
131 lemma Guard_knows_max': "Guard n Ks (knows_max' C evs) |
|
132 ==> Guard n Ks (knows_max C evs)" |
|
133 by (simp add: knows_max_def) |
|
134 |
|
135 lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs |
|
136 ==> Guard n Ks (spies evs)" |
|
137 by (auto simp: Guard_def dest: not_used_not_known parts_sub) |
|
138 |
|
139 lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs; |
|
140 Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)" |
|
141 by (auto simp: Guard_def dest: known_used parts_trans) |
|
142 |
|
143 lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs; |
|
144 Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)" |
|
145 by (auto simp: Guard_def dest: known_max_used parts_trans) |
|
146 |
|
147 lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs; |
|
148 Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)" |
|
149 apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono) |
|
150 by (auto simp: knows_max_def) |
|
151 |
|
152 subsubsection{*regular protocols*} |
|
153 |
|
154 constdefs regular :: "event list set => bool" |
|
155 "regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)" |
|
156 |
|
157 lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==> |
|
158 (Key (priK A):parts (spies evs)) = (A:bad)" |
|
159 by (auto simp: regular_def) |
|
160 |
|
161 lemma priK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==> |
|
162 (Key (priK A):analz (spies evs)) = (A:bad)" |
|
163 by auto |
|
164 |
|
165 lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p; |
|
166 priK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)" |
|
167 apply (clarify, simp only: knows_decomp) |
|
168 apply (drule Guard_invKey_keyset, simp+, safe) |
|
169 apply (drule in_good, simp) |
|
170 apply (drule in_priK_set, simp+, clarify) |
|
171 apply (frule_tac A=A in priK_analz_iff_bad) |
|
172 by (simp add: knows_decomp)+ |
|
173 |
|
174 end |