|
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 \usetikzlibrary{shapes} |
|
19 \usetikzlibrary{shadows} |
|
20 \usetikzlibrary{plotmarks} |
|
21 |
|
22 |
|
23 \isabellestyle{rm} |
|
24 \renewcommand{\isastyle}{\rm}% |
|
25 \renewcommand{\isastyleminor}{\rm}% |
|
26 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}% |
|
27 \renewcommand{\isatagproof}{} |
|
28 \renewcommand{\endisatagproof}{} |
|
29 \renewcommand{\isamarkupcmt}[1]{#1} |
|
30 |
|
31 % Isabelle characters |
|
32 \renewcommand{\isacharunderscore}{\_} |
|
33 \renewcommand{\isacharbar}{\isamath{\mid}} |
|
34 \renewcommand{\isasymiota}{} |
|
35 \renewcommand{\isacharbraceleft}{\{} |
|
36 \renewcommand{\isacharbraceright}{\}} |
|
37 \renewcommand{\isacharless}{$\langle$} |
|
38 \renewcommand{\isachargreater}{$\rangle$} |
|
39 \renewcommand{\isasymsharp}{\isamath{\#}} |
|
40 \renewcommand{\isasymdots}{\isamath{...}} |
|
41 \renewcommand{\isasymbullet}{\act} |
|
42 |
|
43 |
|
44 |
|
45 \definecolor{javared}{rgb}{0.6,0,0} % for strings |
|
46 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments |
|
47 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords |
|
48 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc |
|
49 |
|
50 \lstset{language=Java, |
|
51 basicstyle=\ttfamily, |
|
52 keywordstyle=\color{javapurple}\bfseries, |
|
53 stringstyle=\color{javagreen}, |
|
54 commentstyle=\color{javagreen}, |
|
55 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
56 numbers=left, |
|
57 numberstyle=\tiny\color{black}, |
|
58 stepnumber=1, |
|
59 numbersep=10pt, |
|
60 tabsize=2, |
|
61 showspaces=false, |
|
62 showstringspaces=false} |
|
63 |
|
64 \lstdefinelanguage{scala}{ |
|
65 morekeywords={abstract,case,catch,class,def,% |
|
66 do,else,extends,false,final,finally,% |
|
67 for,if,implicit,import,match,mixin,% |
|
68 new,null,object,override,package,% |
|
69 private,protected,requires,return,sealed,% |
|
70 super,this,throw,trait,true,try,% |
|
71 type,val,var,while,with,yield}, |
|
72 otherkeywords={=>,<-,<\%,<:,>:,\#,@}, |
|
73 sensitive=true, |
|
74 morecomment=[l]{//}, |
|
75 morecomment=[n]{/*}{*/}, |
|
76 morestring=[b]", |
|
77 morestring=[b]', |
|
78 morestring=[b]""" |
|
79 } |
|
80 |
|
81 \lstset{language=Scala, |
|
82 basicstyle=\ttfamily, |
|
83 keywordstyle=\color{javapurple}\bfseries, |
|
84 stringstyle=\color{javagreen}, |
|
85 commentstyle=\color{javagreen}, |
|
86 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
87 numbers=left, |
|
88 numberstyle=\tiny\color{black}, |
|
89 stepnumber=1, |
|
90 numbersep=10pt, |
|
91 tabsize=2, |
|
92 showspaces=false, |
|
93 showstringspaces=false} |
|
94 |
|
95 % beamer stuff |
|
96 \renewcommand{\slidecaption}{APP 07, King's College London, 13 November 2012} |
|
97 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
98 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
|
99 |
|
100 |
|
101 % The data files, written on the first run. |
|
102 \begin{filecontents}{re-python.data} |
|
103 1 0.029 |
|
104 5 0.029 |
|
105 10 0.029 |
|
106 15 0.032 |
|
107 16 0.042 |
|
108 17 0.042 |
|
109 18 0.055 |
|
110 19 0.084 |
|
111 20 0.136 |
|
112 21 0.248 |
|
113 22 0.464 |
|
114 23 0.899 |
|
115 24 1.773 |
|
116 25 3.505 |
|
117 26 6.993 |
|
118 27 14.503 |
|
119 28 29.307 |
|
120 #29 58.886 |
|
121 \end{filecontents} |
|
122 |
|
123 \begin{filecontents}{re1.data} |
|
124 1 0.00179 |
|
125 2 0.00011 |
|
126 3 0.00014 |
|
127 4 0.00026 |
|
128 5 0.00050 |
|
129 6 0.00095 |
|
130 7 0.00190 |
|
131 8 0.00287 |
|
132 9 0.00779 |
|
133 10 0.01399 |
|
134 11 0.01894 |
|
135 12 0.03666 |
|
136 13 0.07994 |
|
137 14 0.08944 |
|
138 15 0.02377 |
|
139 16 0.07392 |
|
140 17 0.22798 |
|
141 18 0.65310 |
|
142 19 2.11360 |
|
143 20 6.31606 |
|
144 21 21.46013 |
|
145 \end{filecontents} |
|
146 |
|
147 \begin{filecontents}{re2.data} |
|
148 1 0.00240 |
|
149 2 0.00013 |
|
150 3 0.00020 |
|
151 4 0.00030 |
|
152 5 0.00049 |
|
153 6 0.00083 |
|
154 7 0.00146 |
|
155 8 0.00228 |
|
156 9 0.00351 |
|
157 10 0.00640 |
|
158 11 0.01217 |
|
159 12 0.02565 |
|
160 13 0.01382 |
|
161 14 0.02423 |
|
162 15 0.05065 |
|
163 16 0.06522 |
|
164 17 0.02140 |
|
165 18 0.05176 |
|
166 19 0.18254 |
|
167 20 0.51898 |
|
168 21 1.39631 |
|
169 22 2.69501 |
|
170 23 8.07952 |
|
171 \end{filecontents} |
|
172 |
|
173 \begin{filecontents}{re-internal.data} |
|
174 1 0.00069 |
|
175 301 0.00700 |
|
176 601 0.00297 |
|
177 901 0.00470 |
|
178 1201 0.01301 |
|
179 1501 0.01175 |
|
180 1801 0.01761 |
|
181 2101 0.01787 |
|
182 2401 0.02717 |
|
183 2701 0.03932 |
|
184 3001 0.03470 |
|
185 3301 0.04349 |
|
186 3601 0.05411 |
|
187 3901 0.06181 |
|
188 4201 0.07119 |
|
189 4501 0.08578 |
|
190 \end{filecontents} |
|
191 |
|
192 \begin{filecontents}{re3.data} |
|
193 1 0.001605 |
|
194 501 0.131066 |
|
195 1001 0.057885 |
|
196 1501 0.136875 |
|
197 2001 0.176238 |
|
198 2501 0.254363 |
|
199 3001 0.37262 |
|
200 3501 0.500946 |
|
201 4001 0.638384 |
|
202 4501 0.816605 |
|
203 5001 1.00491 |
|
204 5501 1.232505 |
|
205 6001 1.525672 |
|
206 6501 1.757502 |
|
207 7001 2.092784 |
|
208 7501 2.429224 |
|
209 8001 2.803037 |
|
210 8501 3.463045 |
|
211 9001 3.609 |
|
212 9501 4.081504 |
|
213 10001 4.54569 |
|
214 \end{filecontents} |
|
215 |
|
216 |
|
217 \begin{document} |
|
218 |
|
219 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
220 \mode<presentation>{ |
|
221 \begin{frame}<1>[t] |
|
222 \frametitle{% |
|
223 \begin{tabular}{@ {}c@ {}} |
|
224 \\ |
|
225 \LARGE Access Control and \\[-3mm] |
|
226 \LARGE Privacy Policies (7)\\[-6mm] |
|
227 \end{tabular}}\bigskip\bigskip\bigskip |
|
228 |
|
229 %\begin{center} |
|
230 %\includegraphics[scale=1.3]{pics/barrier.jpg} |
|
231 %\end{center} |
|
232 |
|
233 \normalsize |
|
234 \begin{center} |
|
235 \begin{tabular}{ll} |
|
236 Email: & christian.urban at kcl.ac.uk\\ |
|
237 Of$\!$fice: & S1.27 (1st floor Strand Building)\\ |
|
238 Slides: & KEATS (also homework is there)\\ |
|
239 \end{tabular} |
|
240 \end{center} |
|
241 |
|
242 |
|
243 \end{frame}} |
|
244 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
245 |
|
246 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
247 \mode<presentation>{ |
|
248 \begin{frame}[c] |
|
249 \frametitle{Judgements} |
|
250 |
|
251 \begin{center} |
|
252 \begin{tikzpicture}[scale=1] |
|
253 |
|
254 \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}}; |
|
255 \onslide<2->{ |
|
256 \draw (-1,-0.3) node (X) {}; |
|
257 \draw (-2.0,-2.0) node (Y) {}; |
|
258 \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}}; |
|
259 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
260 |
|
261 \draw (1.2,-0.1) node (X1) {}; |
|
262 \draw (2.8,-0.1) node (Y1) {}; |
|
263 \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}}; |
|
264 \draw[red, ->, line width = 2mm] (Y1) -- (X1); |
|
265 |
|
266 \draw (-0.1,0.1) node (X2) {}; |
|
267 \draw (0.5,1.5) node (Y2) {}; |
|
268 \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}}; |
|
269 \draw[red, ->, line width = 2mm] (Y2) -- (X2);} |
|
270 |
|
271 \end{tikzpicture} |
|
272 \end{center} |
|
273 |
|
274 \pause\pause |
|
275 \footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic) |
|
276 \end{frame}} |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 \mode<presentation>{ |
|
281 \begin{frame}[c] |
|
282 \frametitle{Inference Rules} |
|
283 |
|
284 \begin{center} |
|
285 \begin{tikzpicture}[scale=1] |
|
286 |
|
287 \draw (0.0,0.0) node |
|
288 {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}}; |
|
289 |
|
290 \draw (-0.1,-0.7) node (X) {}; |
|
291 \draw (-0.1,-1.9) node (Y) {}; |
|
292 \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}}; |
|
293 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
294 |
|
295 \draw (-1,0.6) node (X2) {}; |
|
296 \draw (0.0,1.6) node (Y2) {}; |
|
297 \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}}; |
|
298 \draw[red, ->, line width = 2mm] (Y2) -- (X2); |
|
299 \draw (1,0.6) node (X3) {}; |
|
300 \draw (0.0,1.6) node (Y3) {}; |
|
301 \draw[red, ->, line width = 2mm] (Y3) -- (X3); |
|
302 \end{tikzpicture} |
|
303 \end{center} |
|
304 |
|
305 \only<2>{ |
|
306 \begin{textblock}{11}(1,13) |
|
307 \small |
|
308 \bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $} |
|
309 \end{textblock}} |
|
310 \only<3>{ |
|
311 \begin{textblock}{11}(1,13) |
|
312 \small |
|
313 \bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge |
|
314 \underbrace{P \,\text{says}\, G}_{F_2} $} |
|
315 \end{textblock}} |
|
316 |
|
317 \end{frame}} |
|
318 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
319 |
|
320 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
321 \mode<presentation>{ |
|
322 \begin{frame}[c] |
|
323 |
|
324 \begin{center} |
|
325 \Large |
|
326 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1\Rightarrow F_2 & \Gamma \vdash F_1}}\bigskip\bigskip\bigskip |
|
327 |
|
328 \bl{\infer{\Gamma\vdash P\,\text{says}\, F}{\Gamma \vdash F}} |
|
329 \end{center} |
|
330 |
|
331 \end{frame}} |
|
332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
333 |
|
334 |
|
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
336 \mode<presentation>{ |
|
337 \begin{frame}[t] |
|
338 |
|
339 We want to prove |
|
340 |
|
341 \begin{center} |
|
342 \bl{$\Gamma \vdash \text{del\_file}$} |
|
343 \end{center}\pause |
|
344 |
|
345 There is an inference rule |
|
346 |
|
347 \begin{center} |
|
348 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} |
|
349 \end{center}\pause |
|
350 |
|
351 So we can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause |
|
352 |
|
353 \bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\ |
|
354 So we can use the rule |
|
355 |
|
356 \begin{center} |
|
357 \bl{\infer{\Gamma, F \vdash F}{}} |
|
358 \end{center} |
|
359 |
|
360 \onslide<5>{\bf\alert{What is wrong with this?}} |
|
361 \hfill{\bf Done. Qed.} |
|
362 |
|
363 \end{frame}} |
|
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
365 |
|
366 |
|
367 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
368 \mode<presentation>{ |
|
369 \begin{frame}[c] |
|
370 \frametitle{Digression: Proofs in CS} |
|
371 |
|
372 Formal proofs in CS sound like science fiction? Completely irrelevant! |
|
373 Lecturers gone mad!\pause |
|
374 |
|
375 \begin{itemize} |
|
376 \item in 2008, verification of a small C-compiler |
|
377 \begin{itemize} |
|
378 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
|
379 \item is as good as \texttt{gcc -O1}, but less buggy |
|
380 \end{itemize} |
|
381 \medskip |
|
382 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
|
383 \begin{itemize} |
|
384 \item 200k loc of proof |
|
385 \item 25 - 30 person years |
|
386 \item found 160 bugs in the C code (144 by the proof) |
|
387 \end{itemize} |
|
388 \end{itemize} |
|
389 |
|
390 \end{frame}} |
|
391 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
392 |
|
393 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
394 \mode<presentation>{ |
|
395 \begin{frame}[c] |
|
396 \frametitle{} |
|
397 |
|
398 \begin{tabular}{c@ {\hspace{2mm}}c} |
|
399 \\[6mm] |
|
400 \begin{tabular}{c} |
|
401 \includegraphics[scale=0.11]{harper.jpg}\\[-2mm] |
|
402 {\footnotesize Bob Harper}\\[-2.5mm] |
|
403 {\footnotesize (CMU)} |
|
404 \end{tabular} |
|
405 \begin{tabular}{c} |
|
406 \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm] |
|
407 {\footnotesize Frank Pfenning}\\[-2.5mm] |
|
408 {\footnotesize (CMU)} |
|
409 \end{tabular} & |
|
410 |
|
411 \begin{tabular}{p{6cm}} |
|
412 \raggedright |
|
413 \color{gray}{published a proof about a specification in a journal (2005), |
|
414 $\sim$31pages} |
|
415 \end{tabular}\\ |
|
416 |
|
417 \pause |
|
418 \\[0mm] |
|
419 |
|
420 \begin{tabular}{c} |
|
421 \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] |
|
422 {\footnotesize Andrew Appel}\\[-2.5mm] |
|
423 {\footnotesize (Princeton)} |
|
424 \end{tabular} & |
|
425 |
|
426 \begin{tabular}{p{6cm}} |
|
427 \raggedright |
|
428 \color{gray}{relied on their proof in a\\ {\bf security} critical application} |
|
429 \end{tabular} |
|
430 \end{tabular} |
|
431 |
|
432 \end{frame}} |
|
433 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
434 |
|
435 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
436 \mode<presentation>{ |
|
437 \begin{frame} |
|
438 \frametitle{Proof-Carrying Code} |
|
439 |
|
440 \begin{textblock}{10}(2.5,2.2) |
|
441 \begin{block}{Idea:} |
|
442 \begin{center} |
|
443 \begin{tikzpicture} |
|
444 \draw[help lines,cream] (0,0.2) grid (8,4); |
|
445 |
|
446 \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4); |
|
447 \node[anchor=base] at (6.5,2.8) |
|
448 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user: untrusted code\end{tabular}}; |
|
449 |
|
450 \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4); |
|
451 \node[anchor=base] at (1.5,2.3) |
|
452 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering developer ---\\ web server\end{tabular}}; |
|
453 |
|
454 \onslide<3->{ |
|
455 \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8); |
|
456 \node[anchor=base,white] at (6.5,1.1) |
|
457 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};} |
|
458 |
|
459 \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code}; |
|
460 \onslide<2->{ |
|
461 \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate}; |
|
462 \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof}}; |
|
463 } |
|
464 |
|
465 |
|
466 \end{tikzpicture} |
|
467 \end{center} |
|
468 \end{block} |
|
469 \end{textblock} |
|
470 |
|
471 %\begin{textblock}{15}(2,12) |
|
472 %\small |
|
473 %\begin{itemize} |
|
474 %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; |
|
475 %803 loc in C including 2 library functions)\\[-3mm] |
|
476 %\item<5-> 167 loc in C implement a type-checker |
|
477 %\end{itemize} |
|
478 %\end{textblock} |
|
479 |
|
480 \end{frame}} |
|
481 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
482 |
|
483 \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex] |
|
484 \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, |
|
485 draw=black!50, top color=white, bottom color=black!20] |
|
486 \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, |
|
487 draw=red!70, top color=white, bottom color=red!50!black!20] |
|
488 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
489 \mode<presentation>{ |
|
490 \begin{frame}<2->[squeeze] |
|
491 \frametitle{} |
|
492 |
|
493 \begin{columns} |
|
494 |
|
495 \begin{column}{0.8\textwidth} |
|
496 \begin{textblock}{0}(1,2) |
|
497 |
|
498 \begin{tikzpicture} |
|
499 \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm] |
|
500 { \&[-10mm] |
|
501 \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \& |
|
502 \node (proof1) [node1] {\large Proof}; \& |
|
503 \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\ |
|
504 |
|
505 \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
506 \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \& |
|
507 \onslide<4->{\node (proof2) [node1] {\large Proof};} \& |
|
508 \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ |
|
509 |
|
510 \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
511 \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& |
|
512 \onslide<5->{\node (proof3) [node1] {\large Proof};} \& |
|
513 \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\ |
|
514 |
|
515 \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& |
|
516 \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& |
|
517 \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \& |
|
518 \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ |
|
519 }; |
|
520 |
|
521 \draw[->,black!50,line width=2mm] (proof1) -- (def1); |
|
522 \draw[->,black!50,line width=2mm] (proof1) -- (alg1); |
|
523 |
|
524 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);} |
|
525 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);} |
|
526 |
|
527 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);} |
|
528 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);} |
|
529 |
|
530 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);} |
|
531 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);} |
|
532 |
|
533 \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} |
|
534 \end{tikzpicture} |
|
535 |
|
536 \end{textblock} |
|
537 \end{column} |
|
538 \end{columns} |
|
539 |
|
540 |
|
541 \begin{textblock}{3}(12,3.6) |
|
542 \onslide<4->{ |
|
543 \begin{tikzpicture} |
|
544 \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h}; |
|
545 \end{tikzpicture}} |
|
546 \end{textblock} |
|
547 |
|
548 \end{frame}} |
|
549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
550 |
|
551 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
552 \mode<presentation>{ |
|
553 \begin{frame}[c] |
|
554 \frametitle{Mars Pathfinder Mission 1997} |
|
555 |
|
556 \begin{center} |
|
557 \includegraphics[scale=0.15]{marspath1.png} |
|
558 \includegraphics[scale=0.16]{marspath3.png} |
|
559 \includegraphics[scale=0.3]{marsrover.png} |
|
560 \end{center} |
|
561 |
|
562 \begin{itemize} |
|
563 \item despite NASA's famous testing procedure, the lander crashed frequently on Mars |
|
564 \item problem was an algorithm not used in the OS |
|
565 \end{itemize} |
|
566 |
|
567 \end{frame}} |
|
568 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
569 |
|
570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
571 \mode<presentation>{ |
|
572 \begin{frame}[c] |
|
573 \frametitle{Priority Inheritance Protocol} |
|
574 |
|
575 \begin{itemize} |
|
576 \item \ldots a scheduling algorithm that is widely used in real-time operating systems |
|
577 \item has been ``proved'' correct by hand in a paper in 1983 |
|
578 \item \ldots but the first algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause |
|
579 |
|
580 \item we specified the algorithm and then proved that the specification makes |
|
581 ``sense'' |
|
582 \item we implemented our specification in C on top of PINTOS (used for teaching at Stanford) |
|
583 \item our implementation was much more efficient than their reference implementation |
|
584 \end{itemize} |
|
585 |
|
586 \end{frame}} |
|
587 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
588 |
|
589 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
590 \mode<presentation>{ |
|
591 \begin{frame}[c] |
|
592 \frametitle{Regular Expression Matching} |
|
593 \tiny |
|
594 |
|
595 \begin{tabular}{@ {\hspace{-6mm}}cc} |
|
596 \begin{tikzpicture}[y=.1cm, x=.15cm] |
|
597 %axis |
|
598 \draw (0,0) -- coordinate (x axis mid) (30,0); |
|
599 \draw (0,0) -- coordinate (y axis mid) (0,30); |
|
600 %ticks |
|
601 \foreach \x in {0,5,...,30} |
|
602 \draw (\x,1pt) -- (\x,-3pt) |
|
603 node[anchor=north] {\x}; |
|
604 \foreach \y in {0,5,...,30} |
|
605 \draw (1pt,\y) -- (-3pt,\y) |
|
606 node[anchor=east] {\y}; |
|
607 %labels |
|
608 \node[below=0.3cm] at (x axis mid) {\bl{a}s}; |
|
609 \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; |
|
610 |
|
611 %plots |
|
612 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
613 file {re-python.data}; |
|
614 \only<1->{ |
|
615 \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] |
|
616 file {re1.data};} |
|
617 \only<1->{ |
|
618 \draw[color=green] plot[mark=square*, mark options={fill=white} ] |
|
619 file {re2.data};} |
|
620 |
|
621 %legend |
|
622 \begin{scope}[shift={(4,20)}] |
|
623 \draw[color=blue] (0,0) -- |
|
624 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
625 node[right]{\footnotesize Python}; |
|
626 \only<1->{\draw[yshift=6mm, color=red] (0,0) -- |
|
627 plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
628 node[right]{\footnotesize Scala V1};} |
|
629 \only<1->{ |
|
630 \draw[yshift=12mm, color=green] (0,0) -- |
|
631 plot[mark=square*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
632 node[right]{\footnotesize Scala V2 with simplifications};} |
|
633 \end{scope} |
|
634 \end{tikzpicture} & |
|
635 |
|
636 \begin{tikzpicture}[y=.35cm, x=.00045cm] |
|
637 %axis |
|
638 \draw (0,0) -- coordinate (x axis mid) (10000,0); |
|
639 \draw (0,0) -- coordinate (y axis mid) (0,6); |
|
640 %ticks |
|
641 \foreach \x in {0,2000,...,10000} |
|
642 \draw (\x,1pt) -- (\x,-3pt) |
|
643 node[anchor=north] {\x}; |
|
644 \foreach \y in {0,1,...,6} |
|
645 \draw (1pt,\y) -- (-3pt,\y) |
|
646 node[anchor=east] {\y}; |
|
647 %labels |
|
648 \node[below=0.3cm] at (x axis mid) {\bl{a}s}; |
|
649 \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; |
|
650 |
|
651 %plots |
|
652 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
653 file {re-internal.data}; |
|
654 \only<1->{ |
|
655 \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] |
|
656 file {re3.data};} |
|
657 |
|
658 %legend |
|
659 \begin{scope}[shift={(2000,4)}] |
|
660 \draw[color=blue] (0,0) -- |
|
661 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
662 node[right]{\footnotesize Scala Internal}; |
|
663 \only<1->{ |
|
664 \draw[yshift=6mm, color=red] (0,0) -- |
|
665 plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
666 node[right]{\footnotesize Scala V3};} |
|
667 \end{scope} |
|
668 \end{tikzpicture} |
|
669 \end{tabular}\bigskip\pause |
|
670 \normalsize |
|
671 \begin{itemize} |
|
672 \item I needed a proof in order to make sure my program is correct |
|
673 \end{itemize}\pause |
|
674 |
|
675 \begin{center} |
|
676 \bl{End Digression.\\ (Our small proof is 0.0005\% of the OS-proof.)} |
|
677 \end{center} |
|
678 |
|
679 \end{frame}} |
|
680 |
|
681 |
|
682 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
683 |
|
684 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
685 \mode<presentation>{ |
|
686 \begin{frame}[c] |
|
687 \frametitle{One More Thing} |
|
688 |
|
689 \begin{itemize} |
|
690 \item I arrived at King's last year |
|
691 \item Maxime Crochemore told me about a string algorithm (suffix sorting) that appeared at a |
|
692 conference in 2007 (ICALP) |
|
693 \item ``horribly incomprehensible'', no implementation, but claims to be the best \bl{$O(n + k)$} algorithm\bigskip\pause |
|
694 |
|
695 \item Jian Jiang found 1 error and 1 superfluous step in this algorithm |
|
696 \item he received 88\% for the project and won the prize for the best 7CCSMPRJ project in the department |
|
697 \item no proof \ldots{} yet |
|
698 \end{itemize} |
|
699 |
|
700 \end{frame}} |
|
701 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
702 |
|
703 |
|
704 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
705 \mode<presentation>{ |
|
706 \begin{frame}[c] |
|
707 \frametitle{Trusted Third Party} |
|
708 |
|
709 Simple protocol for establishing a secure connection via a mutually |
|
710 trusted 3rd party (server): |
|
711 |
|
712 \begin{center} |
|
713 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
714 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\ |
|
715 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
716 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\ |
|
717 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\ |
|
718 \end{tabular} |
|
719 \end{center} |
|
720 |
|
721 \end{frame}} |
|
722 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
723 |
|
724 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
725 \mode<presentation>{ |
|
726 \begin{frame}[c] |
|
727 \frametitle{Encrypted Messages} |
|
728 |
|
729 \begin{itemize} |
|
730 \item Alice sends a message \bl{$m$} |
|
731 \begin{center} |
|
732 \bl{Alice says $m$} |
|
733 \end{center}\medskip\pause |
|
734 |
|
735 \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$}) |
|
736 \begin{center} |
|
737 \bl{Alice says $\{m\}_K$} |
|
738 \end{center}\medskip\pause |
|
739 |
|
740 \item Decryption of Alice's message\smallskip |
|
741 \begin{center} |
|
742 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
743 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
744 \end{center} |
|
745 \end{itemize} |
|
746 |
|
747 \end{frame}} |
|
748 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
749 |
|
750 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
751 \mode<presentation>{ |
|
752 \begin{frame}[c] |
|
753 \frametitle{Encryption} |
|
754 |
|
755 \begin{itemize} |
|
756 \item Encryption of a message\smallskip |
|
757 \begin{center} |
|
758 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
|
759 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
760 \end{center} |
|
761 \end{itemize} |
|
762 |
|
763 \end{frame}} |
|
764 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
765 |
|
766 |
|
767 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
768 \mode<presentation>{ |
|
769 \begin{frame}[c] |
|
770 \frametitle{Trusted Third Party} |
|
771 |
|
772 \begin{itemize} |
|
773 \item Alice calls Sam for a key to communicate with Bob |
|
774 \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared) |
|
775 \item Alice sends the message encrypted with the key and the second key it recieved |
|
776 \end{itemize}\bigskip |
|
777 |
|
778 \begin{center} |
|
779 \bl{\begin{tabular}{lcl} |
|
780 $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\ |
|
781 $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
782 $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\ |
|
783 $A$ sends $B$ &:& $\{m\}_{K_{AB}}$ |
|
784 \end{tabular}} |
|
785 \end{center} |
|
786 |
|
787 \end{frame}} |
|
788 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
789 |
|
790 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
791 \mode<presentation>{ |
|
792 \begin{frame}[c] |
|
793 \frametitle{Sending Rule} |
|
794 |
|
795 |
|
796 \bl{\begin{center} |
|
797 \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F} |
|
798 {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}} |
|
799 \end{center}}\bigskip\pause |
|
800 |
|
801 \bl{$P \,\text{sends}\, Q : F \dn$}\\ |
|
802 \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$} |
|
803 |
|
804 \end{frame}} |
|
805 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
806 |
|
807 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
808 \mode<presentation>{ |
|
809 \begin{frame}[c] |
|
810 \frametitle{Trusted Third Party} |
|
811 |
|
812 \begin{center} |
|
813 \bl{\begin{tabular}{l} |
|
814 $A$ sends $S$ : $\textit{Connect}(A,B)$\\ |
|
815 \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ |
|
816 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
|
817 \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\ |
|
818 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
819 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
|
820 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
|
821 \end{tabular}} |
|
822 \end{center}\bigskip\pause |
|
823 |
|
824 |
|
825 \bl{$\Gamma \vdash B \,\text{says} \, m$}? |
|
826 \end{frame}} |
|
827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
828 |
|
829 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
830 \mode<presentation>{ |
|
831 \begin{frame}[c] |
|
832 \frametitle{Challenge-Response Protocol} |
|
833 |
|
834 \begin{itemize} |
|
835 \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip |
|
836 \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip |
|
837 \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip |
|
838 \item if \bl{$E$} receives \bl{$\{N\}_K$} from \bl{$T$}, it starts engine |
|
839 \end{itemize} |
|
840 |
|
841 \end{frame}} |
|
842 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
843 |
|
844 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
845 \mode<presentation>{ |
|
846 \begin{frame}[c] |
|
847 \frametitle{Challenge-Response Protocol} |
|
848 |
|
849 \begin{center} |
|
850 \bl{\begin{tabular}{l} |
|
851 $E \;\text{says}\; N$\hfill(start)\\ |
|
852 $E \;\text{sends}\; T : N$\hfill(challenge)\\ |
|
853 $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\ |
|
854 \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\ |
|
855 $T \;\text{says}\; K$\hfill(key)\\ |
|
856 $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\ |
|
857 $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\ |
|
858 \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\ |
|
859 \end{tabular}} |
|
860 \end{center}\bigskip |
|
861 |
|
862 \bl{$\Gamma \vdash \text{start\_engine}(T)$}? |
|
863 \end{frame}} |
|
864 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
865 |
|
866 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
867 \mode<presentation>{ |
|
868 \begin{frame}[c] |
|
869 \frametitle{Exchange of a Fresh Key} |
|
870 |
|
871 \bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key |
|
872 |
|
873 \begin{itemize} |
|
874 \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip |
|
875 \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$} |
|
876 \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$} |
|
877 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
|
878 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$} |
|
879 \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$} |
|
880 \end{itemize}\bigskip |
|
881 |
|
882 Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$} |
|
883 \end{frame}} |
|
884 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
885 |
|
886 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
887 \mode<presentation>{ |
|
888 \begin{frame}[c] |
|
889 \frametitle{The Attack} |
|
890 |
|
891 An intruder \bl{$I$} convinces \bl{$A$} to accept the compromised key \bl{$K^{new}_{AB}$}\medskip |
|
892 |
|
893 \begin{minipage}{1.1\textwidth} |
|
894 \begin{itemize} |
|
895 \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$} |
|
896 \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$} |
|
897 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
|
898 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause |
|
899 \item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$} |
|
900 \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$} |
|
901 \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$} |
|
902 \item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$} |
|
903 \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause |
|
904 \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also |
|
905 \end{itemize} |
|
906 \end{minipage} |
|
907 |
|
908 \end{frame}} |
|
909 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
910 |
|
911 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
912 \mode<presentation>{ |
|
913 \begin{frame}[c] |
|
914 \frametitle{Another Challenge-Response} |
|
915 |
|
916 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
|
917 each other\bigskip |
|
918 |
|
919 \begin{itemize} |
|
920 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
|
921 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
|
922 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
|
923 \end{itemize} |
|
924 \end{frame}} |
|
925 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
926 |
|
927 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
928 \mode<presentation>{ |
|
929 \begin{frame}[c] |
|
930 \frametitle{Another Challenge-Response} |
|
931 |
|
932 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
|
933 each other\bigskip |
|
934 |
|
935 \begin{itemize} |
|
936 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
|
937 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
|
938 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
|
939 \end{itemize} |
|
940 \end{frame}} |
|
941 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
942 |
|
943 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
944 \mode<presentation>{ |
|
945 \begin{frame}[c] |
|
946 \frametitle{Another Challenge-Response} |
|
947 |
|
948 Unfortunately, an intruder \bl{$I$} can impersonate \bl{$B$}. |
|
949 |
|
950 \begin{center} |
|
951 \begin{tabular}{@{\hspace{-7mm}}c@{\hspace{1mm}}c@{}} |
|
952 \begin{tabular}{@{}l@{}} |
|
953 \onslide<1->{\bl{$A \,\text{sends}\, I : A, N_A$}}\\ |
|
954 \onslide<4->{\bl{$I \,\text{sends}\, A : \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ |
|
955 \onslide<5->{\bl{$A \,\text{sends}\, I : \{N_A\}_{K'_{AB}}$}}\\ |
|
956 \end{tabular} |
|
957 & |
|
958 \begin{tabular}{@{}l@{}} |
|
959 \onslide<2->{\bl{$I \,\text{sends}\, A : B, N_A$}}\\ |
|
960 \onslide<3->{\bl{$A \,\text{sends}\, I : \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ |
|
961 \onslide<6->{\bl{$I \,\text{sends}\, A : \{N_A\}_{K'_{AB}}$}}\\ |
|
962 \end{tabular} |
|
963 \end{tabular} |
|
964 \end{center} |
|
965 |
|
966 \end{frame}} |
|
967 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
968 |
|
969 |
|
970 \end{document} |
|
971 |
|
972 %%% Local Variables: |
|
973 %%% mode: latex |
|
974 %%% TeX-master: t |
|
975 %%% End: |
|
976 |