equal
deleted
inserted
replaced
|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Public}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 The function |
|
20 \isa{pubK} maps agents to their public keys. The function |
|
21 \isa{priK} maps agents to their private keys. It is defined in terms of |
|
22 \isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is |
|
23 not a proper constant, so we declare it using \isacommand{syntax} |
|
24 (cf.\ \S\ref{sec:syntax-translations}).% |
|
25 \end{isamarkuptext}% |
|
26 \isamarkuptrue% |
|
27 \isacommand{consts}\isamarkupfalse% |
|
28 \ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline |
|
29 \isacommand{syntax}\isamarkupfalse% |
|
30 \ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline |
|
31 \isacommand{translations}\isamarkupfalse% |
|
32 \ {\isachardoublequoteopen}priK\ x{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}% |
|
33 \begin{isamarkuptext}% |
|
34 \noindent |
|
35 The set \isa{bad} consists of those agents whose private keys are known to |
|
36 the spy. |
|
37 |
|
38 Two axioms are asserted about the public-key cryptosystem. |
|
39 No two agents have the same public key, and no private key equals |
|
40 any public key.% |
|
41 \end{isamarkuptext}% |
|
42 \isamarkuptrue% |
|
43 \isacommand{axioms}\isamarkupfalse% |
|
44 \isanewline |
|
45 \ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline |
|
46 \ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isachartilde}{\isacharequal}\ pubK\ B{\isachardoublequoteclose}% |
|
47 \isadelimproof |
|
48 % |
|
49 \endisadelimproof |
|
50 % |
|
51 \isatagproof |
|
52 % |
|
53 \endisatagproof |
|
54 {\isafoldproof}% |
|
55 % |
|
56 \isadelimproof |
|
57 % |
|
58 \endisadelimproof |
|
59 % |
|
60 \isadelimproof |
|
61 % |
|
62 \endisadelimproof |
|
63 % |
|
64 \isatagproof |
|
65 % |
|
66 \endisatagproof |
|
67 {\isafoldproof}% |
|
68 % |
|
69 \isadelimproof |
|
70 % |
|
71 \endisadelimproof |
|
72 % |
|
73 \isadelimproof |
|
74 % |
|
75 \endisadelimproof |
|
76 % |
|
77 \isatagproof |
|
78 % |
|
79 \endisatagproof |
|
80 {\isafoldproof}% |
|
81 % |
|
82 \isadelimproof |
|
83 % |
|
84 \endisadelimproof |
|
85 % |
|
86 \isadelimproof |
|
87 % |
|
88 \endisadelimproof |
|
89 % |
|
90 \isatagproof |
|
91 % |
|
92 \endisatagproof |
|
93 {\isafoldproof}% |
|
94 % |
|
95 \isadelimproof |
|
96 % |
|
97 \endisadelimproof |
|
98 % |
|
99 \isadelimproof |
|
100 % |
|
101 \endisadelimproof |
|
102 % |
|
103 \isatagproof |
|
104 % |
|
105 \endisatagproof |
|
106 {\isafoldproof}% |
|
107 % |
|
108 \isadelimproof |
|
109 % |
|
110 \endisadelimproof |
|
111 % |
|
112 \isadelimproof |
|
113 % |
|
114 \endisadelimproof |
|
115 % |
|
116 \isatagproof |
|
117 % |
|
118 \endisatagproof |
|
119 {\isafoldproof}% |
|
120 % |
|
121 \isadelimproof |
|
122 % |
|
123 \endisadelimproof |
|
124 % |
|
125 \isadelimproof |
|
126 % |
|
127 \endisadelimproof |
|
128 % |
|
129 \isatagproof |
|
130 % |
|
131 \endisatagproof |
|
132 {\isafoldproof}% |
|
133 % |
|
134 \isadelimproof |
|
135 % |
|
136 \endisadelimproof |
|
137 % |
|
138 \isadelimproof |
|
139 % |
|
140 \endisadelimproof |
|
141 % |
|
142 \isatagproof |
|
143 % |
|
144 \endisatagproof |
|
145 {\isafoldproof}% |
|
146 % |
|
147 \isadelimproof |
|
148 % |
|
149 \endisadelimproof |
|
150 % |
|
151 \isadelimproof |
|
152 % |
|
153 \endisadelimproof |
|
154 % |
|
155 \isatagproof |
|
156 % |
|
157 \endisatagproof |
|
158 {\isafoldproof}% |
|
159 % |
|
160 \isadelimproof |
|
161 % |
|
162 \endisadelimproof |
|
163 % |
|
164 \isadelimproof |
|
165 % |
|
166 \endisadelimproof |
|
167 % |
|
168 \isatagproof |
|
169 % |
|
170 \endisatagproof |
|
171 {\isafoldproof}% |
|
172 % |
|
173 \isadelimproof |
|
174 % |
|
175 \endisadelimproof |
|
176 % |
|
177 \isadelimproof |
|
178 % |
|
179 \endisadelimproof |
|
180 % |
|
181 \isatagproof |
|
182 % |
|
183 \endisatagproof |
|
184 {\isafoldproof}% |
|
185 % |
|
186 \isadelimproof |
|
187 % |
|
188 \endisadelimproof |
|
189 % |
|
190 \isadelimproof |
|
191 % |
|
192 \endisadelimproof |
|
193 % |
|
194 \isatagproof |
|
195 % |
|
196 \endisatagproof |
|
197 {\isafoldproof}% |
|
198 % |
|
199 \isadelimproof |
|
200 % |
|
201 \endisadelimproof |
|
202 % |
|
203 \isadelimproof |
|
204 % |
|
205 \endisadelimproof |
|
206 % |
|
207 \isatagproof |
|
208 % |
|
209 \endisatagproof |
|
210 {\isafoldproof}% |
|
211 % |
|
212 \isadelimproof |
|
213 % |
|
214 \endisadelimproof |
|
215 % |
|
216 \isadelimproof |
|
217 % |
|
218 \endisadelimproof |
|
219 % |
|
220 \isatagproof |
|
221 % |
|
222 \endisatagproof |
|
223 {\isafoldproof}% |
|
224 % |
|
225 \isadelimproof |
|
226 % |
|
227 \endisadelimproof |
|
228 % |
|
229 \isadelimproof |
|
230 % |
|
231 \endisadelimproof |
|
232 % |
|
233 \isatagproof |
|
234 % |
|
235 \endisatagproof |
|
236 {\isafoldproof}% |
|
237 % |
|
238 \isadelimproof |
|
239 % |
|
240 \endisadelimproof |
|
241 % |
|
242 \isadelimproof |
|
243 % |
|
244 \endisadelimproof |
|
245 % |
|
246 \isatagproof |
|
247 % |
|
248 \endisatagproof |
|
249 {\isafoldproof}% |
|
250 % |
|
251 \isadelimproof |
|
252 % |
|
253 \endisadelimproof |
|
254 % |
|
255 \isadelimproof |
|
256 % |
|
257 \endisadelimproof |
|
258 % |
|
259 \isatagproof |
|
260 % |
|
261 \endisatagproof |
|
262 {\isafoldproof}% |
|
263 % |
|
264 \isadelimproof |
|
265 % |
|
266 \endisadelimproof |
|
267 % |
|
268 \isadelimproof |
|
269 % |
|
270 \endisadelimproof |
|
271 % |
|
272 \isatagproof |
|
273 % |
|
274 \endisatagproof |
|
275 {\isafoldproof}% |
|
276 % |
|
277 \isadelimproof |
|
278 % |
|
279 \endisadelimproof |
|
280 % |
|
281 \isadelimproof |
|
282 % |
|
283 \endisadelimproof |
|
284 % |
|
285 \isatagproof |
|
286 % |
|
287 \endisatagproof |
|
288 {\isafoldproof}% |
|
289 % |
|
290 \isadelimproof |
|
291 % |
|
292 \endisadelimproof |
|
293 % |
|
294 \isadelimML |
|
295 % |
|
296 \endisadelimML |
|
297 % |
|
298 \isatagML |
|
299 % |
|
300 \endisatagML |
|
301 {\isafoldML}% |
|
302 % |
|
303 \isadelimML |
|
304 % |
|
305 \endisadelimML |
|
306 % |
|
307 \isadelimtheory |
|
308 % |
|
309 \endisadelimtheory |
|
310 % |
|
311 \isatagtheory |
|
312 % |
|
313 \endisatagtheory |
|
314 {\isafoldtheory}% |
|
315 % |
|
316 \isadelimtheory |
|
317 % |
|
318 \endisadelimtheory |
|
319 \end{isabellebody}% |
|
320 %%% Local Variables: |
|
321 %%% mode: latex |
|
322 %%% TeX-master: "root" |
|
323 %%% End: |