75 |
74 |
76 |
75 |
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
78 \mode<presentation>{ |
77 \mode<presentation>{ |
79 \begin{frame}[c] |
78 \begin{frame}[c] |
80 \frametitle{Revision: Proofs} |
79 \frametitle{\mbox{}\\[20mm]\huge Revision} |
81 |
|
82 \begin{center} |
|
83 \includegraphics[scale=0.4]{pics/river-stones.jpg} |
|
84 \end{center} |
|
85 |
|
86 \begin{textblock}{5}(11.7,5) |
|
87 goal |
|
88 \end{textblock} |
|
89 |
|
90 \begin{textblock}{5}(11.7,14) |
|
91 start |
|
92 \end{textblock} |
|
93 |
|
94 \begin{textblock}{5}(0,7) |
|
95 \begin{center} |
|
96 \bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm] |
|
97 \bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm] |
|
98 \bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}} |
|
99 \end{center} |
|
100 \end{textblock} |
|
101 |
80 |
102 \end{frame}} |
81 \end{frame}} |
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
104 |
83 |
105 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
106 \mode<presentation>{ |
85 \mode<presentation>{ |
107 \begin{frame}[c] |
86 \begin{frame}[c] |
108 \frametitle{Proof Example Proof} |
87 \frametitle{1st Lecture} |
109 |
88 |
110 \begin{center} |
89 |
111 \bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1} |
90 |
112 {\raisebox{2mm}{\text{\LARGE $?$}}}} |
91 |
113 \end{center} |
92 \end{frame}} |
114 |
93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
115 |
94 |
116 \end{frame}} |
95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
117 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
96 \begin{frame}[fragile,t] |
|
97 \frametitle{\begin{tabular}{c}2nd Lecture:\\ E-Voting\end{tabular}} |
|
98 |
|
99 \begin{itemize} |
|
100 \item Integrity |
|
101 \item Ballot Secrecy |
|
102 \item Voter Authentication |
|
103 \item Enfranchisement |
|
104 \item Availability |
|
105 \end{itemize} |
|
106 |
|
107 |
|
108 |
|
109 \end{frame} |
|
110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
111 |
|
112 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
113 \begin{frame}[fragile,t] |
|
114 \frametitle{\begin{tabular}{c}2nd Lecture:\\ E-Voting\end{tabular}} |
|
115 |
|
116 Online Banking vs.~E-Voting |
|
117 |
|
118 \begin{itemize} |
|
119 \item online banking: if fraud occurred you try to identify who did what (somebody's account got zero)\bigskip |
|
120 \item e-voting: some parts can be done electronically, but not the actual voting (final year project: online voting) |
|
121 \end{itemize} |
|
122 |
|
123 |
|
124 |
|
125 \end{frame} |
|
126 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
127 |
|
128 |
|
129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
130 \tikzset{alt/.code args={<#1>#2#3#4}{% |
|
131 \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path |
|
132 }} |
|
133 |
|
134 \mode<presentation>{ |
|
135 \begin{frame}[t] |
|
136 \frametitle{\begin{tabular}{c}3rd Lecture:\\ Buffer Overflow Attacks\end{tabular}} |
|
137 |
|
138 \begin{itemize} |
|
139 \item the problem arises from the way C/C++ organises its function calls\\[-8mm]\mbox{} |
|
140 \end{itemize} |
|
141 |
|
142 \begin{center} |
|
143 \begin{tikzpicture}[scale=1] |
|
144 %\draw[black!10,step=2mm] (0,0) grid (9,4); |
|
145 %\draw[black!10,thick,step=10mm] (0,0) grid (9,4); |
|
146 |
|
147 \node at (0.5,4.5) {\small\begin{tabular}{l}main\\[-2mm] prog.\end{tabular}}; |
|
148 \draw[line width=0mm, white, alt=<2->{fill=red}{fill=blue}] (0,2.5) rectangle (1,3.8); |
|
149 \draw[line width=0mm, white, alt=<9->{fill=red}{fill=blue}] (0,0.2) rectangle (1,0.5); |
|
150 \draw[line width=1mm, alt=<3->{fill=yellow}{fill=blue}] (0,2.0) rectangle (1,2.5); |
|
151 \draw[line width=1mm, alt=<6->{fill=red}{fill=blue}] (0,1.0) rectangle (1,2.0); |
|
152 \draw[line width=1mm, alt=<7->{fill=yellow}{fill=blue}] (0,0.5) rectangle (1,1.0); |
|
153 \draw[line width=1mm] (0,0) -- (0,4); |
|
154 \draw[line width=1mm] (1,0) -- (1,4); |
|
155 |
|
156 \node at (3.5,3.5) {\small\begin{tabular}{l}fact(n)\end{tabular}}; |
|
157 \draw[line width=1mm, alt=<{4-5,8}>{fill=red}{fill=blue}] (3,1.0) rectangle (4,3.0); |
|
158 |
|
159 \onslide<3-4>{\draw[->, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {n=4} (3,3);} |
|
160 \onslide<5>{\draw[<-, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {res=24} (3,1);} |
|
161 |
|
162 \onslide<7-8>{\draw[->, line width=1mm,red] (1,0.8) to node [above,sloped,midway] {n=3} (3,3);} |
|
163 \onslide<9>{\draw[<-, line width=1mm,red] (1,0.8) to node [above,sloped,midway] {res=6} (3,1);} |
|
164 |
|
165 |
|
166 \node at (7.75,3.9) {\small\begin{tabular}{l}stack\end{tabular}}; |
|
167 \draw[line width=1mm] (7,3.5) -- (7,0.5) -- (8.5,0.5) -- (8.5,3.5); |
|
168 |
|
169 \onslide<3,4,7,8>{ |
|
170 \node at (7.75, 0.8) {ret}; |
|
171 \draw[line width=1mm] (7,1.1) -- (8.5,1.1); |
|
172 } |
|
173 \onslide<3>{ |
|
174 \node at (7.75, 1.4) {4}; |
|
175 \draw[line width=1mm] (7,1.7) -- (8.5,1.7); |
|
176 } |
|
177 \onslide<7>{ |
|
178 \node at (7.75, 1.4) {3}; |
|
179 \draw[line width=1mm] (7,1.7) -- (8.5,1.7); |
|
180 } |
|
181 |
|
182 |
|
183 |
|
184 |
|
185 \end{tikzpicture} |
|
186 \end{center} |
|
187 |
|
188 \end{frame}} |
|
189 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
190 \mode<presentation>{ |
|
191 \begin{frame}[t] |
|
192 |
|
193 \begin{center} |
|
194 \begin{tikzpicture}[scale=1] |
|
195 %\draw[black!10,step=2mm] (0,0) grid (9,4); |
|
196 %\draw[black!10,thick,step=10mm] (0,0) grid (9,4); |
|
197 |
|
198 \node at (0.5,4.5) {\small\begin{tabular}{l}main\\[-2mm] prog.\end{tabular}}; |
|
199 \draw[line width=0mm, white, alt=<2->{fill=red}{fill=blue}] (0,2.5) rectangle (1,3.8); |
|
200 \draw[line width=1mm, white, fill=blue] (0,1.0) rectangle (1,2.0); |
|
201 \draw[line width=1mm, alt=<3->{fill=yellow}{fill=blue}] (0,2.0) rectangle (1,2.5); |
|
202 \draw[line width=1mm] (0,0) -- (0,4); |
|
203 \draw[line width=1mm] (1,0) -- (1,4); |
|
204 |
|
205 \node at (3.5,3.5) {\small\begin{tabular}{l}fact(n)\end{tabular}}; |
|
206 \draw[line width=0mm, alt=<{4-}>{red, fill=red}{blue, fill=blue}] (3,2.8) rectangle (4,3.0); |
|
207 \draw[line width=0mm, alt=<{5-}>{red, fill=red}{blue, fill=blue}] (3,2.8) rectangle (4,2.0); |
|
208 \draw[line width=0mm, alt=<{7-}>{red, fill=red}{blue, fill=blue}] (3,2.0) rectangle (4,1.0); |
|
209 \draw[line width=1mm] (3,1.0) rectangle (4,3.0); |
|
210 |
|
211 \onslide<3->{\draw[->, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {n=4} (3,3);} |
|
212 \onslide<5->{\draw[<-, line width=2mm,red] (4,2) to node [above,sloped,midway] |
|
213 {\begin{tabular}{l}user\\[-1mm] input\end{tabular}} (6,2);} |
|
214 \onslide<8->{\draw[<-, line width=1mm,red] (1,-2) to (3,1);} |
|
215 |
|
216 \node at (7.75,3.9) {\small\begin{tabular}{l}stack\end{tabular}}; |
|
217 \draw[line width=1mm] (7,3.5) -- (7,0.5) -- (8.5,0.5) -- (8.5,3.5); |
|
218 |
|
219 \onslide<3->{ |
|
220 \draw[line width=1mm,alt=<6->{fill=red}{fill=white}] (7,0.5) rectangle (8.5,1.1); |
|
221 \node at (7.75, 0.8) {\alt<6->{@a\#}{ret}}; |
|
222 \draw[line width=1mm,alt=<6->{fill=red}{fill=white}] (7,1.1) rectangle (8.5,1.7); |
|
223 \node at (7.75, 1.4) {\alt<6->{!?w;}4}; |
|
224 } |
|
225 |
|
226 \onslide<4->{ |
|
227 \draw[line width=1mm,fill=red] (7,1.7) rectangle (8.5,3.0); |
|
228 \node[white] at (7.75, 2.4) {buffer}; |
|
229 } |
|
230 |
|
231 \end{tikzpicture} |
|
232 \end{center} |
|
233 |
|
234 \end{frame}} |
|
235 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
236 |
|
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
238 \mode<presentation>{ |
|
239 \begin{frame}[t] |
|
240 \frametitle{\begin{tabular}{c}3rd Lecture:\\ Unix Access Control\end{tabular}} |
|
241 |
|
242 \begin{itemize} |
|
243 \item privileges are specified by file access permissions (``everything is a file'') |
|
244 \end{itemize}\medskip |
|
245 |
|
246 \begin{center} |
|
247 \begin{tikzpicture}[scale=1] |
|
248 |
|
249 \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); |
|
250 \draw (4.7,1) node {Internet}; |
|
251 \draw (-2.7,1.7) node {\footnotesize Application}; |
|
252 \draw (0.6,1.7) node {\footnotesize Interface}; |
|
253 \draw (0.6,-0.4) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] process\end{tabular}}; |
|
254 \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}}; |
|
255 |
|
256 \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2); |
|
257 |
|
258 \draw[white] (1.7,1) node (X) {}; |
|
259 \draw[white] (3.7,1) node (Y) {}; |
|
260 \draw[red, <->, line width = 2mm] (X) -- (Y); |
|
261 |
|
262 \draw[red, <->, line width = 1mm] (-0.6,1) -- (-1.6,1); |
|
263 \end{tikzpicture} |
|
264 \end{center} |
|
265 |
|
266 \begin{itemize} |
|
267 \item the idea is make the attack surface smaller and |
|
268 mitigate the consequences of an attack |
|
269 \end{itemize} |
|
270 |
|
271 \end{frame}} |
|
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
273 |
|
274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
275 \begin{frame}[fragile,t] |
|
276 \frametitle{\begin{tabular}{c}3rd Lecture:\\ Unix Access Control\end{tabular}} |
|
277 |
|
278 \begin{itemize} |
|
279 \item when a file with setuid is executed, the resulting process will assume the |
|
280 UID given to the owner of the file |
|
281 \end{itemize} |
|
282 |
|
283 \small\tt |
|
284 \begin{center} |
|
285 \begin{verbatim} |
|
286 $ ls -ld . * */* |
|
287 drwxr-xr-x 1 ping staff 32768 Apr 2 2010 . |
|
288 -rw----r-- 1 ping students 31359 Jul 24 2011 manual.txt |
|
289 -r--rw--w- 1 bob students 4359 Jul 24 2011 report.txt |
|
290 -rwsr--r-x 1 bob students 141359 Jun 1 2013 microedit |
|
291 dr--r-xr-x 1 bob staff 32768 Jul 23 2011 src |
|
292 -rw-r--r-- 1 bob staff 81359 Feb 28 2012 src/code.c |
|
293 -r--rw---- 1 emma students 959 Jan 23 2012 src/code.h |
|
294 \end{verbatim} |
|
295 \end{center} |
|
296 |
|
297 |
|
298 \end{frame} |
|
299 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
300 |
|
301 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
302 \begin{frame}[fragile,t] |
|
303 \frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}} |
|
304 |
|
305 Bell-LaPadula access model: |
|
306 |
|
307 \begin{itemize} |
|
308 \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if |
|
309 \bl{$P$}'s security level is at least as high as \bl{$O$}'s. |
|
310 \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if |
|
311 \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip |
|
312 |
|
313 \item Meta-Rule: All principals in a system should have a sufficiently high security level |
|
314 in order to access an object. |
|
315 \end{itemize}\bigskip |
|
316 |
|
317 \end{frame} |
|
318 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
319 |
|
320 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
321 \begin{frame}[fragile,t] |
|
322 \frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}} |
|
323 |
|
324 Biba (data integrity) |
|
325 |
|
326 \begin{itemize} |
|
327 \item Biba: {\bf `no read down'} - {\bf `no write up'} |
|
328 \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if |
|
329 \bl{$P$}'s security level is lower or equal than \bl{$O$}'s. |
|
330 \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if |
|
331 \bl{$O$}'s security level is lower or equal than \bl{$P$}'s. |
|
332 \end{itemize} |
|
333 |
|
334 \end{frame} |
|
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
336 |
|
337 |
|
338 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
339 \begin{frame}[fragile,t] |
|
340 \frametitle{\begin{tabular}{c}4th Lecture:\\ Protocols\end{tabular}} |
|
341 |
|
342 A mutual authentication protocol |
|
343 |
|
344 \begin{center} |
|
345 \begin{tabular}{ll} |
|
346 \bl{$A \rightarrow B$:} & \bl{$N_a$}\\ |
|
347 \bl{$B \rightarrow A$:} & \bl{$\{N_a, N_b\}_{K_{ab}}$}\\ |
|
348 \bl{$A \rightarrow B$:} & \bl{$N_b$}\\ |
|
349 \end{tabular} |
|
350 \end{center} |
|
351 |
|
352 |
|
353 \end{frame} |
|
354 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
355 |
|
356 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
357 \begin{frame}[fragile,t] |
|
358 \frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}} |
|
359 |
|
360 |
|
361 \begin{itemize} |
|
362 \item formulas |
|
363 \item judgements |
|
364 \end{itemize}\pause |
|
365 |
|
366 \begin{center} |
|
367 \begin{tikzpicture}[scale=1] |
|
368 |
|
369 \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); |
|
370 \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; |
|
371 \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; |
|
372 \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; |
|
373 |
|
374 \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); |
|
375 \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); |
|
376 \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); |
|
377 |
|
378 \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}}; |
|
379 |
|
380 \end{tikzpicture} |
|
381 \end{center} |
|
382 |
|
383 |
|
384 \end{frame} |
|
385 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
386 |
|
387 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
388 \begin{frame}[fragile,t] |
|
389 \frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}} |
|
390 |
|
391 \begin{center} |
|
392 \begin{tikzpicture}[scale=1] |
|
393 |
|
394 \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}}; |
|
395 \onslide<1->{ |
|
396 \draw (-1,-0.3) node (X) {}; |
|
397 \draw (-2.0,-2.0) node (Y) {}; |
|
398 \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}}; |
|
399 \draw[red, ->, line width = 2mm] (Y) -- (X); |
|
400 |
|
401 \draw (1.2,-0.1) node (X1) {}; |
|
402 \draw (2.8,-0.1) node (Y1) {}; |
|
403 \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}}; |
|
404 \draw[red, ->, line width = 2mm] (Y1) -- (X1); |
|
405 |
|
406 \draw (-0.1,0.1) node (X2) {}; |
|
407 \draw (0.5,1.5) node (Y2) {}; |
|
408 \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}}; |
|
409 \draw[red, ->, line width = 2mm] (Y2) -- (X2);} |
|
410 |
|
411 \end{tikzpicture} |
|
412 \end{center} |
|
413 |
|
414 |
|
415 \end{frame} |
|
416 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
417 |
118 |
418 |
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
419 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
120 \mode<presentation>{ |
420 \mode<presentation>{ |
121 \begin{frame}[c] |
421 \begin{frame}[c] |
122 \frametitle{Proof Example Proof} |
422 \frametitle{\begin{tabular}{c}5th Lecture:\\ Inference Rules\end{tabular}} |
123 |
423 |
124 \begin{tabular}{@{\hspace{-6mm}}l} |
424 |
125 \begin{minipage}{1.1\textwidth} |
425 \begin{center} |
126 We have (by axiom) |
426 \begin{tikzpicture}[scale=1] |
127 |
427 |
128 \begin{center} |
428 \draw (0.0,0.0) node |
129 \begin{tabular}{@{}ll@{}} |
429 {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}}; |
130 (1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$} |
430 |
131 \end{tabular} |
431 \draw (-0.1,-0.7) node (X) {}; |
132 \end{center} |
432 \draw (-0.1,-1.9) node (Y) {}; |
133 |
433 \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}}; |
134 From (1) we get |
434 \draw[red, ->, line width = 2mm] (Y) -- (X); |
135 |
435 |
136 \begin{center} |
436 \draw (-1,0.6) node (X2) {}; |
137 \begin{tabular}{@{}ll@{}} |
437 \draw (0.0,1.6) node (Y2) {}; |
138 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\ |
438 \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}}; |
139 (3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\ |
439 \draw[red, ->, line width = 2mm] (Y2) -- (X2); |
140 \end{tabular} |
440 \draw (1,0.6) node (X3) {}; |
141 \end{center} |
441 \draw (0.0,1.6) node (Y3) {}; |
142 |
442 \draw[red, ->, line width = 2mm] (Y3) -- (X3); |
143 From (3) and (2) we get |
443 \end{tikzpicture} |
144 |
444 \end{center} |
145 \begin{center} |
445 |
146 \begin{tabular}{@{}ll@{}} |
446 |
147 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$} |
447 \end{frame}} |
148 \end{tabular} |
448 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
149 \end{center} |
449 |
150 |
450 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
151 Done. |
451 \mode<presentation>{ |
152 \end{minipage} |
452 \begin{frame}[c] |
153 \end{tabular} |
453 \frametitle{\begin{tabular}{c}6th Lecture:\\ Privacy\end{tabular}} |
154 |
454 |
155 \end{frame}} |
455 |
156 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
456 |
|
457 |
|
458 \end{frame}} |
|
459 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
460 |
157 |
461 |
158 |
462 |
159 \end{document} |
463 \end{document} |
160 |
464 |
161 %%% Local Variables: |
465 %%% Local Variables: |