1 \documentclass[dvipsnames,14pt,t]{beamer} |
1 \documentclass[dvipsnames,14pt,t]{beamer} |
2 \usepackage{proof} |
2 \usepackage{../slides} |
3 \usepackage{beamerthemeplaincu} |
3 \usepackage{../graphics} |
4 \usepackage{fontenc} |
4 \usepackage{../langs} |
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} |
5 \usetikzlibrary{arrows} |
15 \usetikzlibrary{positioning} |
6 \usetikzlibrary{shapes} |
16 \usetikzlibrary{calc} |
7 |
17 \usepackage{graphicx} |
8 \setmonofont[Scale=.88]{Consolas} |
18 \setmonofont{Consolas} |
9 \newfontfamily{\consolas}{Consolas} |
19 |
10 |
20 \isabellestyle{rm} |
11 \hfuzz=220pt |
21 \renewcommand{\isastyle}{\rm}% |
|
22 \renewcommand{\isastyleminor}{\rm}% |
|
23 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}% |
|
24 \renewcommand{\isatagproof}{} |
|
25 \renewcommand{\endisatagproof}{} |
|
26 \renewcommand{\isamarkupcmt}[1]{#1} |
|
27 |
|
28 % Isabelle characters |
|
29 \renewcommand{\isacharunderscore}{\_} |
|
30 \renewcommand{\isacharbar}{\isamath{\mid}} |
|
31 \renewcommand{\isasymiota}{} |
|
32 \renewcommand{\isacharbraceleft}{\{} |
|
33 \renewcommand{\isacharbraceright}{\}} |
|
34 \renewcommand{\isacharless}{$\langle$} |
|
35 \renewcommand{\isachargreater}{$\rangle$} |
|
36 \renewcommand{\isasymsharp}{\isamath{\#}} |
|
37 \renewcommand{\isasymdots}{\isamath{...}} |
|
38 \renewcommand{\isasymbullet}{\act} |
|
39 \newcommand{\isaliteral}[1]{} |
|
40 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
|
41 |
|
42 \definecolor{javared}{rgb}{0.6,0,0} % for strings |
|
43 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments |
|
44 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords |
|
45 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc |
|
46 |
|
47 \makeatletter |
|
48 \lst@CCPutMacro\lst@ProcessOther {"2D}{\lst@ttfamily{-{}}{-{}}} |
|
49 \@empty\z@\@empty |
|
50 \makeatother |
|
51 |
|
52 |
|
53 \lstdefinelanguage{scala}{ |
|
54 morekeywords={abstract,case,catch,class,def,% |
|
55 do,else,extends,false,final,finally,% |
|
56 for,if,implicit,import,match,mixin,% |
|
57 new,null,object,override,package,% |
|
58 private,protected,requires,return,sealed,% |
|
59 super,this,throw,trait,true,try,% |
|
60 type,val,var,while,with,yield}, |
|
61 otherkeywords={=>,<-,<\%,<:,>:,\#,@}, |
|
62 sensitive=true, |
|
63 morecomment=[l]{//}, |
|
64 morecomment=[n]{/*}{*/}, |
|
65 morestring=[b]", |
|
66 morestring=[b]', |
|
67 morestring=[b]""" |
|
68 } |
|
69 |
|
70 \lstdefinelanguage{while}{ |
|
71 morekeywords={while, if, then. else, read, write}, |
|
72 otherkeywords={=>,<-,<\%,<:,>:,\#,@}, |
|
73 sensitive=true, |
|
74 morecomment=[l]{//}, |
|
75 morecomment=[n]{/*}{*/}, |
|
76 morestring=[b]", |
|
77 morestring=[b]', |
|
78 morestring=[b]""" |
|
79 } |
|
80 |
|
81 |
|
82 \lstset{language=Scala, |
|
83 basicstyle=\ttfamily, |
|
84 keywordstyle=\color{javapurple}\bfseries, |
|
85 stringstyle=\color{javagreen}, |
|
86 commentstyle=\color{javagreen}, |
|
87 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
88 numbers=left, |
|
89 numberstyle=\tiny\color{black}, |
|
90 stepnumber=1, |
|
91 numbersep=10pt, |
|
92 tabsize=2, |
|
93 showspaces=false, |
|
94 showstringspaces=false} |
|
95 |
|
96 |
12 |
97 % beamer stuff |
13 % beamer stuff |
98 \renewcommand{\slidecaption}{APP 05, King's College London, 29 October 2013} |
14 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
99 |
15 \renewcommand{\slidecaption}{APP 05, King's College London} |
100 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
16 |
|
17 |
101 \begin{document} |
18 \begin{document} |
102 |
19 |
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
104 \mode<presentation>{ |
21 \begin{frame}[t] |
105 \begin{frame}<1>[t] |
|
106 \frametitle{% |
22 \frametitle{% |
107 \begin{tabular}{@ {}c@ {}} |
23 \begin{tabular}{@ {}c@ {}} |
108 \\ |
24 \\ |
109 \LARGE Access Control and \\[-3mm] |
25 \LARGE Access Control and \\[-3mm] |
110 \LARGE Privacy Policies (5)\\[-6mm] |
26 \LARGE Privacy Policies (5)\\[-6mm] |
111 \end{tabular}}\bigskip\bigskip\bigskip |
27 \end{tabular}}\bigskip\bigskip\bigskip |
112 |
28 |
113 %\begin{center} |
29 \normalsize |
114 %\includegraphics[scale=1.3]{pics/barrier.jpg} |
|
115 %\end{center} |
|
116 |
|
117 \normalsize |
|
118 \begin{center} |
30 \begin{center} |
119 \begin{tabular}{ll} |
31 \begin{tabular}{ll} |
120 Email: & christian.urban at kcl.ac.uk\\ |
32 Email: & christian.urban at kcl.ac.uk\\ |
121 Office: & S1.27 (1st floor Strand Building)\\ |
33 Office: & S1.27 (1st floor Strand Building)\\ |
122 Slides: & KEATS (also homework is there)\\ |
34 Slides: & KEATS (also homework is there)\\ |
123 \end{tabular} |
35 \end{tabular} |
124 \end{center} |
36 \end{center} |
125 |
37 |
126 |
38 \end{frame} |
127 \end{frame}} |
39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
128 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
40 |
129 |
41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
130 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
131 \mode<presentation>{ |
|
132 \begin{frame}[t] |
|
133 \frametitle{Last Week} |
|
134 |
|
135 \mbox{} |
|
136 |
|
137 \begin{tabular}{l} |
|
138 {\Large \bl{$A\;\rightarrow\; B : \ldots$}}\\ |
|
139 \onslide<1->{\Large \bl{$B\;\rightarrow\; A : \ldots$}}\\ |
|
140 \onslide<1->{\Large \;\;\;\;\;\bl{$:$}}\bigskip |
|
141 \end{tabular} |
|
142 |
|
143 \begin{itemize} |
|
144 \item by convention \bl{$A$}, \bl{$B$} are named principals \bl{Alice\ldots}\\ |
|
145 but most likely they are programs |
|
146 \item indicates one ``protocol run'', or session, which specifies an |
|
147 order in the communication |
|
148 \item there can be several sessions in parallel (think of wifi routers) |
|
149 \item nonces (randomly generated numbers) used only once |
|
150 \end{itemize} |
|
151 |
|
152 \end{frame}} |
|
153 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
154 |
|
155 |
|
156 |
|
157 |
|
158 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
159 \mode<presentation>{ |
|
160 \begin{frame}[c] |
|
161 \frametitle{Cryptographic Protocol Failures} |
|
162 |
|
163 Ross Anderson and Roger Needham wrote:\bigskip |
|
164 |
|
165 \begin{quote} |
|
166 \textcolor{gray}{ |
|
167 A lot of the recorded frauds were the result of this kind of blunder, or from |
|
168 management negligence pure and simple.} However, there have been a |
|
169 significant number of cases where the designers protected the right things, |
|
170 used cryptographic algorithms which were not broken, and yet found that their |
|
171 systems were still successfully attacked. |
|
172 \end{quote} |
|
173 |
|
174 |
|
175 \end{frame}} |
|
176 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
177 |
|
178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
179 \mode<presentation>{ |
|
180 \begin{frame}[c] |
42 \begin{frame}[c] |
181 \frametitle{Protocols} |
43 \frametitle{Protocols} |
182 |
44 |
183 Examples where ``over-the-air'' protocols are used |
45 Some examples where ``over-the-air'' protocols are used: |
184 |
46 |
185 \begin{itemize} |
47 \begin{itemize} |
186 \item wifi |
48 \item wifi |
187 \item card readers (you cannot trust the terminals) |
49 \item card readers (you cannot trust the terminals) |
188 \item RFI (passports) |
50 \item RFID (passports) |
189 \end{itemize} |
51 \item car transponders |
190 |
52 \end{itemize}\medskip\pause |
191 \end{frame}} |
53 |
|
54 The point is that we cannot control the network: |
|
55 An attacker can install a packet sniffer, inject packets, |
|
56 modify packets, replay messages. |
|
57 \end{frame} |
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
193 |
59 |
194 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
195 \mode<presentation>{ |
61 \begin{frame}[c] |
196 \begin{frame}[c] |
62 \frametitle{Keyless Car Transponders} |
197 |
63 |
198 \begin{center} |
64 \begin{center} |
199 \includegraphics[scale=0.5]{pics/dogs.jpg} |
65 \includegraphics[scale=0.1]{../pics/keyfob.jpg} |
200 \end{center} |
66 \quad |
201 |
67 \includegraphics[scale=0.27]{../pics/startstop.jpg} |
202 \end{frame}} |
68 \end{center} |
203 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
69 |
204 |
70 \begin{itemize} |
205 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
71 \item There are two security mechanisms: one remote central |
206 \mode<presentation>{ |
72 locking system and one passive RFID tag (engine immobiliser). |
207 \begin{frame}[c] |
73 \item How can I get in? How can thieves be kept out? |
208 \frametitle{\begin{tabular}{c}Chip-and-PIN\end{tabular}} |
74 How to avoid MITM attacks? |
209 |
75 \end{itemize}\medskip |
210 |
76 |
211 \begin{itemize} |
77 \footnotesize |
212 \item A ``tamperesitant'' terminal playing Tetris on |
78 \hfill Papers: Gone in 360 Seconds: Hijacking with Hitag2,\\ |
213 \textcolor{blue}{\href{http://www.youtube.com/watch?v=wWTzkD9M0sU}{youtube}}.\\ |
79 \hfill Dismantling Megamos Crypto: Wirelessly Lockpicking\\ |
214 \textcolor{lightgray}{\footnotesize(\url{http://www.youtube.com/watch?v=wWTzkD9M0sU})} |
80 \hfill a Vehicle Immobilizer |
215 \end{itemize} |
81 |
216 |
82 \end{frame} |
217 |
83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
218 \includegraphics[scale=0.2]{pics/tetris.jpg} |
84 |
219 |
85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
220 |
86 \begin{frame}[c] |
221 \end{frame}} |
87 \frametitle{HTTPS / GSM} |
222 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
88 |
223 |
89 \begin{center} |
224 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
90 \includegraphics[scale=0.25]{../pics/barclays.jpg} |
225 \mode<presentation>{ |
91 \quad |
226 \begin{frame}<1-3>[c] |
92 \includegraphics[scale=0.25]{../pics/phone-signal.jpg} |
227 \frametitle{Oyster Cards} |
93 \end{center} |
228 |
94 |
229 \includegraphics[scale=0.4]{pics/oysterc.jpg} |
95 \begin{itemize} |
230 |
96 \item I am sitting at Starbuck. How can I be sure I am |
231 \begin{itemize} |
97 really visiting Barclays? I have no control of the access |
232 \item good example of a bad protocol\\ (security by obscurity)\bigskip |
98 point. |
233 \item<3-> ``Breaching security on Oyster cards should not |
99 \item How can I achieve that a secret key is established |
234 allow unauthorised use for more than a day, as TfL promises to turn |
100 in order to encrypt my conversation? I have no control over |
235 off any cloned cards within 24 hours\ldots'' |
101 the access point. |
236 \end{itemize} |
102 \end{itemize} |
237 |
103 |
238 \only<2>{ |
104 \end{frame} |
239 \begin{textblock}{12}(0.5,0.5) |
105 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
240 \begin{tikzpicture} |
106 |
241 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
107 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
242 {\color{darkgray} |
108 \begin{frame}[c] |
243 \begin{minipage}{11cm}\raggedright\footnotesize |
109 \frametitle{Handshakes} |
244 {\bf Wirelessly Pickpocketing a Mifare Classic Card}\medskip |
110 |
245 |
111 \begin{itemize} |
246 The Mifare Classic is the most widely used contactless smartcard on the |
112 \item starting a TCP connection between a client and a server |
247 market. The stream cipher CRYPTO1 used by the Classic has recently been |
113 initiates the following three-way handshake protocol: |
248 reverse engineered and serious attacks have been proposed. The most serious |
114 \end{itemize} |
249 of them retrieves a secret key in under a second. In order to clone a card, |
115 |
250 previously proposed attacks require that the adversary either has access to |
116 \begin{columns}[t] |
251 an eavesdropped communication session or executes a message-by-message |
117 \begin{column}{5cm} |
252 man-in-the-middle attack between the victim and a legitimate |
118 \begin{minipage}[t]{4cm} |
253 reader. Although this is already disastrous from a cryptographic point of |
119 \begin{center} |
254 view, system integrators maintain that these attacks cannot be performed |
120 \raisebox{-2cm}{\includegraphics[scale=0.5]{../pics/handshake.png}} |
255 undetected.\smallskip |
121 \end{center} |
256 |
122 \end{minipage} |
257 This paper proposes four attacks that can be executed by an adversary having |
123 \end{column} |
258 only wireless access to just a card (and not to a legitimate reader). The |
124 \begin{column}{5cm} |
259 most serious of them recovers a secret key in less than a second on ordinary |
125 \begin{tabular}[t]{rl} |
260 hardware. Besides the cryptographic weaknesses, we exploit other weaknesses |
126 Alice: & Hello server!\\ |
261 in the protocol stack. A vulnerability in the computation of parity bits |
127 Server: & I heard you\\ |
262 allows an adversary to establish a side channel. Another vulnerability |
128 Alice: & Thanks |
263 regarding nested authentications provides enough plaintext for a speedy |
129 \end{tabular} |
264 known-plaintext attack. |
130 \end{column} |
265 \end{minipage}}; |
131 \end{columns}\pause |
266 \end{tikzpicture} |
132 |
267 \end{textblock}} |
133 \begin{center} |
268 |
134 \begin{tabular}{rl} |
269 \end{frame}} |
135 \bl{$A \rightarrow S$}: & \bl{SYN}\\ |
270 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
136 \bl{$S \rightarrow A$}: & \bl{SYN-ACK}\\ |
271 |
137 \bl{$A \rightarrow S$}: & \bl{ACK}\\ |
272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
138 \end{tabular} |
273 \mode<presentation>{ |
139 \end{center} |
274 \begin{frame}<1->[t] |
140 |
275 \frametitle{Another Example} |
141 \only<2>{ |
276 |
142 \begin{textblock}{3}(11,5) |
277 In an email from Ross Anderson\bigskip\small |
143 \begin{bubble}[3.2cm] |
278 |
144 SYNflood attacks:\medskip\\ |
|
145 \includegraphics[scale=0.4]{../pics/synflood.png} |
|
146 \end{bubble} |
|
147 \end{textblock}} |
|
148 |
|
149 \end{frame} |
|
150 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
151 |
|
152 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
153 \begin{frame}[c] |
|
154 \frametitle{Authentication} |
|
155 |
|
156 \begin{columns} |
|
157 \begin{column}{8cm} |
|
158 \begin{minipage}[t]{7.5cm} |
|
159 \begin{center} |
|
160 \raisebox{-2cm}{\includegraphics[scale=0.4]{../pics/dogs.jpg}} |
|
161 \end{center} |
|
162 \end{minipage} |
|
163 \end{column} |
|
164 \begin{column}{5cm} |
|
165 \begin{minipage}[t]{4.5cm} |
279 \begin{tabular}{l} |
166 \begin{tabular}{l} |
280 From: Ross Anderson <Ross.Anderson@cl.cam.ac.uk>\\ |
167 Knock Knock!\\ |
281 Sender: cl-security-research-bounces@lists.cam.ac.uk\\ |
168 Who's there?\\ |
282 To: cl-security-research@lists.cam.ac.uk\\ |
169 Alice.\\ |
283 Subject: Birmingham case\\ |
170 Alice who? |
284 Date: Tue, 13 Aug 2013 15:13:17 +0100\\ |
|
285 \end{tabular} |
171 \end{tabular} |
286 |
172 \end{minipage} |
287 |
173 \end{column} |
288 \only<2>{ |
174 \end{columns} |
289 \begin{textblock}{12}(0.5,0.5) |
175 |
290 \begin{tikzpicture} |
176 \end{frame} |
291 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
292 {\color{darkgray} |
178 |
293 \begin{minipage}{11cm}\raggedright\footnotesize |
179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
294 As you may know, Volkswagen got an injunction against the University of |
|
295 Birmingham suppressing the publication of the design of a weak cipher |
|
296 used in the remote key entry systems in its recent-model cars. The paper |
|
297 is being given today at Usenix, minus the cipher design.\medskip |
|
298 |
|
299 I've been contacted by Birmingham University's lawyers who seek to prove |
|
300 that the cipher can be easily obtained anyway. They are looking for a |
|
301 student who will download the firmware from any newish VW, disassemble |
|
302 it and look for the cipher. They'd prefer this to be done by a student |
|
303 rather than by a professor to emphasise how easy it is.\medskip |
|
304 |
|
305 Volkswagen's argument was that the Birmingham people had reversed a |
|
306 locksmithing tool produced by a company in Vietnam, and since their key |
|
307 fob chip is claimed to be tamper-resistant, this must have involved a |
|
308 corrupt insider at VW or at its supplier Thales. Birmingham's argument |
|
309 is that this is nonsense as the cipher is easy to get hold of. Their |
|
310 lawyers feel this argument would come better from an independent |
|
311 outsider.\medskip |
|
312 |
|
313 Let me know if you're interested in having a go, and I'll put you in |
|
314 touch |
|
315 |
|
316 Ross |
|
317 \end{minipage}}; |
|
318 \end{tikzpicture} |
|
319 \end{textblock}} |
|
320 |
|
321 \end{frame}} |
|
322 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
323 |
|
324 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
325 \mode<presentation>{ |
|
326 \begin{frame}[c] |
180 \begin{frame}[c] |
327 \frametitle{Authentication Protocols} |
181 \frametitle{Authentication Protocols} |
328 |
182 |
329 |
183 Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key |
330 Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip |
184 \bl{$K_{AB}$}\bigskip |
331 |
185 |
332 Passwords: |
186 Passwords: |
333 |
187 |
334 \begin{center} |
188 \begin{center} |
335 \bl{$B \rightarrow A: K_{AB}$} |
189 \bl{$A \rightarrow B: K_{AB}$} |
336 \end{center}\pause\bigskip |
190 \end{center}\pause\bigskip |
337 |
191 |
338 Problems: Eavesdropper can capture the secret and replay it; \bl{$A$} cannot confirm the |
192 Problems: Eavesdropper can capture the secret and replay it; |
339 identity of \bl{$B$} |
193 \bl{$B$} cannot confirm the identity of \bl{$A$} |
340 |
194 |
341 \end{frame}} |
195 \end{frame} |
342 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
196 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
343 |
197 |
344 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
198 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
345 \mode<presentation>{ |
|
346 \begin{frame}[c] |
199 \begin{frame}[c] |
347 \frametitle{Authentication Protocols} |
200 \frametitle{Authentication Protocols} |
348 |
201 |
349 Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip |
202 Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key |
|
203 \bl{$K_{AB}$}\bigskip |
350 |
204 |
351 Simple Challenge Response: |
205 Simple Challenge Response: |
352 |
206 |
353 \begin{center} |
207 \begin{center} |
354 \begin{tabular}{ll} |
208 \begin{tabular}{lll} |
355 \bl{$A \rightarrow B:$} & \bl{$N$}\\ |
209 \bl{$A \rightarrow B:$} & \bl{Hi I am A}\\ |
356 \bl{$B \rightarrow A:$} & \bl{$\{N\}_{K_{AB}}$}\\ |
210 \bl{$B \rightarrow A:$} & \bl{$N$} & (challenge)\\ |
|
211 \bl{$A \rightarrow B:$} & \bl{$\{N\}_{K_{AB}}$}\\ |
357 \end{tabular} |
212 \end{tabular} |
358 \end{center} |
213 \end{center}\pause |
359 |
214 |
360 |
215 \begin{itemize} |
361 \end{frame}} |
216 \item cannot replay since next time will be another challenge |
362 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
217 \item \bl{$B$} authenticates \bl{$A$}, but \bl{$A$} does not |
363 |
218 authenticate \bl{$B$} (be Eve in the middle, intercept |
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
219 messages from \bl{$A$} and ignore last) |
365 \mode<presentation>{ |
220 \end{itemize} |
|
221 |
|
222 \end{frame} |
|
223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
224 |
|
225 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
366 \begin{frame}[c] |
226 \begin{frame}[c] |
367 \frametitle{Authentication Protocols} |
227 \frametitle{Authentication Protocols} |
368 |
228 |
369 Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip |
229 Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip |
370 |
230 |
554 \end{quote} |
499 \end{quote} |
555 |
500 |
556 \end{frame}} |
501 \end{frame}} |
557 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
502 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
558 |
503 |
559 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
560 \mode<presentation>{ |
|
561 \begin{frame}[t] |
|
562 \frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}} |
|
563 |
|
564 \begin{itemize} |
|
565 \item Formulas |
|
566 |
|
567 \begin{center}\color{blue} |
|
568 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
|
569 \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ |
|
570 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ |
|
571 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ |
|
572 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ |
|
573 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F} & \textcolor{black}{implies}\\ |
|
574 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F} & \textcolor{black}{negation}\\ |
|
575 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \textcolor{black}{predicates}\\ |
|
576 & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} & |
|
577 \onslide<2->{\textcolor{black}{forall quantification}}\\ |
|
578 & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} & |
|
579 \onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm] |
|
580 \end{tabular} |
|
581 \end{center} |
|
582 |
|
583 \end{itemize} |
|
584 |
|
585 \begin{textblock}{12}(1,14) |
|
586 Terms \textcolor{blue}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{7C}{\isacharbar}}\ c\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}} |
|
587 \end{textblock} |
|
588 |
|
589 \end{frame}} |
|
590 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
591 % |
|
592 |
|
593 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
594 \mode<presentation>{ |
|
595 \begin{frame}[c] |
|
596 |
|
597 {\lstset{language=Scala}\fontsize{10}{12}\selectfont |
|
598 \texttt{\lstinputlisting{../programs/formulas.scala}}} |
|
599 |
|
600 \end{frame}} |
|
601 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
602 |
|
603 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
604 \mode<presentation>{ |
|
605 \begin{frame}[t] |
|
606 \frametitle{Judgements} |
|
607 |
|
608 \begin{center} |
|
609 \LARGE |
|
610 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}} |
|
611 \end{center} |
|
612 |
|
613 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause |
|
614 |
|
615 \begin{itemize} |
|
616 \item Example\mbox{}\\[-3mm] |
|
617 |
|
618 \only<2>{\begin{center}\tiny |
|
619 \textcolor{blue}{ |
|
620 \begin{tabular}{l} |
|
621 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
622 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
623 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
624 \end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} |
|
625 \end{center}} |
|
626 \only<3>{\small |
|
627 \textcolor{blue}{ |
|
628 \begin{center} |
|
629 \mbox{ |
|
630 \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
631 {\mbox{\begin{tabular}{@ {}l@ {}} |
|
632 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
633 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
634 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
635 \end{tabular}} |
|
636 } |
|
637 } |
|
638 \end{center} |
|
639 }} |
|
640 \only<4>{\small |
|
641 \textcolor{blue}{ |
|
642 \begin{center} |
|
643 \mbox{ |
|
644 \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}} |
|
645 {\mbox{\begin{tabular}{@ {}l@ {}} |
|
646 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\ |
|
647 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
648 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
649 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
650 \end{tabular}} |
|
651 } |
|
652 } |
|
653 \end{center} |
|
654 }} |
|
655 |
|
656 \end{itemize} |
|
657 |
|
658 \end{frame}} |
|
659 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
660 |
|
661 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
662 \mode<presentation>{ |
|
663 \begin{frame}[c] |
|
664 |
|
665 {\lstset{language=Scala}\fontsize{10}{12}\selectfont |
|
666 \texttt{\lstinputlisting{../programs/judgement.scala}}} |
|
667 |
|
668 \end{frame}} |
|
669 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
670 |
|
671 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
672 \mode<presentation>{ |
|
673 \begin{frame}[t] |
|
674 \frametitle{Inference Rules} |
|
675 |
|
676 \textcolor{blue}{ |
|
677 \begin{center} |
|
678 \Large |
|
679 \mbox{ |
|
680 \infer{\mbox{\isa{conclusion}}} |
|
681 {\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}} |
|
682 \end{center}} |
|
683 |
|
684 The conlusion and premises are judgements\bigskip\pause |
|
685 |
|
686 \begin{itemize} |
|
687 \item Examples |
|
688 \textcolor{blue}{ |
|
689 \begin{center} |
|
690 \mbox{ |
|
691 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
692 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} |
|
693 \end{center}}\pause |
|
694 |
|
695 \textcolor{blue}{ |
|
696 \begin{center} |
|
697 \mbox{ |
|
698 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
699 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
700 \hspace{10mm} |
|
701 \mbox{ |
|
702 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
703 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} |
|
704 \end{center}} |
|
705 \end{itemize} |
|
706 |
|
707 \end{frame}} |
|
708 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
709 % |
|
710 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
711 \mode<presentation>{ |
|
712 \begin{frame}[t] |
|
713 \frametitle{Implication} |
|
714 \Large |
|
715 |
|
716 \textcolor{blue}{ |
|
717 \begin{center} |
|
718 \mbox{ |
|
719 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
720 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}} |
|
721 \end{center}} |
|
722 |
|
723 \textcolor{blue}{ |
|
724 \begin{center} |
|
725 \mbox{ |
|
726 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
727 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
728 \end{center}} |
|
729 |
|
730 \end{frame}} |
|
731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
732 % |
|
733 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
734 \mode<presentation>{ |
|
735 \begin{frame}[t] |
|
736 \frametitle{Universal Quantification} |
|
737 \Large |
|
738 |
|
739 \textcolor{blue}{ |
|
740 \begin{center} |
|
741 \mbox{ |
|
742 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{$\isacharbrackleft$}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{$\isacharbrackright$}}}}} |
|
743 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}} |
|
744 \end{center}} |
|
745 |
|
746 \end{frame}} |
|
747 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
748 % |
|
749 |
|
750 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
751 \mode<presentation>{ |
|
752 \begin{frame}[t] |
|
753 \frametitle{Start Rules / Axioms} |
|
754 |
|
755 \normalsize |
|
756 \alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}} |
|
757 |
|
758 \textcolor{blue}{\Large |
|
759 \begin{center} |
|
760 \mbox{ |
|
761 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}} |
|
762 \end{center}}\bigskip\pause |
|
763 |
|
764 \normalsize |
|
765 Also written as: |
|
766 \textcolor{blue}{\Large |
|
767 \begin{center} |
|
768 \mbox{ |
|
769 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}} |
|
770 \end{center}}\pause |
|
771 |
|
772 \textcolor{blue}{\Large |
|
773 \begin{center} |
|
774 \mbox{ |
|
775 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}} |
|
776 \end{center}} |
|
777 |
|
778 \end{frame}} |
|
779 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
780 % |
|
781 |
|
782 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
783 \mode<presentation>{ |
|
784 \begin{frame}[t] |
|
785 \frametitle{} |
|
786 |
|
787 \begin{minipage}{1.1\textwidth} |
|
788 Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l} |
|
789 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
790 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
791 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
792 \end{tabular}} |
|
793 \end{minipage} |
|
794 |
|
795 \only<2>{ |
|
796 \begin{textblock}{12}(4,3)\footnotesize |
|
797 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm} |
|
798 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} |
|
799 \end{textblock}} |
|
800 |
|
801 \only<3->{ |
|
802 \begin{textblock}{12}(4,3)\footnotesize |
|
803 \mbox{\textcolor{blue}{ |
|
804 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
805 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm} |
|
806 \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
807 }} |
|
808 \end{textblock}} |
|
809 |
|
810 \only<4>{ |
|
811 \begin{textblock}{14}(0.5,6)\footnotesize |
|
812 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}} |
|
813 \end{textblock}} |
|
814 |
|
815 \only<5->{ |
|
816 \begin{textblock}{14}(0.5,6)\footnotesize |
|
817 \textcolor{blue}{ |
|
818 \infer{\mbox{\begin{tabular}{l}\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ |
|
819 \hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}} |
|
820 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}}}} |
|
821 \end{textblock}} |
|
822 |
|
823 \only<6->{ |
|
824 \begin{textblock}{14}(5,10)\footnotesize |
|
825 \textcolor{blue}{ |
|
826 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}} |
|
827 {\vdots & \hspace{30mm} \vdots}} |
|
828 \end{textblock}} |
|
829 |
|
830 \end{frame}} |
|
831 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
832 % |
|
833 |
|
834 |
|
835 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
836 \mode<presentation>{ |
|
837 \begin{frame}[t] |
|
838 \frametitle{Access Control} |
|
839 \Large |
|
840 |
|
841 \textcolor{blue}{ |
|
842 \begin{center} |
|
843 \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F} |
|
844 \end{center}}\bigskip |
|
845 |
|
846 \normalsize |
|
847 \begin{itemize} |
|
848 \item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted) |
|
849 \item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied) |
|
850 \end{itemize}\bigskip\pause |
|
851 |
|
852 \begin{minipage}{1.1\textwidth} |
|
853 \small |
|
854 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
855 \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
856 \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\ |
|
857 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\ |
|
858 \end{tabular}}\medskip |
|
859 |
|
860 \textcolor{blue}{ |
|
861 \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}} |
|
862 \end{minipage} |
|
863 \end{frame}} |
|
864 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
865 % |
|
866 |
|
867 |
|
868 |
|
869 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
870 \mode<presentation>{ |
|
871 \begin{frame}[c] |
|
872 \frametitle{The Access Control Problem} |
|
873 |
|
874 |
|
875 \begin{center} |
|
876 \begin{tikzpicture}[scale=1] |
|
877 |
|
878 \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); |
|
879 \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; |
|
880 \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; |
|
881 \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; |
|
882 |
|
883 \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); |
|
884 \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); |
|
885 \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); |
|
886 |
|
887 \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}}; |
|
888 |
|
889 \end{tikzpicture} |
|
890 \end{center} |
|
891 |
|
892 \end{frame}} |
|
893 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
894 |
|
895 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
896 \mode<presentation>{ |
|
897 \begin{frame}[c] |
|
898 \frametitle{Bad News} |
|
899 |
|
900 \begin{itemize} |
|
901 \item We introduced (roughly) first-order logic. \bigskip\pause |
|
902 |
|
903 \item Judgements |
|
904 \begin{center} |
|
905 \textcolor{blue} |
|
906 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} |
|
907 \end{center} |
|
908 |
|
909 are in general \alert{undecidable}.\pause\medskip\\ |
|
910 |
|
911 The problem is \alert{semi-decidable}. |
|
912 |
|
913 \end{itemize} |
|
914 |
|
915 |
|
916 \end{frame}} |
|
917 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
918 % |
|
919 |
|
920 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
921 \mode<presentation>{ |
|
922 \begin{frame}[t] |
|
923 \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}} |
|
924 |
|
925 \begin{itemize} |
|
926 \item[] |
|
927 |
|
928 \begin{center}\color{blue} |
|
929 \begin{tabular}[t]{rcl@ {\hspace{10mm}}l} |
|
930 \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\ |
|
931 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\ |
|
932 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\ |
|
933 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\ |
|
934 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\ |
|
935 & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\ |
|
936 & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ |
|
937 \end{tabular} |
|
938 \end{center}\medskip |
|
939 |
|
940 where \textcolor{blue}{\isa{P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ Alice{\isaliteral{2C}{\isacharcomma}}\ Bob{\isaliteral{2C}{\isacharcomma}}\ Christian{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}} (principals)\bigskip\pause |
|
941 |
|
942 \item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} |
|
943 \end{itemize} |
|
944 |
|
945 |
|
946 |
|
947 \end{frame}} |
|
948 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
949 % |
|
950 |
|
951 |
|
952 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
953 \mode<presentation>{ |
|
954 \begin{frame}[c] |
|
955 |
|
956 {\lstset{language=Scala}\fontsize{10}{12}\selectfont |
|
957 \texttt{\lstinputlisting{../programs/formulas1.scala}}} |
|
958 |
|
959 \end{frame}} |
|
960 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
961 |
|
962 |
|
963 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
964 \mode<presentation>{ |
|
965 \begin{frame}[t] |
|
966 \frametitle{Rules about Says} |
|
967 |
|
968 \textcolor{blue}{ |
|
969 \begin{center} |
|
970 \mbox{ |
|
971 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
972 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}} |
|
973 \end{center}} |
|
974 |
|
975 \textcolor{blue}{ |
|
976 \begin{center} |
|
977 \mbox{ |
|
978 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
979 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{10mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
980 \end{center}} |
|
981 |
|
982 \textcolor{blue}{ |
|
983 \begin{center} |
|
984 \mbox{ |
|
985 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
986 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}} |
|
987 \end{center}} |
|
988 |
|
989 \end{frame}} |
|
990 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
991 % |
|
992 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
993 \mode<presentation>{ |
|
994 \begin{frame}[c] |
|
995 \frametitle{} |
|
996 |
|
997 Consider the following scenario: |
|
998 |
|
999 \begin{itemize} |
|
1000 \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
|
1001 should be deleted, then this file must be deleted. |
|
1002 \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether |
|
1003 \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted. |
|
1004 \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}. |
|
1005 \end{itemize}\bigskip\pause |
|
1006 |
|
1007 \small |
|
1008 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
1009 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\ |
|
1010 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ |
|
1011 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ |
|
1012 \end{tabular}}\medskip\pause |
|
1013 |
|
1014 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
|
1015 \end{frame}} |
|
1016 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1017 % |
|
1018 |
|
1019 |
|
1020 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1021 \mode<presentation>{ |
|
1022 \begin{frame}[c] |
|
1023 \frametitle{} |
|
1024 |
|
1025 \textcolor{blue}{ |
|
1026 \begin{center} |
|
1027 \mbox{ |
|
1028 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1029 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip |
|
1030 \mbox{ |
|
1031 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}} |
|
1032 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{5mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}} |
|
1033 \end{center}}\bigskip |
|
1034 |
|
1035 \small |
|
1036 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l} |
|
1037 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\ |
|
1038 \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\ |
|
1039 \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\ |
|
1040 \end{tabular}}\medskip |
|
1041 |
|
1042 \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} |
|
1043 \end{frame}} |
|
1044 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1045 % |
|
1046 |
|
1047 |
|
1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1049 \mode<presentation>{ |
|
1050 \begin{frame}[t] |
|
1051 \frametitle{} |
|
1052 \small |
|
1053 |
|
1054 \textcolor{blue}{ |
|
1055 \begin{center} |
|
1056 \only<1>{$ \underbrace{ |
|
1057 \mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}} |
|
1058 {\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$} |
|
1059 \end{center}} |
|
1060 |
|
1061 \textcolor{blue}{ |
|
1062 \begin{center} |
|
1063 \only<1>{ |
|
1064 $ \underbrace{ |
|
1065 \mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}} |
|
1066 {\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{} |
|
1067 & |
|
1068 \deduce[$\vdots$]{X}{} |
|
1069 }}}_{Y}$} |
|
1070 \end{center}} |
|
1071 |
|
1072 \textcolor{blue}{ |
|
1073 \begin{center} |
|
1074 \only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}} |
|
1075 {\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{} |
|
1076 & |
|
1077 \deduce[$\vdots$]{Y}{} |
|
1078 }}} |
|
1079 \end{center}} |
|
1080 |
|
1081 \end{frame}} |
|
1082 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1083 % |
|
1084 |
|
1085 |
|
1086 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1087 \mode<presentation>{ |
|
1088 \begin{frame}[c] |
|
1089 \frametitle{Controls} |
|
1090 \small |
|
1091 |
|
1092 \begin{itemize} |
|
1093 \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} |
|
1094 |
|
1095 \item its meaning ``\bl{P} is entitled to do \bl{F}'' |
|
1096 \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause |
|
1097 |
|
1098 \begin{center} |
|
1099 \bl{\mbox{ |
|
1100 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} |
|
1101 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1102 }} |
|
1103 \end{center}\pause |
|
1104 |
|
1105 \begin{center} |
|
1106 \bl{\mbox{ |
|
1107 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}} |
|
1108 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1109 }} |
|
1110 \end{center} |
|
1111 \end{itemize} |
|
1112 |
|
1113 \end{frame}} |
|
1114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1115 % |
|
1116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1117 \mode<presentation>{ |
|
1118 \begin{frame}[c] |
|
1119 \frametitle{Speaks For} |
|
1120 \small |
|
1121 |
|
1122 \begin{itemize} |
|
1123 \item \bl{\isa{P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}F{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ says\ F{\isaliteral{29}{\isacharparenright}}}} |
|
1124 |
|
1125 \item its meaning ``\bl{P} speaks for \bl{Q}'' |
|
1126 |
|
1127 |
|
1128 \begin{center} |
|
1129 \bl{\mbox{ |
|
1130 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}} |
|
1131 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}} |
|
1132 }} |
|
1133 \end{center}\pause |
|
1134 |
|
1135 \begin{center} |
|
1136 \bl{\mbox{ |
|
1137 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}} |
|
1138 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}} |
|
1139 }} |
|
1140 \end{center} |
|
1141 |
|
1142 \begin{center} |
|
1143 \bl{\mbox{ |
|
1144 \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}} |
|
1145 {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}} |
|
1146 }} |
|
1147 \end{center} |
|
1148 \end{itemize} |
|
1149 |
|
1150 \end{frame}} |
|
1151 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1152 % |
|
1153 |
|
1154 |
|
1155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1156 \mode<presentation>{ |
|
1157 \begin{frame}[c] |
|
1158 \frametitle{Security Levels} |
|
1159 \small |
|
1160 |
|
1161 \begin{itemize} |
|
1162 \item Top secret (\bl{$T\!S$}) |
|
1163 \item Secret (\bl{$S$}) |
|
1164 \item Public (\bl{$P$}) |
|
1165 \end{itemize} |
|
1166 |
|
1167 \begin{center} |
|
1168 \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause |
|
1169 \end{center} |
|
1170 |
|
1171 \begin{itemize} |
|
1172 \item Bob has a clearance for ``secret'' |
|
1173 \item Bob can read documents that are public or sectret, but not top secret |
|
1174 \end{itemize} |
|
1175 |
|
1176 \end{frame}} |
|
1177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1178 % |
|
1179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1180 \mode<presentation>{ |
|
1181 \begin{frame}[c] |
|
1182 \frametitle{Reading a File} |
|
1183 |
|
1184 \bl{\begin{center} |
|
1185 \begin{tabular}{c} |
|
1186 \begin{tabular}{@ {}l@ {}} |
|
1187 \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ |
|
1188 \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\ |
|
1189 Bob says Permitted $($File, read$)$\only<2->{\\} |
|
1190 \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}% |
|
1191 \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}% |
|
1192 \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}% |
|
1193 \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}% |
|
1194 \end{tabular}\\ |
|
1195 \hline |
|
1196 Permitted $($File, read$)$ |
|
1197 \end{tabular} |
|
1198 \end{center}} |
|
1199 |
|
1200 \end{frame}} |
|
1201 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1202 % |
|
1203 |
|
1204 |
|
1205 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1206 \mode<presentation>{ |
|
1207 \begin{frame}[c] |
|
1208 \frametitle{Substitution Rule} |
|
1209 \small |
|
1210 |
|
1211 \bl{\begin{center} |
|
1212 \begin{tabular}{c} |
|
1213 $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$ |
|
1214 \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline |
|
1215 $\Gamma \vdash slev(P) < slev(Q)$ |
|
1216 \end{tabular} |
|
1217 \end{center}}\bigskip\pause |
|
1218 |
|
1219 \begin{itemize} |
|
1220 \item \bl{$slev($Bob$)$ $=$ $S$} |
|
1221 \item \bl{$slev($File$)$ $=$ $P$} |
|
1222 \item \bl{$slev(P) < slev(S)$} |
|
1223 \end{itemize} |
|
1224 |
|
1225 \end{frame}} |
|
1226 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1227 % |
|
1228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1229 \mode<presentation>{ |
|
1230 \begin{frame}[c] |
|
1231 \frametitle{Reading a File} |
|
1232 |
|
1233 \bl{\begin{center} |
|
1234 \begin{tabular}{c} |
|
1235 \begin{tabular}{@ {}l@ {}} |
|
1236 $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ |
|
1237 \hspace{3cm}Bob controls Permitted $($File, read$)$\\ |
|
1238 Bob says Permitted $($File, read$)$\\ |
|
1239 $slev($File$)$ $=$ $P$\\ |
|
1240 $slev($Bob$)$ $=$ $T\!S$\\ |
|
1241 \only<1>{\textcolor{red}{$?$}}% |
|
1242 \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}% |
|
1243 \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}% |
|
1244 \end{tabular}\\ |
|
1245 \hline |
|
1246 Permitted $($File, read$)$ |
|
1247 \end{tabular} |
|
1248 \end{center}} |
|
1249 |
|
1250 \end{frame}} |
|
1251 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1252 % |
|
1253 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1254 \mode<presentation>{ |
|
1255 \begin{frame}[c] |
|
1256 \frametitle{Transitivity Rule} |
|
1257 \small |
|
1258 |
|
1259 \bl{\begin{center} |
|
1260 \begin{tabular}{c} |
|
1261 $\Gamma \vdash l_1 < l_2$ |
|
1262 \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline |
|
1263 $\Gamma \vdash l_1 < l_3$ |
|
1264 \end{tabular} |
|
1265 \end{center}}\bigskip |
|
1266 |
|
1267 \begin{itemize} |
|
1268 \item \bl{$slev(P) < slev (S)$} |
|
1269 \item \bl{$slev(S) < slev (T\!S)$} |
|
1270 \item[] \bl{$slev(P) < slev (T\!S)$} |
|
1271 \end{itemize} |
|
1272 |
|
1273 \end{frame}} |
|
1274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1275 % |
|
1276 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1277 \mode<presentation>{ |
|
1278 \begin{frame}[c] |
|
1279 \frametitle{Reading Files} |
|
1280 |
|
1281 \begin{itemize} |
|
1282 \item Access policy for reading |
|
1283 \end{itemize} |
|
1284 |
|
1285 \bl{\begin{center} |
|
1286 \begin{tabular}{c} |
|
1287 \begin{tabular}{@ {}l@ {}} |
|
1288 $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ |
|
1289 \hspace{3cm}Bob controls Permitted $(f$, read$)$\\ |
|
1290 Bob says Permitted $($File, read$)$\\ |
|
1291 $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\ |
|
1292 $slev($Bob$)$ $=$ $T\!S$\\ |
|
1293 $slev(P) < slev(S)$\\ |
|
1294 $slev(S) < slev(T\!S)$ |
|
1295 \end{tabular}\\ |
|
1296 \hline |
|
1297 Permitted $($File, read$)$ |
|
1298 \end{tabular} |
|
1299 \end{center}} |
|
1300 |
|
1301 \end{frame}} |
|
1302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1303 % |
|
1304 |
|
1305 |
|
1306 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1307 \mode<presentation>{ |
|
1308 \begin{frame}[c] |
|
1309 \frametitle{Writing Files} |
|
1310 |
|
1311 \begin{itemize} |
|
1312 \item Access policy for \underline{writing} |
|
1313 \end{itemize} |
|
1314 |
|
1315 \bl{\begin{center} |
|
1316 \begin{tabular}{c} |
|
1317 \begin{tabular}{@ {}l@ {}} |
|
1318 $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ |
|
1319 \hspace{3cm}Bob controls Permitted $(f$, write$)$\\ |
|
1320 Bob says Permitted $($File, write$)$\\ |
|
1321 $slev($File$)$ $=$ $T\!S$\\ |
|
1322 $slev($Bob$)$ $=$ $S$\\ |
|
1323 $slev(P) < slev(S)$\\ |
|
1324 $slev(S) < slev(T\!S)$ |
|
1325 \end{tabular}\\ |
|
1326 \hline |
|
1327 Permitted $($File, write$)$ |
|
1328 \end{tabular} |
|
1329 \end{center}} |
|
1330 |
|
1331 \end{frame}} |
|
1332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1333 % |
|
1334 |
|
1335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1336 \mode<presentation>{ |
|
1337 \begin{frame}[c] |
|
1338 \frametitle{Point to Take Home} |
|
1339 |
|
1340 \begin{itemize} |
|
1341 \item Formal methods can be an excellent way of finding |
|
1342 bugs as they force the designer |
|
1343 to make everything explicit and thus confront difficult design |
|
1344 choices that might otherwise be fudged. |
|
1345 \end{itemize} |
|
1346 |
|
1347 \end{frame}} |
|
1348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1349 |
|
1350 \end{document} |
504 \end{document} |
1351 |
505 |
1352 %%% Local Variables: |
506 %%% Local Variables: |
1353 %%% mode: latex |
507 %%% mode: latex |
1354 %%% TeX-master: t |
508 %%% TeX-master: t |