|
1 \documentclass[dvipsnames,14pt,t]{beamer} |
|
2 \usepackage{proof} |
|
3 \usepackage{beamerthemeplainculight} |
|
4 \usepackage[T1]{fontenc} |
|
5 \usepackage[latin1]{inputenc} |
|
6 \usepackage{mathpartir} |
|
7 \usepackage{isabelle} |
|
8 \usepackage{isabellesym} |
|
9 \usepackage[absolute,overlay]{textpos} |
|
10 \usepackage{ifthen} |
|
11 \usepackage{tikz} |
|
12 \usepackage{courier} |
|
13 \usepackage{listings} |
|
14 \usetikzlibrary{arrows} |
|
15 \usetikzlibrary{positioning} |
|
16 \usetikzlibrary{calc} |
|
17 \usepackage{graphicx} |
|
18 |
|
19 \isabellestyle{rm} |
|
20 \renewcommand{\isastyle}{\rm}% |
|
21 \renewcommand{\isastyleminor}{\rm}% |
|
22 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}% |
|
23 \renewcommand{\isatagproof}{} |
|
24 \renewcommand{\endisatagproof}{} |
|
25 \renewcommand{\isamarkupcmt}[1]{#1} |
|
26 |
|
27 % Isabelle characters |
|
28 \renewcommand{\isacharunderscore}{\_} |
|
29 \renewcommand{\isacharbar}{\isamath{\mid}} |
|
30 \renewcommand{\isasymiota}{} |
|
31 \renewcommand{\isacharbraceleft}{\{} |
|
32 \renewcommand{\isacharbraceright}{\}} |
|
33 \renewcommand{\isacharless}{$\langle$} |
|
34 \renewcommand{\isachargreater}{$\rangle$} |
|
35 \renewcommand{\isasymsharp}{\isamath{\#}} |
|
36 \renewcommand{\isasymdots}{\isamath{...}} |
|
37 \renewcommand{\isasymbullet}{\act} |
|
38 |
|
39 |
|
40 |
|
41 \definecolor{javared}{rgb}{0.6,0,0} % for strings |
|
42 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments |
|
43 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords |
|
44 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc |
|
45 |
|
46 \lstset{language=Java, |
|
47 basicstyle=\ttfamily, |
|
48 keywordstyle=\color{javapurple}\bfseries, |
|
49 stringstyle=\color{javagreen}, |
|
50 commentstyle=\color{javagreen}, |
|
51 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
52 numbers=left, |
|
53 numberstyle=\tiny\color{black}, |
|
54 stepnumber=1, |
|
55 numbersep=10pt, |
|
56 tabsize=2, |
|
57 showspaces=false, |
|
58 showstringspaces=false} |
|
59 |
|
60 \lstdefinelanguage{scala}{ |
|
61 morekeywords={abstract,case,catch,class,def,% |
|
62 do,else,extends,false,final,finally,% |
|
63 for,if,implicit,import,match,mixin,% |
|
64 new,null,object,override,package,% |
|
65 private,protected,requires,return,sealed,% |
|
66 super,this,throw,trait,true,try,% |
|
67 type,val,var,while,with,yield}, |
|
68 otherkeywords={=>,<-,<\%,<:,>:,\#,@}, |
|
69 sensitive=true, |
|
70 morecomment=[l]{//}, |
|
71 morecomment=[n]{/*}{*/}, |
|
72 morestring=[b]", |
|
73 morestring=[b]', |
|
74 morestring=[b]""" |
|
75 } |
|
76 |
|
77 \lstset{language=Scala, |
|
78 basicstyle=\ttfamily, |
|
79 keywordstyle=\color{javapurple}\bfseries, |
|
80 stringstyle=\color{javagreen}, |
|
81 commentstyle=\color{javagreen}, |
|
82 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
83 numbers=left, |
|
84 numberstyle=\tiny\color{black}, |
|
85 stepnumber=1, |
|
86 numbersep=10pt, |
|
87 tabsize=2, |
|
88 showspaces=false, |
|
89 showstringspaces=false} |
|
90 |
|
91 % beamer stuff |
|
92 \renewcommand{\slidecaption}{APP 06, King's College London, 29 October 2012} |
|
93 |
|
94 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
|
95 \begin{document} |
|
96 |
|
97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
98 \mode<presentation>{ |
|
99 \begin{frame}<1>[t] |
|
100 \frametitle{% |
|
101 \begin{tabular}{@ {}c@ {}} |
|
102 \\ |
|
103 \LARGE Access Control and \\[-3mm] |
|
104 \LARGE Privacy Policies (6)\\[-6mm] |
|
105 \end{tabular}}\bigskip\bigskip\bigskip |
|
106 |
|
107 %\begin{center} |
|
108 %\includegraphics[scale=1.3]{pics/barrier.jpg} |
|
109 %\end{center} |
|
110 |
|
111 \normalsize |
|
112 \begin{center} |
|
113 \begin{tabular}{ll} |
|
114 Email: & christian.urban at kcl.ac.uk\\ |
|
115 Of$\!$fice: & S1.27 (1st floor Strand Building)\\ |
|
116 Slides: & KEATS (also homework is there)\\ |
|
117 \end{tabular} |
|
118 \end{center} |
|
119 |
|
120 |
|
121 \end{frame}} |
|
122 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
123 |
|
124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
125 \mode<presentation>{ |
|
126 \begin{frame}[c] |
|
127 \frametitle{1st Week} |
|
128 |
|
129 \begin{itemize} |
|
130 \item What are hashes and salts?\bigskip\pause |
|
131 \item \ldots can be use to store securely data on a client, but |
|
132 you cannot make your protocol dependent on the |
|
133 presence of the data\bigskip\pause |
|
134 \item \ldots can be used to store and verify passwords |
|
135 |
|
136 \end{itemize} |
|
137 |
|
138 \end{frame}} |
|
139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
140 |
|
141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
142 \mode<presentation>{ |
|
143 \begin{frame}[c] |
|
144 \frametitle{2nd Week} |
|
145 |
|
146 \begin{itemize} |
|
147 \item Buffer overflows\bigskip |
|
148 \item choice of programming language can mitigate or even eliminate this problem |
|
149 \end{itemize} |
|
150 |
|
151 \end{frame}} |
|
152 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
153 |
|
154 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
155 \mode<presentation>{ |
|
156 \begin{frame}[c] |
|
157 \frametitle{3rd Week} |
|
158 |
|
159 \begin{itemize} |
|
160 \item defence in depth\bigskip |
|
161 \item privilege separation afforded by the OS |
|
162 \end{itemize} |
|
163 |
|
164 \begin{center} |
|
165 \begin{tikzpicture}[scale=1] |
|
166 |
|
167 \draw[line width=1mm] (0, 1.1) rectangle (1.2,2); |
|
168 \draw (4.7,1) node {Internet}; |
|
169 \draw (0.6,1.7) node {\footnotesize Slave}; |
|
170 \draw[line width=1mm] (0, 0) rectangle (1.2,0.9); |
|
171 \draw (0.6,1.7) node {\footnotesize Slave}; |
|
172 \draw (0.6,0.6) node {\footnotesize Slave}; |
|
173 \draw (0.6,-0.5) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] processes\end{tabular}}; |
|
174 \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}}; |
|
175 |
|
176 \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2); |
|
177 \draw (-2.9,1.7) node {\footnotesize Monitor}; |
|
178 |
|
179 \draw[white] (1.7,1) node (X) {}; |
|
180 \draw[white] (3.7,1) node (Y) {}; |
|
181 \draw[red, <->, line width = 2mm] (X) -- (Y); |
|
182 |
|
183 \draw[red, <->, line width = 1mm] (-0.4,1.4) -- (-1.4,1.1); |
|
184 \draw[red, <->, line width = 1mm] (-0.4,0.6) -- (-1.4,0.9); |
|
185 |
|
186 \end{tikzpicture} |
|
187 \end{center} |
|
188 |
|
189 \end{frame}} |
|
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
191 |
|
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
193 \mode<presentation>{ |
|
194 \begin{frame}[c] |
|
195 \frametitle{4th Week} |
|
196 |
|
197 \begin{itemize} |
|
198 \item voting\ldots has security requirements that are in tension with each other |
|
199 \begin{center} |
|
200 integrity vs ballot secrecy\\ |
|
201 authentication vs enfranchisment |
|
202 \end{center}\bigskip |
|
203 |
|
204 \item electronic voting makes `whole sale' fraud easier as opposed to `retail attacks' |
|
205 \end{itemize} |
|
206 |
|
207 \end{frame}} |
|
208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
209 |
|
210 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
211 \mode<presentation>{ |
|
212 \begin{frame}[c] |
|
213 \frametitle{5th Week} |
|
214 |
|
215 \begin{itemize} |
|
216 \item access control logic\bigskip |
|
217 |
|
218 \item formulas |
|
219 \item judgements |
|
220 \item inference rules |
|
221 \end{itemize} |
|
222 |
|
223 \end{frame}} |
|
224 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
225 |
|
226 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
227 \mode<presentation>{ |
|
228 \begin{frame}[t] |
|
229 \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}} |
|
230 |
|
231 Formulas |
|
232 |
|
233 \begin{itemize} |
|
234 \item[] |
|
235 |
|
236 \begin{center}\color{blue} |
|
237 \begin{tabular}[t]{rcl@ {\hspace{10mm}}l} |
|
238 \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ |
|
239 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ |
|
240 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ |
|
241 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ |
|
242 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\ |
|
243 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\ |
|
244 & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ |
|
245 \end{tabular} |
|
246 \end{center} |
|
247 |
|
248 \end{itemize} |
|
249 |
|
250 Judgements |
|
251 |
|
252 \begin{itemize} |
|
253 \item[] \mbox{\hspace{9mm}}\bl{$\Gamma \vdash \text{F}$} |
|
254 \end{itemize} |
|
255 |
|
256 \end{frame}} |
|
257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
258 |
|
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
260 \mode<presentation>{ |
|
261 \begin{frame}[c] |
|
262 \frametitle{Inference Rules} |
|
263 |
|
264 \begin{center} |
|
265 \bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\ |
|
266 |
|
267 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}} |
|
268 \qquad |
|
269 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\ |
|
270 |
|
271 \bl{\infer{\Gamma \vdash P\,\text{says}\, F}{\Gamma \vdash F}}\medskip\\ |
|
272 |
|
273 \bl{\infer{\Gamma \vdash P \,\text{says}\, F_2} |
|
274 {\Gamma \vdash P \,\text{says}\, (F_1\Rightarrow F_2) \quad |
|
275 \Gamma \vdash P \,\text{says}\, F_1}} |
|
276 \end{center} |
|
277 |
|
278 \end{frame}} |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 |
|
281 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
282 \mode<presentation>{ |
|
283 \begin{frame}[c] |
|
284 \frametitle{Proofs} |
|
285 |
|
286 \begin{center} |
|
287 \bl{ |
|
288 \infer{\Gamma \vdash F} |
|
289 {\infer{\hspace{1cm}:\hspace{1cm}} |
|
290 {\infer{\hspace{1cm}:\hspace{1cm}}{:} |
|
291 & |
|
292 \infer{\hspace{1cm}:\hspace{1cm}}{:\quad :} |
|
293 }} |
|
294 } |
|
295 \end{center} |
|
296 |
|
297 \end{frame}} |
|
298 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
299 |
|
300 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
301 \mode<presentation>{ |
|
302 \begin{frame}[c] |
|
303 \frametitle{The Access Control Problem} |
|
304 |
|
305 |
|
306 \begin{center} |
|
307 \begin{tikzpicture}[scale=1] |
|
308 |
|
309 \draw[line width=1mm] (-.3, -0.5) rectangle (1.5,2); |
|
310 \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; |
|
311 \draw (4.2,1) node {\begin{tabular}{l}provable/\\not provable\end{tabular}}; |
|
312 \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}}; |
|
313 |
|
314 \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); |
|
315 \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); |
|
316 \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); |
|
317 |
|
318 \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}}; |
|
319 |
|
320 \end{tikzpicture} |
|
321 \end{center} |
|
322 |
|
323 \end{frame}} |
|
324 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
325 |
|
326 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
327 \mode<presentation>{ |
|
328 \begin{frame}[c] |
|
329 \frametitle{} |
|
330 |
|
331 Recall the following scenario: |
|
332 |
|
333 \begin{itemize} |
|
334 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}} |
|
335 should be deleted, then this file must be deleted. |
|
336 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
|
337 \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted. |
|
338 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}. |
|
339 \end{itemize}\bigskip |
|
340 |
|
341 \small |
|
342 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
343 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\ |
|
344 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ |
|
345 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\ |
|
346 \end{tabular}}\medskip |
|
347 |
|
348 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}} |
|
349 \end{frame}} |
|
350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
351 |
|
352 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
353 \mode<presentation>{ |
|
354 \begin{frame}[c] |
|
355 |
|
356 How to prove \bl{$\Gamma \vdash F$}?\bigskip\bigskip |
|
357 |
|
358 \begin{center} |
|
359 \Large \bl{\infer{\Gamma, F\vdash F}{}} |
|
360 \end{center} |
|
361 |
|
362 \end{frame}} |
|
363 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
364 |
|
365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
366 \mode<presentation>{ |
|
367 \begin{frame}[c] |
|
368 |
|
369 \begin{center} |
|
370 \Large |
|
371 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}} |
|
372 \end{center} |
|
373 |
|
374 \end{frame}} |
|
375 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
376 |
|
377 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
378 \mode<presentation>{ |
|
379 \begin{frame}[c] |
|
380 |
|
381 \begin{center} |
|
382 \Large |
|
383 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} |
|
384 \end{center} |
|
385 |
|
386 \end{frame}} |
|
387 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
388 |
|
389 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
390 \mode<presentation>{ |
|
391 \begin{frame}[c] |
|
392 |
|
393 \begin{center} |
|
394 \Large |
|
395 \bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}\qquad |
|
396 \bl{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}\ |
|
397 \end{center} |
|
398 |
|
399 \end{frame}} |
|
400 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
401 |
|
402 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
403 \mode<presentation>{ |
|
404 \begin{frame}[c] |
|
405 |
|
406 \begin{center} |
|
407 \Large |
|
408 \bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 \quad \Gamma \vdash F_2}} |
|
409 \end{center} |
|
410 |
|
411 \end{frame}} |
|
412 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
413 |
|
414 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
415 \mode<presentation>{ |
|
416 \begin{frame}[t] |
|
417 |
|
418 I want to prove \bl{$\Gamma \vdash \text{Pred}$}\bigskip\bigskip\pause |
|
419 |
|
420 \begin{enumerate} |
|
421 \item I found that \bl{$\Gamma$} contains the assumption \bl{$F_1 \Rightarrow F_2$}\bigskip\pause |
|
422 \item If I can prove \bl{$\Gamma \vdash F_1$},\pause{} then I can prove |
|
423 \begin{center} |
|
424 \bl{$\Gamma \vdash F_2$} |
|
425 \end{center}\bigskip\pause |
|
426 |
|
427 \item So better I try to prove \bl{$\Gamma \vdash \text{Pred}$} with the additional assumption |
|
428 \bl{$F_2$}.\bigskip |
|
429 \begin{center} |
|
430 \bl{$F_2, \Gamma \vdash \text{Pred}$} |
|
431 \end{center} |
|
432 \end{enumerate} |
|
433 |
|
434 \only<4>{ |
|
435 \begin{textblock}{11}(1,10.5) |
|
436 \bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}} |
|
437 \end{textblock}} |
|
438 |
|
439 |
|
440 \end{frame}} |
|
441 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
442 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
443 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
444 \mode<presentation>{ |
|
445 \begin{frame}[c] |
|
446 |
|
447 \begin{itemize} |
|
448 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ |
|
449 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip |
|
450 |
|
451 \begin{center} |
|
452 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} |
|
453 \end{center} |
|
454 |
|
455 \item \bl{$P$} speaks for \bl{$Q$}\smallskip\\ |
|
456 \bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip |
|
457 |
|
458 \begin{center} |
|
459 \bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}} |
|
460 \medskip\\ |
|
461 \bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\ |
|
462 |
|
463 \end{center} |
|
464 \end{itemize} |
|
465 |
|
466 \end{frame}} |
|
467 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
468 |
|
469 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
470 \mode<presentation>{ |
|
471 \begin{frame}[c] |
|
472 \frametitle{Protocol Specifications} |
|
473 |
|
474 The Needham-Schroeder Protocol: |
|
475 |
|
476 \begin{center} |
|
477 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
478 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B, N_A$}\\ |
|
479 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
480 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\ |
|
481 Message 4 & \bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\ |
|
482 Message 5 & \bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\ |
|
483 \end{tabular} |
|
484 \end{center} |
|
485 |
|
486 \end{frame}} |
|
487 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
488 |
|
489 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
490 \mode<presentation>{ |
|
491 \begin{frame}[c] |
|
492 \frametitle{Trusted Third Party} |
|
493 |
|
494 Simple protocol for establishing a secure connection via a mutually |
|
495 trusted 3rd party (server): |
|
496 |
|
497 \begin{center} |
|
498 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
499 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\ |
|
500 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
501 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\ |
|
502 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\ |
|
503 \end{tabular} |
|
504 \end{center} |
|
505 |
|
506 \end{frame}} |
|
507 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
508 |
|
509 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
510 \mode<presentation>{ |
|
511 \begin{frame}[c] |
|
512 \frametitle{Sending Messages} |
|
513 |
|
514 \begin{itemize} |
|
515 \item Alice sends a message \bl{$m$} |
|
516 \begin{center} |
|
517 \bl{Alice says $m$} |
|
518 \end{center}\medskip\pause |
|
519 |
|
520 \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$}) |
|
521 \begin{center} |
|
522 \bl{Alice says $\{m\}_K$} |
|
523 \end{center}\medskip\pause |
|
524 |
|
525 \item Decryption of Alice's message\smallskip |
|
526 \begin{center} |
|
527 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
528 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
529 \end{center} |
|
530 \end{itemize} |
|
531 |
|
532 \end{frame}} |
|
533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
534 |
|
535 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
536 \mode<presentation>{ |
|
537 \begin{frame}[c] |
|
538 \frametitle{Encryption} |
|
539 |
|
540 \begin{itemize} |
|
541 \item Encryption of a message\smallskip |
|
542 \begin{center} |
|
543 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
|
544 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
545 \end{center} |
|
546 \end{itemize} |
|
547 |
|
548 \end{frame}} |
|
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
550 |
|
551 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
552 \mode<presentation>{ |
|
553 \begin{frame}[c] |
|
554 \frametitle{Public/Private Keys} |
|
555 |
|
556 \begin{itemize} |
|
557 \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip |
|
558 \begin{center} |
|
559 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
560 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} & |
|
561 \Gamma \vdash K_{Bob}^{priv}}}} |
|
562 \end{center}\bigskip\pause |
|
563 |
|
564 \item this is {\bf not} a derived rule! |
|
565 \end{itemize} |
|
566 |
|
567 \end{frame}} |
|
568 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
569 |
|
570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
571 \mode<presentation>{ |
|
572 \begin{frame}[c] |
|
573 \frametitle{Trusted Third Party} |
|
574 |
|
575 \begin{itemize} |
|
576 \item Alice calls Sam for a key to communicate with Bob |
|
577 \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared) |
|
578 \item Alice sends the message encrypted with the key and the second key it recieved |
|
579 \end{itemize}\bigskip |
|
580 |
|
581 \begin{center} |
|
582 \bl{\begin{tabular}{lcl} |
|
583 $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\ |
|
584 $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
585 $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\ |
|
586 $A$ sends $B$ &:& $\{m\}_{K_{AB}}$ |
|
587 \end{tabular}} |
|
588 \end{center} |
|
589 |
|
590 \end{frame}} |
|
591 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
592 |
|
593 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
594 \mode<presentation>{ |
|
595 \begin{frame}[c] |
|
596 \frametitle{Sending Rule} |
|
597 |
|
598 \bl{\begin{center} |
|
599 \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F} |
|
600 {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}} |
|
601 \end{center}}\bigskip\pause |
|
602 |
|
603 \bl{$P \,\text{sends}\, Q : F \dn$}\\ |
|
604 \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$} |
|
605 |
|
606 \end{frame}} |
|
607 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
608 |
|
609 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
610 \mode<presentation>{ |
|
611 \begin{frame}[c] |
|
612 \frametitle{Trusted Third Party} |
|
613 |
|
614 \begin{center} |
|
615 \bl{\begin{tabular}{l} |
|
616 $A$ sends $S$ : $\textit{Connect}(A,B)$\\ |
|
617 \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ |
|
618 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
|
619 \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\ |
|
620 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
621 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
|
622 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
|
623 \end{tabular}} |
|
624 \end{center}\bigskip\pause |
|
625 |
|
626 |
|
627 \bl{$\Gamma \vdash B \,\text{says} \, m$}? |
|
628 \end{frame}} |
|
629 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
630 \end{document} |
|
631 |
|
632 %%% Local Variables: |
|
633 %%% mode: latex |
|
634 %%% TeX-master: t |
|
635 %%% End: |
|
636 |