|
1 \documentclass[dvipsnames,14pt,t]{beamer} |
|
2 \usepackage{proof} |
|
3 \usepackage{beamerthemeplaincu} |
|
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 \newcommand{\isaliteral}[1]{} |
|
31 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
|
32 |
|
33 |
|
34 % Isabelle characters |
|
35 \renewcommand{\isacharunderscore}{\_} |
|
36 \renewcommand{\isacharbar}{\isamath{\mid}} |
|
37 \renewcommand{\isasymiota}{} |
|
38 \renewcommand{\isacharbraceleft}{\{} |
|
39 \renewcommand{\isacharbraceright}{\}} |
|
40 \renewcommand{\isacharless}{$\langle$} |
|
41 \renewcommand{\isachargreater}{$\rangle$} |
|
42 \renewcommand{\isasymsharp}{\isamath{\#}} |
|
43 \renewcommand{\isasymdots}{\isamath{...}} |
|
44 \renewcommand{\isasymbullet}{\act} |
|
45 |
|
46 |
|
47 |
|
48 \definecolor{javared}{rgb}{0.6,0,0} % for strings |
|
49 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments |
|
50 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords |
|
51 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc |
|
52 |
|
53 \lstset{language=Java, |
|
54 basicstyle=\ttfamily, |
|
55 keywordstyle=\color{javapurple}\bfseries, |
|
56 stringstyle=\color{javagreen}, |
|
57 commentstyle=\color{javagreen}, |
|
58 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
59 numbers=left, |
|
60 numberstyle=\tiny\color{black}, |
|
61 stepnumber=1, |
|
62 numbersep=10pt, |
|
63 tabsize=2, |
|
64 showspaces=false, |
|
65 showstringspaces=false} |
|
66 |
|
67 \lstdefinelanguage{scala}{ |
|
68 morekeywords={abstract,case,catch,class,def,% |
|
69 do,else,extends,false,final,finally,% |
|
70 for,if,implicit,import,match,mixin,% |
|
71 new,null,object,override,package,% |
|
72 private,protected,requires,return,sealed,% |
|
73 super,this,throw,trait,true,try,% |
|
74 type,val,var,while,with,yield}, |
|
75 otherkeywords={=>,<-,<\%,<:,>:,\#,@}, |
|
76 sensitive=true, |
|
77 morecomment=[l]{//}, |
|
78 morecomment=[n]{/*}{*/}, |
|
79 morestring=[b]", |
|
80 morestring=[b]', |
|
81 morestring=[b]""" |
|
82 } |
|
83 |
|
84 \lstset{language=Scala, |
|
85 basicstyle=\ttfamily, |
|
86 keywordstyle=\color{javapurple}\bfseries, |
|
87 stringstyle=\color{javagreen}, |
|
88 commentstyle=\color{javagreen}, |
|
89 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
90 numbers=left, |
|
91 numberstyle=\tiny\color{black}, |
|
92 stepnumber=1, |
|
93 numbersep=10pt, |
|
94 tabsize=2, |
|
95 showspaces=false, |
|
96 showstringspaces=false} |
|
97 |
|
98 % beamer stuff |
|
99 \renewcommand{\slidecaption}{APP 07, King's College London, 19 November 2013} |
|
100 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
101 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
|
102 |
|
103 |
|
104 |
|
105 \begin{document} |
|
106 |
|
107 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
108 \mode<presentation>{ |
|
109 \begin{frame}<1>[t] |
|
110 \frametitle{% |
|
111 \begin{tabular}{@ {}c@ {}} |
|
112 \\ |
|
113 \LARGE Access Control and \\[-3mm] |
|
114 \LARGE Privacy Policies (7)\\[-6mm] |
|
115 \end{tabular}}\bigskip\bigskip\bigskip |
|
116 |
|
117 %\begin{center} |
|
118 %\includegraphics[scale=1.3]{pics/barrier.jpg} |
|
119 %\end{center} |
|
120 |
|
121 \normalsize |
|
122 \begin{center} |
|
123 \begin{tabular}{ll} |
|
124 Email: & christian.urban at kcl.ac.uk\\ |
|
125 Office: & N7.07 (North Wing, Bush House)\\ |
|
126 Slides: & KEATS (also homework is there)\\ |
|
127 \end{tabular} |
|
128 \end{center} |
|
129 |
|
130 |
|
131 \end{frame}} |
|
132 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
133 |
|
134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
135 \mode<presentation>{ |
|
136 \begin{frame}[c] |
|
137 \frametitle{} |
|
138 |
|
139 Recall the following scenario: |
|
140 |
|
141 \begin{itemize} |
|
142 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file}} |
|
143 should be deleted, then this file must be deleted. |
|
144 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
|
145 \textcolor{blue}{\isa{file}} should be deleted (delegation). |
|
146 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file}}. |
|
147 \end{itemize}\bigskip |
|
148 |
|
149 \small |
|
150 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
151 \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}{}},\\ |
|
152 \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}}},\\ |
|
153 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\ |
|
154 \end{tabular}}\medskip |
|
155 |
|
156 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}} |
|
157 \end{frame}} |
|
158 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
159 |
|
160 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
161 \mode<presentation>{ |
|
162 \begin{frame}[c] |
|
163 \frametitle{\begin{tabular}{@ {\hspace{-2mm}}c@ {}}The Access Control Problem\end{tabular}} |
|
164 |
|
165 |
|
166 \begin{center} |
|
167 \begin{tikzpicture}[scale=1] |
|
168 |
|
169 \draw[line width=1mm] (-.3, -0.5) rectangle (1.5,2); |
|
170 \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; |
|
171 \draw (4.2,1) node {\begin{tabular}{l}provable/\\not provable\end{tabular}}; |
|
172 \draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}}; |
|
173 |
|
174 \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); |
|
175 \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); |
|
176 \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); |
|
177 |
|
178 \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\boldmath\bl{$\Gamma$})\end{tabular}}; |
|
179 |
|
180 \end{tikzpicture} |
|
181 \end{center} |
|
182 |
|
183 \end{frame}} |
|
184 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
186 \mode<presentation>{ |
|
187 \begin{frame}[c] |
|
188 |
|
189 \begin{itemize} |
|
190 \item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or |
|
191 can make a ``statement'' \bl{$F$}\bigskip\pause |
|
192 |
|
193 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ |
|
194 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip |
|
195 |
|
196 \begin{center} |
|
197 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} |
|
198 \end{center} |
|
199 |
|
200 |
|
201 \end{itemize} |
|
202 |
|
203 \end{frame}} |
|
204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
205 |
|
206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
207 \mode<presentation>{ |
|
208 \begin{frame}[c] |
|
209 \frametitle{Security Levels} |
|
210 \small |
|
211 |
|
212 \begin{itemize} |
|
213 \item Top secret (\bl{$T\!S$}) |
|
214 \item Secret (\bl{$S$}) |
|
215 \item Public (\bl{$P$}) |
|
216 \end{itemize} |
|
217 |
|
218 \begin{center} |
|
219 \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause |
|
220 \end{center} |
|
221 |
|
222 \begin{itemize} |
|
223 \item Bob has a clearance for ``secret'' |
|
224 \item Bob can read documents that are public or sectret, but not top secret |
|
225 \end{itemize} |
|
226 |
|
227 \end{frame}} |
|
228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
229 % |
|
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
231 \mode<presentation>{ |
|
232 \begin{frame}[c] |
|
233 \frametitle{Reading a File} |
|
234 |
|
235 \bl{\begin{center} |
|
236 \begin{tabular}{c} |
|
237 \begin{tabular}{@ {}l@ {}} |
|
238 \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ |
|
239 \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\ |
|
240 Bob says Permitted $($File, read$)$\only<2->{\\} |
|
241 \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}% |
|
242 \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}% |
|
243 \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}% |
|
244 \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}% |
|
245 \end{tabular}\\ |
|
246 \hline |
|
247 Permitted $($File, read$)$ |
|
248 \end{tabular} |
|
249 \end{center}} |
|
250 |
|
251 \end{frame}} |
|
252 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
253 % |
|
254 |
|
255 |
|
256 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
257 \mode<presentation>{ |
|
258 \begin{frame}[c] |
|
259 \frametitle{Substitution Rule} |
|
260 \small |
|
261 |
|
262 \bl{\begin{center} |
|
263 \begin{tabular}{c} |
|
264 $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$ |
|
265 \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline |
|
266 $\Gamma \vdash slev(P) < slev(Q)$ |
|
267 \end{tabular} |
|
268 \end{center}}\bigskip\pause |
|
269 |
|
270 \begin{itemize} |
|
271 \item \bl{$slev($Bob$)$ $=$ $S$} |
|
272 \item \bl{$slev($File$)$ $=$ $P$} |
|
273 \item \bl{$slev(P) < slev(S)$} |
|
274 \end{itemize} |
|
275 |
|
276 \end{frame}} |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 % |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 \mode<presentation>{ |
|
281 \begin{frame}[c] |
|
282 \frametitle{Reading a File} |
|
283 |
|
284 \bl{\begin{center} |
|
285 \begin{tabular}{c} |
|
286 \begin{tabular}{@ {}l@ {}} |
|
287 $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ |
|
288 \hspace{3cm}Bob controls Permitted $($File, read$)$\\ |
|
289 Bob says Permitted $($File, read$)$\\ |
|
290 $slev($File$)$ $=$ $P$\\ |
|
291 $slev($Bob$)$ $=$ $T\!S$\\ |
|
292 \only<1>{\textcolor{red}{$?$}}% |
|
293 \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}% |
|
294 \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}% |
|
295 \end{tabular}\\ |
|
296 \hline |
|
297 Permitted $($File, read$)$ |
|
298 \end{tabular} |
|
299 \end{center}} |
|
300 |
|
301 \end{frame}} |
|
302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
303 % |
|
304 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
305 \mode<presentation>{ |
|
306 \begin{frame}[c] |
|
307 \frametitle{Transitivity Rule} |
|
308 \small |
|
309 |
|
310 \bl{\begin{center} |
|
311 \begin{tabular}{c} |
|
312 $\Gamma \vdash l_1 < l_2$ |
|
313 \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline |
|
314 $\Gamma \vdash l_1 < l_3$ |
|
315 \end{tabular} |
|
316 \end{center}}\bigskip |
|
317 |
|
318 \begin{itemize} |
|
319 \item \bl{$slev(P) < slev (S)$} |
|
320 \item \bl{$slev(S) < slev (T\!S)$} |
|
321 \item[] \bl{$slev(P) < slev (T\!S)$} |
|
322 \end{itemize} |
|
323 |
|
324 \end{frame}} |
|
325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
326 % |
|
327 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
328 \mode<presentation>{ |
|
329 \begin{frame}[c] |
|
330 \frametitle{Reading Files} |
|
331 |
|
332 \begin{itemize} |
|
333 \item Access policy for Bob for reading |
|
334 \end{itemize} |
|
335 |
|
336 \bl{\begin{center} |
|
337 \begin{tabular}{c} |
|
338 \begin{tabular}{@ {}l@ {}} |
|
339 $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ |
|
340 \hspace{3cm}Bob controls Permitted $(f$, read$)$\\ |
|
341 Bob says Permitted $($File, read$)$\\ |
|
342 $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\ |
|
343 $slev($Bob$)$ $=$ $T\!S$\\ |
|
344 $slev(P) < slev(S)$\\ |
|
345 $slev(S) < slev(T\!S)$ |
|
346 \end{tabular}\\ |
|
347 \hline |
|
348 Permitted $($File, read$)$ |
|
349 \end{tabular} |
|
350 \end{center}} |
|
351 |
|
352 \end{frame}} |
|
353 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
354 % |
|
355 |
|
356 |
|
357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
358 \mode<presentation>{ |
|
359 \begin{frame}[c] |
|
360 \frametitle{Writing Files} |
|
361 |
|
362 \begin{itemize} |
|
363 \item Access policy for Bob for {\bf writing} |
|
364 \end{itemize} |
|
365 |
|
366 \bl{\begin{center} |
|
367 \begin{tabular}{c} |
|
368 \begin{tabular}{@ {}l@ {}} |
|
369 $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ |
|
370 \hspace{3cm}Bob controls Permitted $(f$, write$)$\\ |
|
371 Bob says Permitted $($File, write$)$\\ |
|
372 $slev($File$)$ $=$ $T\!S$\\ |
|
373 $slev($Bob$)$ $=$ $S$\\ |
|
374 $slev(P) < slev(S)$\\ |
|
375 $slev(S) < slev(T\!S)$ |
|
376 \end{tabular}\\ |
|
377 \hline |
|
378 Permitted $($File, write$)$ |
|
379 \end{tabular} |
|
380 \end{center}} |
|
381 |
|
382 \end{frame}} |
|
383 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
384 % |
|
385 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
386 \mode<presentation>{ |
|
387 \begin{frame}[c] |
|
388 \frametitle{Encrypted Messages} |
|
389 |
|
390 \begin{itemize} |
|
391 \item Alice sends a message \bl{$m$} |
|
392 \begin{center} |
|
393 \bl{Alice says $m$} |
|
394 \end{center}\medskip\pause |
|
395 |
|
396 \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$}) |
|
397 \begin{center} |
|
398 \bl{Alice says $\{m\}_K$} |
|
399 \end{center}\medskip\pause |
|
400 |
|
401 \item Decryption of Alice's message\smallskip |
|
402 \begin{center} |
|
403 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
404 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
405 \end{center} |
|
406 \end{itemize} |
|
407 |
|
408 \end{frame}} |
|
409 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
410 |
|
411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
412 \mode<presentation>{ |
|
413 \begin{frame}[c] |
|
414 \frametitle{Encryption} |
|
415 |
|
416 \begin{itemize} |
|
417 \item Encryption of a message\smallskip |
|
418 \begin{center} |
|
419 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
|
420 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
421 \end{center} |
|
422 \end{itemize} |
|
423 |
|
424 \end{frame}} |
|
425 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
426 |
|
427 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
428 \mode<presentation>{ |
|
429 \begin{frame}[c] |
|
430 \frametitle{Trusted Third Party} |
|
431 |
|
432 Simple protocol for establishing a secure connection via a mutually |
|
433 trusted 3rd party (server): |
|
434 |
|
435 \begin{center} |
|
436 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
437 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\ |
|
438 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
439 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\ |
|
440 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\ |
|
441 \end{tabular} |
|
442 \end{center} |
|
443 |
|
444 \end{frame}} |
|
445 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
446 |
|
447 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
448 \mode<presentation>{ |
|
449 \begin{frame}[c] |
|
450 \frametitle{Sending Rule} |
|
451 |
|
452 \bl{\begin{center} |
|
453 \mbox{$\infer{\Gamma \vdash Q \;\text{says}\; F} |
|
454 {\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{sends}\; Q : F}$} |
|
455 \end{center}}\bigskip\pause |
|
456 |
|
457 \bl{$P \,\text{sends}\, Q : F \dn$}\\ |
|
458 \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$} |
|
459 |
|
460 \end{frame}} |
|
461 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
462 |
|
463 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
464 \mode<presentation>{ |
|
465 \begin{frame}[c] |
|
466 \frametitle{Trusted Third Party} |
|
467 |
|
468 \begin{center} |
|
469 \bl{\begin{tabular}{l} |
|
470 $A$ sends $S$ : $\text{Connect}(A,B)$\\ |
|
471 \bl{$S \,\text{says}\, (\text{Connect}(A,B) \Rightarrow$}\\ |
|
472 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
|
473 \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\ |
|
474 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
475 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
|
476 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
|
477 \end{tabular}} |
|
478 \end{center}\bigskip\pause |
|
479 |
|
480 |
|
481 \bl{$\Gamma \vdash B \,\text{says} \, m$}? |
|
482 \end{frame}} |
|
483 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
484 |
|
485 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
486 \mode<presentation>{ |
|
487 \begin{frame}[c] |
|
488 \frametitle{Public/Private Keys} |
|
489 |
|
490 \begin{itemize} |
|
491 \item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip |
|
492 \begin{center} |
|
493 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
494 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} & |
|
495 \Gamma \vdash K_{Bob}^{priv}}}} |
|
496 \end{center}\bigskip\pause |
|
497 |
|
498 \item this is {\bf not} a derived rule! |
|
499 \end{itemize} |
|
500 |
|
501 \end{frame}} |
|
502 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
503 |
|
504 |
|
505 % \begin{itemize} |
|
506 % \item Alice calls Sam for a key to communicate with Bob |
|
507 % \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared) |
|
508 % \item Alice sends the message encrypted with the key and the second key it recieved |
|
509 % \end{itemize}\bigskip |
|
510 |
|
511 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
512 \mode<presentation>{ |
|
513 \begin{frame}[c] |
|
514 \frametitle{Sending Rule} |
|
515 |
|
516 |
|
517 \bl{\begin{center} |
|
518 \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F} |
|
519 {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}} |
|
520 \end{center}}\bigskip\pause |
|
521 |
|
522 \bl{$P \,\text{sends}\, Q : F \dn$}\\ |
|
523 \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$} |
|
524 |
|
525 \end{frame}} |
|
526 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
527 |
|
528 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
529 \mode<presentation>{ |
|
530 \begin{frame}[c] |
|
531 \frametitle{Trusted Third Party} |
|
532 |
|
533 \begin{center} |
|
534 \bl{\begin{tabular}{l} |
|
535 $A$ sends $S$ : $\textit{Connect}(A,B)$\\ |
|
536 \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ |
|
537 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
|
538 \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\ |
|
539 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
540 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
|
541 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
|
542 \end{tabular}} |
|
543 \end{center}\bigskip\pause |
|
544 |
|
545 |
|
546 \bl{$\Gamma \vdash B \,\text{says} \, m$}? |
|
547 \end{frame}} |
|
548 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
549 |
|
550 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
551 \mode<presentation>{ |
|
552 \begin{frame}[c] |
|
553 \frametitle{Challenge-Response Protocol} |
|
554 |
|
555 \begin{itemize} |
|
556 \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip |
|
557 \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip |
|
558 \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip |
|
559 \item if \bl{$E$} receives \bl{$\{N\}_K$} from \bl{$T$}, it starts engine |
|
560 \end{itemize} |
|
561 |
|
562 \end{frame}} |
|
563 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
564 |
|
565 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
566 \mode<presentation>{ |
|
567 \begin{frame}[c] |
|
568 \frametitle{Challenge-Response Protocol} |
|
569 |
|
570 \begin{center} |
|
571 \bl{\begin{tabular}{l} |
|
572 $E \;\text{says}\; N$\hfill(start)\\ |
|
573 $E \;\text{sends}\; T : N$\hfill(challenge)\\ |
|
574 $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\ |
|
575 \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\ |
|
576 $T \;\text{says}\; K$\hfill(key)\\ |
|
577 $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\ |
|
578 $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\ |
|
579 \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\ |
|
580 \end{tabular}} |
|
581 \end{center}\bigskip |
|
582 |
|
583 \bl{$\Gamma \vdash \text{start\_engine}(T)$}? |
|
584 \end{frame}} |
|
585 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
586 |
|
587 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
588 \mode<presentation>{ |
|
589 \begin{frame}[c] |
|
590 \frametitle{Exchange of a Fresh Key} |
|
591 |
|
592 \bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key |
|
593 |
|
594 \begin{itemize} |
|
595 \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip |
|
596 \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$} |
|
597 \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$} |
|
598 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
|
599 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$} |
|
600 \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$} |
|
601 \end{itemize}\bigskip |
|
602 |
|
603 Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$} |
|
604 \end{frame}} |
|
605 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
606 |
|
607 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
608 \mode<presentation>{ |
|
609 \begin{frame}[c] |
|
610 \frametitle{The Attack} |
|
611 |
|
612 An intruder \bl{$I$} convinces \bl{$A$} to accept the compromised key \bl{$K^{new}_{AB}$}\medskip |
|
613 |
|
614 \begin{minipage}{1.1\textwidth} |
|
615 \begin{itemize} |
|
616 \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$} |
|
617 \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$} |
|
618 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
|
619 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause |
|
620 \item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$} |
|
621 \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$} |
|
622 \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$} |
|
623 \item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$} |
|
624 \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause |
|
625 \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also |
|
626 \end{itemize} |
|
627 \end{minipage} |
|
628 |
|
629 \end{frame}} |
|
630 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
631 |
|
632 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
633 \mode<presentation>{ |
|
634 \begin{frame}[c] |
|
635 |
|
636 A Man-in-the-middle attack in real life: |
|
637 |
|
638 \begin{itemize} |
|
639 \item the card only says yes or no to the terminal if the PIN is correct |
|
640 \item trick the card in thinking transaction is verified by signature |
|
641 \item trick the terminal in thinking the transaction was verified by PIN |
|
642 \end{itemize} |
|
643 |
|
644 \begin{minipage}{1.1\textwidth} |
|
645 \begin{center} |
|
646 \mbox{}\hspace{-6mm}\includegraphics[scale=0.5]{pics/chip-attack.png} |
|
647 \includegraphics[scale=0.3]{pics/chipnpinflaw.png} |
|
648 \end{center} |
|
649 \end{minipage} |
|
650 |
|
651 \end{frame}} |
|
652 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
653 |
|
654 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
655 \mode<presentation>{ |
|
656 \begin{frame}[c] |
|
657 \frametitle{Problems with EMV} |
|
658 |
|
659 \begin{itemize} |
|
660 \item it is a wrapper for many protocols |
|
661 \item specification by consensus (resulted unmanageable complexity) |
|
662 \item its specification is 700 pages in English plus 2000+ pages for testing, additionally some |
|
663 further parts are secret |
|
664 \item other attacks have been found |
|
665 |
|
666 \item one solution might be to require always online verification of the PIN with the bank |
|
667 \end{itemize} |
|
668 |
|
669 \end{frame}} |
|
670 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
671 |
|
672 |
|
673 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
674 \mode<presentation>{ |
|
675 \begin{frame}[c] |
|
676 \frametitle{\begin{tabular}{c}Problems with WEP (Wifi)\end{tabular}} |
|
677 |
|
678 \begin{itemize} |
|
679 \item a standard ratified in 1999 |
|
680 \item the protocol was designed by a committee not including cryptographers |
|
681 \item it used the RC4 encryption algorithm which is a stream cipher requiring a unique nonce |
|
682 \item WEP did not allocate enough bits for the nonce |
|
683 \item for authenticating packets it used CRC checksum which can be easily broken |
|
684 \item the network password was used to directly encrypt packages (instead of a key negotiation protocol)\bigskip |
|
685 \item encryption was turned off by default |
|
686 \end{itemize} |
|
687 |
|
688 \end{frame}} |
|
689 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
690 |
|
691 |
|
692 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
693 \mode<presentation>{ |
|
694 \begin{frame}[c] |
|
695 \frametitle{Protocols are Difficult} |
|
696 |
|
697 \begin{itemize} |
|
698 \item even the systems designed by experts regularly fail\medskip |
|
699 \item try to make everything explicit (you need to authenticate all data you might rely on)\medskip |
|
700 \item the one who can fix a system should also be liable for the losses\medskip |
|
701 \item cryptography is often not {\bf the} answer\bigskip\bigskip |
|
702 \end{itemize} |
|
703 |
|
704 logic is one way protocols are studied in academia |
|
705 (you can use computers to search for attacks) |
|
706 |
|
707 \end{frame}} |
|
708 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
709 |
|
710 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
711 \mode<presentation>{ |
|
712 \begin{frame}[c] |
|
713 \frametitle{Public-Key Infrastructure} |
|
714 |
|
715 \begin{itemize} |
|
716 \item the idea is to have a certificate authority (CA) |
|
717 \item you go to the CA to identify yourself |
|
718 \item CA: ``I, the CA, have verified that public key \bl{$P^{pub}_{Bob}$} belongs to Bob''\bigskip |
|
719 \item CA must be trusted by everybody |
|
720 \item What happens if CA issues a false certificate? Who pays in case of loss? (VeriSign |
|
721 explicitly limits liability to \$100.) |
|
722 \end{itemize} |
|
723 |
|
724 \end{frame}} |
|
725 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
726 |
|
727 |
|
728 |
|
729 |
|
730 |
|
731 |
|
732 |
|
733 \end{document} |
|
734 |
|
735 %%% Local Variables: |
|
736 %%% mode: latex |
|
737 %%% TeX-master: t |
|
738 %%% End: |
|
739 |