|
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 07, King's College London, 13 November 2012} |
|
93 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
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 (7)\\[-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{Judgements} |
|
128 |
|
129 \begin{center} |
|
130 \begin{tikzpicture}[scale=1] |
|
131 |
|
132 \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}}; |
|
133 \onslide<2->{ |
|
134 \draw (-1,-0.3) node (X) {}; |
|
135 \draw (-2.0,-2.0) node (Y) {}; |
|
136 \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}}; |
|
137 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
138 |
|
139 \draw (1.2,-0.1) node (X1) {}; |
|
140 \draw (2.8,-0.1) node (Y1) {}; |
|
141 \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}}; |
|
142 \draw[red, ->, line width = 2mm] (Y1) -- (X1); |
|
143 |
|
144 \draw (-0.1,0.1) node (X2) {}; |
|
145 \draw (0.5,1.5) node (Y2) {}; |
|
146 \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}}; |
|
147 \draw[red, ->, line width = 2mm] (Y2) -- (X2);} |
|
148 |
|
149 \end{tikzpicture} |
|
150 \end{center} |
|
151 |
|
152 \pause\pause |
|
153 \footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic) |
|
154 \end{frame}} |
|
155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
156 |
|
157 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
158 \mode<presentation>{ |
|
159 \begin{frame}[c] |
|
160 \frametitle{Inference Rules} |
|
161 |
|
162 \begin{center} |
|
163 \begin{tikzpicture}[scale=1] |
|
164 |
|
165 \draw (0.0,0.0) node |
|
166 {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}}; |
|
167 |
|
168 \draw (-0.1,-0.7) node (X) {}; |
|
169 \draw (-0.1,-1.9) node (Y) {}; |
|
170 \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}}; |
|
171 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
172 |
|
173 \draw (-1,0.6) node (X2) {}; |
|
174 \draw (0.0,1.6) node (Y2) {}; |
|
175 \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}}; |
|
176 \draw[red, ->, line width = 2mm] (Y2) -- (X2); |
|
177 \draw (1,0.6) node (X3) {}; |
|
178 \draw (0.0,1.6) node (Y3) {}; |
|
179 \draw[red, ->, line width = 2mm] (Y3) -- (X3); |
|
180 \end{tikzpicture} |
|
181 \end{center} |
|
182 |
|
183 \end{frame}} |
|
184 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
185 |
|
186 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
187 \mode<presentation>{ |
|
188 \begin{frame}[c] |
|
189 \frametitle{Trusted Third Party} |
|
190 |
|
191 Simple protocol for establishing a secure connection via a mutually |
|
192 trusted 3rd party (server): |
|
193 |
|
194 \begin{center} |
|
195 \begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
196 Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\ |
|
197 Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\ |
|
198 Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\ |
|
199 Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\ |
|
200 \end{tabular} |
|
201 \end{center} |
|
202 |
|
203 \end{frame}} |
|
204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
205 |
|
206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
207 \mode<presentation>{ |
|
208 \begin{frame}[c] |
|
209 \frametitle{Encrypted Messages} |
|
210 |
|
211 \begin{itemize} |
|
212 \item Alice sends a message \bl{$m$} |
|
213 \begin{center} |
|
214 \bl{Alice says $m$} |
|
215 \end{center}\medskip\pause |
|
216 |
|
217 \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$}) |
|
218 \begin{center} |
|
219 \bl{Alice says $\{m\}_K$} |
|
220 \end{center}\medskip\pause |
|
221 |
|
222 \item Decryption of Alice's message\smallskip |
|
223 \begin{center} |
|
224 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m} |
|
225 {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
226 \end{center} |
|
227 \end{itemize} |
|
228 |
|
229 \end{frame}} |
|
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
231 |
|
232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
233 \mode<presentation>{ |
|
234 \begin{frame}[c] |
|
235 \frametitle{Encryption} |
|
236 |
|
237 \begin{itemize} |
|
238 \item Encryption of a message\smallskip |
|
239 \begin{center} |
|
240 \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K} |
|
241 {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}} |
|
242 \end{center} |
|
243 \end{itemize} |
|
244 |
|
245 \end{frame}} |
|
246 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
247 |
|
248 |
|
249 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
250 \mode<presentation>{ |
|
251 \begin{frame}[c] |
|
252 \frametitle{Trusted Third Party} |
|
253 |
|
254 \begin{itemize} |
|
255 \item Alice calls Sam for a key to communicate with Bob |
|
256 \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared) |
|
257 \item Alice sends the message encrypted with the key and the second key it recieved |
|
258 \end{itemize}\bigskip |
|
259 |
|
260 \begin{center} |
|
261 \bl{\begin{tabular}{lcl} |
|
262 $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\ |
|
263 $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
264 $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\ |
|
265 $A$ sends $B$ &:& $\{m\}_{K_{AB}}$ |
|
266 \end{tabular}} |
|
267 \end{center} |
|
268 |
|
269 \end{frame}} |
|
270 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
271 |
|
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
273 \mode<presentation>{ |
|
274 \begin{frame}[c] |
|
275 \frametitle{Sending Rule} |
|
276 |
|
277 \bl{\begin{center} |
|
278 \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F} |
|
279 {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}} |
|
280 \end{center}}\bigskip\pause |
|
281 |
|
282 \bl{$P \,\text{sends}\, Q : F \dn$}\\ |
|
283 \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$} |
|
284 |
|
285 \end{frame}} |
|
286 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
287 |
|
288 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
289 \mode<presentation>{ |
|
290 \begin{frame}[c] |
|
291 \frametitle{Trusted Third Party} |
|
292 |
|
293 \begin{center} |
|
294 \bl{\begin{tabular}{l} |
|
295 $A$ sends $S$ : $\textit{Connect}(A,B)$\\ |
|
296 \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ |
|
297 \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge |
|
298 \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\ |
|
299 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\ |
|
300 $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\ |
|
301 $A$ sends $B$ : $\{m\}_{K_{AB}}$ |
|
302 \end{tabular}} |
|
303 \end{center}\bigskip\pause |
|
304 |
|
305 |
|
306 \bl{$\Gamma \vdash B \,\text{says} \, m$}? |
|
307 \end{frame}} |
|
308 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
309 |
|
310 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
311 \mode<presentation>{ |
|
312 \begin{frame}[c] |
|
313 \frametitle{Challenge-Response Protocol} |
|
314 |
|
315 \begin{itemize} |
|
316 \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip |
|
317 \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip |
|
318 \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip |
|
319 \item if \bl{$E$} receives \bl{$\{N\}_K$} from \bl{$T$} then starts engine |
|
320 \end{itemize} |
|
321 |
|
322 \end{frame}} |
|
323 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
324 |
|
325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
326 \mode<presentation>{ |
|
327 \begin{frame}[c] |
|
328 \frametitle{Challenge-Response Protokol} |
|
329 |
|
330 \begin{center} |
|
331 \bl{\begin{tabular}{l} |
|
332 $E \;\text{says}\; N$\hfill(start)\\ |
|
333 $E \;\text{sends}\; T : N$\hfill(challenge)\\ |
|
334 $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\ |
|
335 \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\ |
|
336 $T \;\text{says}\; K$\hfill(key)\\ |
|
337 $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\ |
|
338 $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\ |
|
339 \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\ |
|
340 \end{tabular}} |
|
341 \end{center}\bigskip |
|
342 |
|
343 \bl{$\Gamma \vdash \text{start\_engine}(T)$}? |
|
344 \end{frame}} |
|
345 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
346 |
|
347 \end{document} |
|
348 |
|
349 %%% Local Variables: |
|
350 %%% mode: latex |
|
351 %%% TeX-master: t |
|
352 %%% End: |
|
353 |