--- a/slides/slides05.tex Sun Oct 19 16:44:31 2014 +0100
+++ b/slides/slides05.tex Tue Oct 21 02:35:06 2014 +0100
@@ -1,108 +1,24 @@
\documentclass[dvipsnames,14pt,t]{beamer}
-\usepackage{proof}
-\usepackage{beamerthemeplaincu}
-\usepackage{fontenc}
-\usepackage[latin1]{inputenc}
-\usepackage{mathpartir}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage[absolute,overlay]{textpos}
-\usepackage{ifthen}
-\usepackage{tikz}
-\usepackage{courier}
-\usepackage{listings}
+\usepackage{../slides}
+\usepackage{../graphics}
+\usepackage{../langs}
\usetikzlibrary{arrows}
-\usetikzlibrary{positioning}
-\usetikzlibrary{calc}
-\usepackage{graphicx}
-\setmonofont{Consolas}
+\usetikzlibrary{shapes}
-\isabellestyle{rm}
-\renewcommand{\isastyle}{\rm}%
-\renewcommand{\isastyleminor}{\rm}%
-\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
-\renewcommand{\isatagproof}{}
-\renewcommand{\endisatagproof}{}
-\renewcommand{\isamarkupcmt}[1]{#1}
+\setmonofont[Scale=.88]{Consolas}
+\newfontfamily{\consolas}{Consolas}
-% Isabelle characters
-\renewcommand{\isacharunderscore}{\_}
-\renewcommand{\isacharbar}{\isamath{\mid}}
-\renewcommand{\isasymiota}{}
-\renewcommand{\isacharbraceleft}{\{}
-\renewcommand{\isacharbraceright}{\}}
-\renewcommand{\isacharless}{$\langle$}
-\renewcommand{\isachargreater}{$\rangle$}
-\renewcommand{\isasymsharp}{\isamath{\#}}
-\renewcommand{\isasymdots}{\isamath{...}}
-\renewcommand{\isasymbullet}{\act}
-\newcommand{\isaliteral}[1]{}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\hfuzz=220pt
-\definecolor{javared}{rgb}{0.6,0,0} % for strings
-\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
-\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
-\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
-
-\makeatletter
-\lst@CCPutMacro\lst@ProcessOther {"2D}{\lst@ttfamily{-{}}{-{}}}
-\@empty\z@\@empty
-\makeatother
+% beamer stuff
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+\renewcommand{\slidecaption}{APP 05, King's College London}
-\lstdefinelanguage{scala}{
- morekeywords={abstract,case,catch,class,def,%
- do,else,extends,false,final,finally,%
- for,if,implicit,import,match,mixin,%
- new,null,object,override,package,%
- private,protected,requires,return,sealed,%
- super,this,throw,trait,true,try,%
- type,val,var,while,with,yield},
- otherkeywords={=>,<-,<\%,<:,>:,\#,@},
- sensitive=true,
- morecomment=[l]{//},
- morecomment=[n]{/*}{*/},
- morestring=[b]",
- morestring=[b]',
- morestring=[b]"""
-}
-
-\lstdefinelanguage{while}{
- morekeywords={while, if, then. else, read, write},
- otherkeywords={=>,<-,<\%,<:,>:,\#,@},
- sensitive=true,
- morecomment=[l]{//},
- morecomment=[n]{/*}{*/},
- morestring=[b]",
- morestring=[b]',
- morestring=[b]"""
-}
-
-
-\lstset{language=Scala,
- basicstyle=\ttfamily,
- keywordstyle=\color{javapurple}\bfseries,
- stringstyle=\color{javagreen},
- commentstyle=\color{javagreen},
- morecomment=[s][\color{javadocblue}]{/**}{*/},
- numbers=left,
- numberstyle=\tiny\color{black},
- stepnumber=1,
- numbersep=10pt,
- tabsize=2,
- showspaces=false,
- showstringspaces=false}
-
-
-% beamer stuff
-\renewcommand{\slidecaption}{APP 05, King's College London, 29 October 2013}
-
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>[t]
+\begin{frame}[t]
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\\
@@ -110,11 +26,7 @@
\LARGE Privacy Policies (5)\\[-6mm]
\end{tabular}}\bigskip\bigskip\bigskip
- %\begin{center}
- %\includegraphics[scale=1.3]{pics/barrier.jpg}
- %\end{center}
-
-\normalsize
+ \normalsize
\begin{center}
\begin{tabular}{ll}
Email: & christian.urban at kcl.ac.uk\\
@@ -123,246 +35,194 @@
\end{tabular}
\end{center}
-
-\end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Last Week}
-
-\mbox{}
-
-\begin{tabular}{l}
-{\Large \bl{$A\;\rightarrow\; B : \ldots$}}\\
-\onslide<1->{\Large \bl{$B\;\rightarrow\; A : \ldots$}}\\
-\onslide<1->{\Large \;\;\;\;\;\bl{$:$}}\bigskip
-\end{tabular}
-
- \begin{itemize}
- \item by convention \bl{$A$}, \bl{$B$} are named principals \bl{Alice\ldots}\\
- but most likely they are programs
-\item indicates one ``protocol run'', or session, which specifies an
-order in the communication
-\item there can be several sessions in parallel (think of wifi routers)
-\item nonces (randomly generated numbers) used only once
-\end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Cryptographic Protocol Failures}
-
-Ross Anderson and Roger Needham wrote:\bigskip
-
-\begin{quote}
-\textcolor{gray}{
-A lot of the recorded frauds were the result of this kind of blunder, or from
-management negligence pure and simple.} However, there have been a
-significant number of cases where the designers protected the right things,
-used cryptographic algorithms which were not broken, and yet found that their
-systems were still successfully attacked.
-\end{quote}
-
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Protocols}
-Examples where ``over-the-air'' protocols are used
+Some examples where ``over-the-air'' protocols are used:
\begin{itemize}
\item wifi
\item card readers (you cannot trust the terminals)
-\item RFI (passports)
+\item RFID (passports)
+\item car transponders
+\end{itemize}\medskip\pause
+
+The point is that we cannot control the network:
+An attacker can install a packet sniffer, inject packets,
+modify packets, replay messages.
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Keyless Car Transponders}
+
+\begin{center}
+\includegraphics[scale=0.1]{../pics/keyfob.jpg}
+\quad
+\includegraphics[scale=0.27]{../pics/startstop.jpg}
+\end{center}
+
+\begin{itemize}
+\item There are two security mechanisms: one remote central
+locking system and one passive RFID tag (engine immobiliser).
+\item How can I get in? How can thieves be kept out?
+How to avoid MITM attacks?
+\end{itemize}\medskip
+
+\footnotesize
+\hfill Papers: Gone in 360 Seconds: Hijacking with Hitag2,\\
+\hfill Dismantling Megamos Crypto: Wirelessly Lockpicking\\
+\hfill a Vehicle Immobilizer
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{HTTPS / GSM}
+
+\begin{center}
+\includegraphics[scale=0.25]{../pics/barclays.jpg}
+\quad
+\includegraphics[scale=0.25]{../pics/phone-signal.jpg}
+\end{center}
+
+\begin{itemize}
+\item I am sitting at Starbuck. How can I be sure I am
+really visiting Barclays? I have no control of the access
+point.
+\item How can I achieve that a secret key is established
+in order to encrypt my conversation? I have no control over
+the access point.
\end{itemize}
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
+\frametitle{Handshakes}
+
+\begin{itemize}
+\item starting a TCP connection between a client and a server
+initiates the following three-way handshake protocol:
+\end{itemize}
+
+\begin{columns}[t]
+\begin{column}{5cm}
+\begin{minipage}[t]{4cm}
+\begin{center}
+\raisebox{-2cm}{\includegraphics[scale=0.5]{../pics/handshake.png}}
+\end{center}
+\end{minipage}
+\end{column}
+\begin{column}{5cm}
+\begin{tabular}[t]{rl}
+Alice: & Hello server!\\
+Server: & I heard you\\
+Alice: & Thanks
+\end{tabular}
+\end{column}
+\end{columns}\pause
\begin{center}
-\includegraphics[scale=0.5]{pics/dogs.jpg}
+\begin{tabular}{rl}
+\bl{$A \rightarrow S$}: & \bl{SYN}\\
+\bl{$S \rightarrow A$}: & \bl{SYN-ACK}\\
+\bl{$A \rightarrow S$}: & \bl{ACK}\\
+\end{tabular}
\end{center}
-\end{frame}}
+\only<2>{
+\begin{textblock}{3}(11,5)
+\begin{bubble}[3.2cm]
+SYNflood attacks:\medskip\\
+\includegraphics[scale=0.4]{../pics/synflood.png}
+\end{bubble}
+\end{textblock}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Authentication}
+
+\begin{columns}
+\begin{column}{8cm}
+\begin{minipage}[t]{7.5cm}
+\begin{center}
+\raisebox{-2cm}{\includegraphics[scale=0.4]{../pics/dogs.jpg}}
+\end{center}
+\end{minipage}
+\end{column}
+\begin{column}{5cm}
+\begin{minipage}[t]{4.5cm}
+\begin{tabular}{l}
+Knock Knock!\\
+Who's there?\\
+Alice.\\
+Alice who?
+\end{tabular}
+\end{minipage}
+\end{column}
+\end{columns}
+
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{\begin{tabular}{c}Chip-and-PIN\end{tabular}}
-
-
-\begin{itemize}
-\item A ``tamperesitant'' terminal playing Tetris on
-\textcolor{blue}{\href{http://www.youtube.com/watch?v=wWTzkD9M0sU}{youtube}}.\\
-\textcolor{lightgray}{\footnotesize(\url{http://www.youtube.com/watch?v=wWTzkD9M0sU})}
-\end{itemize}
-
-
-\includegraphics[scale=0.2]{pics/tetris.jpg}
-
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-3>[c]
- \frametitle{Oyster Cards}
-
- \includegraphics[scale=0.4]{pics/oysterc.jpg}
-
- \begin{itemize}
- \item good example of a bad protocol\\ (security by obscurity)\bigskip
- \item<3-> ``Breaching security on Oyster cards should not
- allow unauthorised use for more than a day, as TfL promises to turn
- off any cloned cards within 24 hours\ldots''
- \end{itemize}
-
- \only<2>{
- \begin{textblock}{12}(0.5,0.5)
- \begin{tikzpicture}
- \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
- {\color{darkgray}
- \begin{minipage}{11cm}\raggedright\footnotesize
- {\bf Wirelessly Pickpocketing a Mifare Classic Card}\medskip
-
- The Mifare Classic is the most widely used contactless smartcard on the
- market. The stream cipher CRYPTO1 used by the Classic has recently been
- reverse engineered and serious attacks have been proposed. The most serious
- of them retrieves a secret key in under a second. In order to clone a card,
- previously proposed attacks require that the adversary either has access to
- an eavesdropped communication session or executes a message-by-message
- man-in-the-middle attack between the victim and a legitimate
- reader. Although this is already disastrous from a cryptographic point of
- view, system integrators maintain that these attacks cannot be performed
- undetected.\smallskip
-
- This paper proposes four attacks that can be executed by an adversary having
- only wireless access to just a card (and not to a legitimate reader). The
- most serious of them recovers a secret key in less than a second on ordinary
- hardware. Besides the cryptographic weaknesses, we exploit other weaknesses
- in the protocol stack. A vulnerability in the computation of parity bits
- allows an adversary to establish a side channel. Another vulnerability
- regarding nested authentications provides enough plaintext for a speedy
- known-plaintext attack.
- \end{minipage}};
- \end{tikzpicture}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1->[t]
- \frametitle{Another Example}
-
-In an email from Ross Anderson\bigskip\small
-
-\begin{tabular}{l}
-From: Ross Anderson <Ross.Anderson@cl.cam.ac.uk>\\
-Sender: cl-security-research-bounces@lists.cam.ac.uk\\
-To: cl-security-research@lists.cam.ac.uk\\
-Subject: Birmingham case\\
-Date: Tue, 13 Aug 2013 15:13:17 +0100\\
-\end{tabular}
-
-
- \only<2>{
- \begin{textblock}{12}(0.5,0.5)
- \begin{tikzpicture}
- \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
- {\color{darkgray}
- \begin{minipage}{11cm}\raggedright\footnotesize
-As you may know, Volkswagen got an injunction against the University of
-Birmingham suppressing the publication of the design of a weak cipher
-used in the remote key entry systems in its recent-model cars. The paper
-is being given today at Usenix, minus the cipher design.\medskip
-
-I've been contacted by Birmingham University's lawyers who seek to prove
-that the cipher can be easily obtained anyway. They are looking for a
-student who will download the firmware from any newish VW, disassemble
-it and look for the cipher. They'd prefer this to be done by a student
-rather than by a professor to emphasise how easy it is.\medskip
-
-Volkswagen's argument was that the Birmingham people had reversed a
-locksmithing tool produced by a company in Vietnam, and since their key
-fob chip is claimed to be tamper-resistant, this must have involved a
-corrupt insider at VW or at its supplier Thales. Birmingham's argument
-is that this is nonsense as the cipher is easy to get hold of. Their
-lawyers feel this argument would come better from an independent
-outsider.\medskip
-
-Let me know if you're interested in having a go, and I'll put you in
-touch
-
-Ross
- \end{minipage}};
- \end{tikzpicture}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Authentication Protocols}
-
-Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip
+Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key
+\bl{$K_{AB}$}\bigskip
Passwords:
\begin{center}
-\bl{$B \rightarrow A: K_{AB}$}
+\bl{$A \rightarrow B: K_{AB}$}
\end{center}\pause\bigskip
-Problems: Eavesdropper can capture the secret and replay it; \bl{$A$} cannot confirm the
-identity of \bl{$B$}
+Problems: Eavesdropper can capture the secret and replay it;
+\bl{$B$} cannot confirm the identity of \bl{$A$}
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Authentication Protocols}
-Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip
+Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key
+\bl{$K_{AB}$}\bigskip
Simple Challenge Response:
\begin{center}
-\begin{tabular}{ll}
-\bl{$A \rightarrow B:$} & \bl{$N$}\\
-\bl{$B \rightarrow A:$} & \bl{$\{N\}_{K_{AB}}$}\\
+\begin{tabular}{lll}
+\bl{$A \rightarrow B:$} & \bl{Hi I am A}\\
+\bl{$B \rightarrow A:$} & \bl{$N$} & (challenge)\\
+\bl{$A \rightarrow B:$} & \bl{$\{N\}_{K_{AB}}$}\\
\end{tabular}
-\end{center}
+\end{center}\pause
+\begin{itemize}
+\item cannot replay since next time will be another challenge
+\item \bl{$B$} authenticates \bl{$A$}, but \bl{$A$} does not
+authenticate \bl{$B$} (be Eve in the middle, intercept
+messages from \bl{$A$} and ignore last)
+\end{itemize}
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Authentication Protocols}
@@ -379,26 +239,118 @@
\end{center}
-\end{frame}}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Nonces}
+
+\begin{enumerate}
+\item I generate a nonce (random number) and send it to you encrypted with a key we share
+\item you increase it by one, encrypt it under a key I know and send
+it back to me
+\end{enumerate}
+
+
+I can infer:
+
+\begin{itemize}
+\item you must have received my message
+\item you could only have generated your answer after I send you my initial
+message
+\item if only you and me know the key, the message must have come from you
+\end{itemize}
+
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
-\frametitle{One Time Passwords}
+
+\begin{center}
+\begin{tabular}{ll}
+\bl{$A \rightarrow B$:} & \bl{$N_A$}\\
+\bl{$B \rightarrow A$:} & \bl{$\{N_A, N_B\}_{K_{ab}}$}\\
+\bl{$A \rightarrow B$:} & \bl{$N_B$}\\
+\end{tabular}
+\end{center}
+
+The attack (let $A$ decrypt her own messages):
\begin{center}
-\bl{$B \rightarrow A: C, C_{K_{AB}}$}
-\end{center}\bigskip
+\begin{tabular}{ll}
+\bl{$A \rightarrow E$:} & \bl{$N_A$}\\
+\textcolor{gray}{$E \rightarrow A$:} & \textcolor{gray}{$N_A$}\\
+\textcolor{gray}{$A \rightarrow E$:} & \textcolor{gray}{$\{N_A, N_A'\}_{K_{AB}}$}\\
+\bl{$E \rightarrow A$:} & \bl{$\{N_A, N_A'\}_{K_{AB}}$}\\
+\bl{$A \rightarrow E$:} & \bl{$N_A' \;\;(= N_B)$}\\
+\end{tabular}
+\end{center}\pause
+
+\small Solutions: \bl{$K_{AB} \not= K_{BA}$} or include an id in the second message
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Encryption to the Rescue?}
+
+
+ \begin{itemize}
+ \item \bl{$A \,\rightarrow\, B : \{A, N_A\}_{K_{AB}}$}\hspace{1cm} encrypted\bigskip
+ \item \bl{$B\,\rightarrow\, A : \{N_A, K'_{AB}\}_{K_{AB}}$}\bigskip
+ \item \bl{$A \,\rightarrow\, B : \{N_A\}_{K'_{AB}}$}\bigskip
+ \end{itemize}\pause
+
+means you need to send separate ``Hello'' signals (bad), or worse
+share a single key between many entities
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-A counter \bl{$C$} increases with each transmission; \bl{$A$} will not accept a
-\bl{$C$} which has already been accepted (used in car key fob).
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Protocol Attacks}
+
+\begin{itemize}
+\item replay attacks
+\item reflection attacks
+\item man-in-the-middle attacks
+\item timing attacks
+\item parallel session attacks
+\item binding attacks (public key protocols)
+\item changing environment / changing assumptions\bigskip
+
+\item (social engineering attacks)
+\end{itemize}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Public-Key Infrastructure}
+
+\begin{itemize}
+\item the idea is to have a certificate authority (CA)
+\item you go to the CA to identify yourself
+\item CA: ``I, the CA, have verified that public key \bl{$P^{pub}_{Bob}$} belongs to Bob''\bigskip
+\item CA must be trusted by everybody
+\item What happens if CA issues a false certificate? Who pays in case of loss? (VeriSign
+explicitly limits liability to \$100.)
+\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Person-in-the-Middle}
@@ -413,7 +365,7 @@
with its private key
\end{itemize}
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -435,7 +387,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Person-in-the-Middle}
@@ -452,34 +403,30 @@
\bl{$C$} would have to invent a totally new message
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
-\frametitle{Motivation}
-
-The ISO/IEC 9798 specifies authentication mechanisms which use security
-techniques. These mechanisms are used to corroborate that an entity is the one
-that is claimed. An entity to be authenticated proves its identity by showing its
-knowledge of a secret. The mechanisms are defined as exchanges of information
-between entities and, where required, exchanges with a trusted third party.
+\frametitle{Car Transponder (HiTag2)}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{enumerate}
+\item \bl{$C$} generates a random number \bl{$r$}
+\item \bl{$C$} calculates \bl{$(F,G) = \{r\}_K$}
+\item \bl{$C \to T$}: \bl{$r, F$}
+\item \bl{$T$} calculates \bl{$(F',G') = \{r\}_K$}
+\item \bl{$T$} checks that \bl{$F = F'$}
+\item \bl{$T \to C$}: \bl{$r, G'$}
+\item \bl{$C$} checks that \bl{$G = G'$}
+\end{enumerate}\pause
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Motivation}
+\small
+This process means that the transponder believes the car knows
+the key \bl{$K$}, and the car believes the transponder knows
+the key \bl{$K$}. They should have authenticated themselves
+to each other.
-But\ldots\bigskip
-
-The ISO/IEC 9798 standard neither specifies a threat model nor defines the security properties that the protocols should satisfy.\pause\bigskip
-
Unfortunately, there are no general precise definitions for the goals of protocols.
-
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -502,8 +449,12 @@
\begin{frame}[c]
\frametitle{Best Practices}
-{\bf Principle 3:} Be clear about why encryption is being done. Encryption is not wholly cheap, and not asking precisely why it is being done can lead to redundancy. Encryption is not synonymous with security.
+{\bf Principle 3:} Be clear about why encryption is being
+done. Encryption is not wholly cheap, and not asking precisely
+why it is being done can lead to redundancy. Encryption is not
+synonymous with security.
+\small
\begin{center}
Possible Uses of Encryption
@@ -519,26 +470,21 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
\frametitle{Best Practices}
{\bf Principle 4:} The protocol designer should know which trust relations his protocol depends on, and why the dependence is necessary. The reasons for particular trust relations being acceptable should be explicit though they will be founded on judgment and policy rather than on logic.\bigskip
Example Certification Authorities: CAs are trusted to certify a key only after proper steps
-have been taken to identify the principal that owns it.
-
-
+have been taken to identify the principal that owns it.
-
-
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
-\frametitle{Access Control Logic}
+\frametitle{Formal Methods}
Ross Anderson about the use of Logic:\bigskip
@@ -552,797 +498,6 @@
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}}
-
- \begin{itemize}
- \item Formulas
-
- \begin{center}\color{blue}
- \begin{tabular}{rcl@ {\hspace{10mm}}l}
- \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F} & \textcolor{black}{implies}\\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F} & \textcolor{black}{negation}\\
- & \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}\\
- & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} &
- \onslide<2->{\textcolor{black}{forall quantification}}\\
- & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} &
- \onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm]
- \end{tabular}
- \end{center}
-
- \end{itemize}
-
- \begin{textblock}{12}(1,14)
- 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}}}}
- \end{textblock}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
-
-{\lstset{language=Scala}\fontsize{10}{12}\selectfont
-\texttt{\lstinputlisting{../programs/formulas.scala}}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Judgements}
-
- \begin{center}
- \LARGE
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}
- \end{center}
-
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause
-
- \begin{itemize}
- \item Example\mbox{}\\[-3mm]
-
- \only<2>{\begin{center}\tiny
- \textcolor{blue}{
- \begin{tabular}{l}
- \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
- \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
- \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}}}\\
- \end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
- \end{center}}
- \only<3>{\small
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
- {\mbox{\begin{tabular}{@ {}l@ {}}
- \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
- \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
- \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}}}\\
- \end{tabular}}
- }
- }
- \end{center}
- }}
- \only<4>{\small
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}
- {\mbox{\begin{tabular}{@ {}l@ {}}
- \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\
- \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
- \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
- \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}}}\\
- \end{tabular}}
- }
- }
- \end{center}
- }}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
-
-{\lstset{language=Scala}\fontsize{10}{12}\selectfont
-\texttt{\lstinputlisting{../programs/judgement.scala}}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Inference Rules}
-
- \textcolor{blue}{
- \begin{center}
- \Large
- \mbox{
- \infer{\mbox{\isa{conclusion}}}
- {\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}}
- \end{center}}
-
- The conlusion and premises are judgements\bigskip\pause
-
- \begin{itemize}
- \item Examples
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
- {\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}}}}}}
- \end{center}}\pause
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}
- \hspace{10mm}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
- \end{center}}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Implication}
- \Large
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\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{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
- \end{center}}
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
- {\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}}}}}}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Universal Quantification}
- \Large
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{$\isacharbrackleft$}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{$\isacharbrackright$}}}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Start Rules / Axioms}
-
- \normalsize
- \alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}}
-
- \textcolor{blue}{\Large
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}
- \end{center}}\bigskip\pause
-
- \normalsize
- Also written as:
- \textcolor{blue}{\Large
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}
- \end{center}}\pause
-
- \textcolor{blue}{\Large
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{}
-
- \begin{minipage}{1.1\textwidth}
- Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l}
- \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
- \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
- \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}}}\\
- \end{tabular}}
- \end{minipage}
-
- \only<2>{
- \begin{textblock}{12}(4,3)\footnotesize
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm}
- \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}}}}
- \end{textblock}}
-
- \only<3->{
- \begin{textblock}{12}(4,3)\footnotesize
- \mbox{\textcolor{blue}{
- \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}}}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm}
- \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
- }}
- \end{textblock}}
-
- \only<4>{
- \begin{textblock}{14}(0.5,6)\footnotesize
- \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}}}}
- \end{textblock}}
-
- \only<5->{
- \begin{textblock}{14}(0.5,6)\footnotesize
- \textcolor{blue}{
- \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}}}\\
- \hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}}
- {\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}}}}}}
- \end{textblock}}
-
- \only<6->{
- \begin{textblock}{14}(5,10)\footnotesize
- \textcolor{blue}{
- \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}}}}}
- {\vdots & \hspace{30mm} \vdots}}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Access Control}
- \Large
-
- \textcolor{blue}{
- \begin{center}
- \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}
- \end{center}}\bigskip
-
- \normalsize
- \begin{itemize}
- \item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted)
- \item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied)
- \end{itemize}\bigskip\pause
-
-\begin{minipage}{1.1\textwidth}
- \small
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
- \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
- \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
- \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}}}\\
- \end{tabular}}\medskip
-
- \textcolor{blue}{
- \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}
-\end{minipage}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{The Access Control Problem}
-
-
-\begin{center}
- \begin{tikzpicture}[scale=1]
-
- \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
- \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
- \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}};
- \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}};
-
- \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1);
- \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
- \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2);
-
- \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};
-
- \end{tikzpicture}
-\end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Bad News}
-
- \begin{itemize}
- \item We introduced (roughly) first-order logic. \bigskip\pause
-
- \item Judgements
- \begin{center}
- \textcolor{blue}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
- \end{center}
-
- are in general \alert{undecidable}.\pause\medskip\\
-
- The problem is \alert{semi-decidable}.
-
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
-
- \begin{itemize}
- \item[]
-
- \begin{center}\color{blue}
- \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
- \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\
- & \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}}} \\
- & \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\
- \end{tabular}
- \end{center}\medskip
-
- 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
-
- \item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
- \end{itemize}
-
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
-
-{\lstset{language=Scala}\fontsize{10}{12}\selectfont
-\texttt{\lstinputlisting{../programs/formulas1.scala}}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Rules about Says}
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}
- \end{center}}
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
- {\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}}}}}}
- \end{center}}
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{}
-
- Consider the following scenario:
-
- \begin{itemize}
- \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
- should be deleted, then this file must be deleted.
- \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
- \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted.
- \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}.
- \end{itemize}\bigskip\pause
-
- \small
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
- \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}}},\\
- \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}}},\\
- \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
- \end{tabular}}\medskip\pause
-
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{}
-
- \textcolor{blue}{
- \begin{center}
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip
- \mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
- {\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}}}}}}
- \end{center}}\bigskip
-
- \small
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
- \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}}},\\
- \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}}},\\
- \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
- \end{tabular}}\medskip
-
- \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{}
- \small
-
- \textcolor{blue}{
- \begin{center}
- \only<1>{$ \underbrace{
- \mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}}
- {\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$}
- \end{center}}
-
- \textcolor{blue}{
- \begin{center}
- \only<1>{
- $ \underbrace{
- \mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}}
- {\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{}
- &
- \deduce[$\vdots$]{X}{}
- }}}_{Y}$}
- \end{center}}
-
- \textcolor{blue}{
- \begin{center}
- \only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}}
- {\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{}
- &
- \deduce[$\vdots$]{Y}{}
- }}}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Controls}
- \small
-
- \begin{itemize}
- \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}
-
- \item its meaning ``\bl{P} is entitled to do \bl{F}''
- \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- }}
- \end{center}\pause
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
- {\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}}}
- }}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Speaks For}
- \small
-
- \begin{itemize}
- \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}}}}
-
- \item its meaning ``\bl{P} speaks for \bl{Q}''
-
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
- }}
- \end{center}\pause
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}}
- {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}}
- }}
- \end{center}
-
- \begin{center}
- \bl{\mbox{
- \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}}
- {\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}}}
- }}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Security Levels}
- \small
-
- \begin{itemize}
- \item Top secret (\bl{$T\!S$})
- \item Secret (\bl{$S$})
- \item Public (\bl{$P$})
- \end{itemize}
-
- \begin{center}
- \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
- \end{center}
-
- \begin{itemize}
- \item Bob has a clearance for ``secret''
- \item Bob can read documents that are public or sectret, but not top secret
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
- \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\only<2->{\\}
- \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
- \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
- \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
- \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Substitution Rule}
- \small
-
- \bl{\begin{center}
- \begin{tabular}{c}
- $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
- \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
- $\Gamma \vdash slev(P) < slev(Q)$
- \end{tabular}
- \end{center}}\bigskip\pause
-
- \begin{itemize}
- \item \bl{$slev($Bob$)$ $=$ $S$}
- \item \bl{$slev($File$)$ $=$ $P$}
- \item \bl{$slev(P) < slev(S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading a File}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $($File, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ $P$\\
- $slev($Bob$)$ $=$ $T\!S$\\
- \only<1>{\textcolor{red}{$?$}}%
- \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
- \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Transitivity Rule}
- \small
-
- \bl{\begin{center}
- \begin{tabular}{c}
- $\Gamma \vdash l_1 < l_2$
- \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
- $\Gamma \vdash l_1 < l_3$
- \end{tabular}
- \end{center}}\bigskip
-
- \begin{itemize}
- \item \bl{$slev(P) < slev (S)$}
- \item \bl{$slev(S) < slev (T\!S)$}
- \item[] \bl{$slev(P) < slev (T\!S)$}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Reading Files}
-
- \begin{itemize}
- \item Access policy for reading
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
- Bob says Permitted $($File, read$)$\\
- $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
- $slev($Bob$)$ $=$ $T\!S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, read$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Writing Files}
-
- \begin{itemize}
- \item Access policy for \underline{writing}
- \end{itemize}
-
- \bl{\begin{center}
- \begin{tabular}{c}
- \begin{tabular}{@ {}l@ {}}
- $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
- \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
- Bob says Permitted $($File, write$)$\\
- $slev($File$)$ $=$ $T\!S$\\
- $slev($Bob$)$ $=$ $S$\\
- $slev(P) < slev(S)$\\
- $slev(S) < slev(T\!S)$
- \end{tabular}\\
- \hline
- Permitted $($File, write$)$
- \end{tabular}
- \end{center}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Point to Take Home}
-
-\begin{itemize}
-\item Formal methods can be an excellent way of finding
-bugs as they force the designer
-to make everything explicit and thus confront difficult design
-choices that might otherwise be fudged.
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
\end{document}
%%% Local Variables: