52
+ − 1
\documentclass[dvipsnames,14pt,t]{beamer}
+ − 2
\usepackage{proof}
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 3
\usepackage{beamerthemeplaincu}
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 4
\usepackage{fontenc}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 5
\usepackage[latin1]{inputenc}
52
+ − 6
\usepackage{mathpartir}
+ − 7
\usepackage{isabelle}
+ − 8
\usepackage{isabellesym}
+ − 9
\usepackage[absolute,overlay]{textpos}
+ − 10
\usepackage{ifthen}
+ − 11
\usepackage{tikz}
+ − 12
\usepackage{courier}
+ − 13
\usepackage{listings}
+ − 14
\usetikzlibrary{arrows}
+ − 15
\usetikzlibrary{positioning}
+ − 16
\usetikzlibrary{calc}
+ − 17
\usepackage{graphicx}
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 18
\setmonofont{Consolas}
52
+ − 19
+ − 20
\isabellestyle{rm}
+ − 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}
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 39
\newcommand{\isaliteral}[1]{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 40
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
52
+ − 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
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 47
\makeatletter
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 48
\lst@CCPutMacro\lst@ProcessOther {"2D}{\lst@ttfamily{-{}}{-{}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 49
\@empty\z@\@empty
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 50
\makeatother
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 51
52
+ − 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
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 70
\lstdefinelanguage{while}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 71
morekeywords={while, if, then. else, read, write},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 72
otherkeywords={=>,<-,<\%,<:,>:,\#,@},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 73
sensitive=true,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 74
morecomment=[l]{//},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 75
morecomment=[n]{/*}{*/},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 76
morestring=[b]",
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 77
morestring=[b]',
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 78
morestring=[b]"""
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 79
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 81
52
+ − 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}
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 95
52
+ − 96
+ − 97
% beamer stuff
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 98
\renewcommand{\slidecaption}{APP 05, King's College London, 29 October 2013}
52
+ − 99
+ − 100
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+ − 101
\begin{document}
+ − 102
+ − 103
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 104
\mode<presentation>{
+ − 105
\begin{frame}<1>[t]
+ − 106
\frametitle{%
+ − 107
\begin{tabular}{@ {}c@ {}}
+ − 108
\\
+ − 109
\LARGE Access Control and \\[-3mm]
+ − 110
\LARGE Privacy Policies (5)\\[-6mm]
+ − 111
\end{tabular}}\bigskip\bigskip\bigskip
+ − 112
+ − 113
%\begin{center}
+ − 114
%\includegraphics[scale=1.3]{pics/barrier.jpg}
+ − 115
%\end{center}
+ − 116
+ − 117
\normalsize
+ − 118
\begin{center}
+ − 119
\begin{tabular}{ll}
+ − 120
Email: & christian.urban at kcl.ac.uk\\
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 121
Office: & S1.27 (1st floor Strand Building)\\
52
+ − 122
Slides: & KEATS (also homework is there)\\
+ − 123
\end{tabular}
+ − 124
\end{center}
+ − 125
+ − 126
+ − 127
\end{frame}}
+ − 128
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 129
+ − 130
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 131
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 132
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 133
\frametitle{Last Week}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 135
\mbox{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 137
\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 138
{\Large \bl{$A\;\rightarrow\; B : \ldots$}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 139
\onslide<1->{\Large \bl{$B\;\rightarrow\; A : \ldots$}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 140
\onslide<1->{\Large \;\;\;\;\;\bl{$:$}}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 141
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 142
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 143
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 144
\item by convention \bl{$A$}, \bl{$B$} are named principals \bl{Alice\ldots}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 145
but most likely they are programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 146
\item indicates one ``protocol run'', or session, which specifies an
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 147
order in the communication
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 148
\item there can be several sessions in parallel (think of wifi routers)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 149
\item nonces (randomly generated numbers) used only once
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 150
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 151
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 152
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 153
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 154
52
+ − 155
+ − 156
+ − 157
+ − 158
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 159
\mode<presentation>{
+ − 160
\begin{frame}[c]
54
+ − 161
\frametitle{Cryptographic Protocol Failures}
+ − 162
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 163
Ross Anderson and Roger Needham wrote:\bigskip
54
+ − 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
52
+ − 174
+ − 175
\end{frame}}
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 176
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 177
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 178
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 179
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 180
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 181
\frametitle{Protocols}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 182
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 183
Examples where ``over-the-air'' protocols are used
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 184
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 185
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 186
\item wifi
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 187
\item card readers (you cannot trust the terminals)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 188
\item RFI (passports)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 189
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 190
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 191
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 192
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 193
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 194
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 195
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 196
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 198
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 199
\includegraphics[scale=0.5]{pics/dogs.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 200
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 203
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 204
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 205
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 206
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 208
\frametitle{\begin{tabular}{c}Chip-and-PIN\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 209
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 210
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 211
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 212
\item A ``tamperesitant'' terminal playing Tetris on
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 213
\textcolor{blue}{\href{http://www.youtube.com/watch?v=wWTzkD9M0sU}{youtube}}.\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 214
\textcolor{lightgray}{\footnotesize(\url{http://www.youtube.com/watch?v=wWTzkD9M0sU})}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 215
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 217
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 218
\includegraphics[scale=0.2]{pics/tetris.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 219
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 220
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 221
\end{frame}}
52
+ − 222
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 223
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 224
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 225
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 226
\begin{frame}<1-3>[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 227
\frametitle{Oyster Cards}
52
+ − 228
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 229
\includegraphics[scale=0.4]{pics/oysterc.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 230
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 231
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 232
\item good example of a bad protocol\\ (security by obscurity)\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 233
\item<3-> ``Breaching security on Oyster cards should not
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 234
allow unauthorised use for more than a day, as TfL promises to turn
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 235
off any cloned cards within 24 hours\ldots''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 236
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 237
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 238
\only<2>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 239
\begin{textblock}{12}(0.5,0.5)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 240
\begin{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 241
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 242
{\color{darkgray}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 243
\begin{minipage}{11cm}\raggedright\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 244
{\bf Wirelessly Pickpocketing a Mifare Classic Card}\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 245
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 246
The Mifare Classic is the most widely used contactless smartcard on the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 247
market. The stream cipher CRYPTO1 used by the Classic has recently been
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 248
reverse engineered and serious attacks have been proposed. The most serious
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 249
of them retrieves a secret key in under a second. In order to clone a card,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 250
previously proposed attacks require that the adversary either has access to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 251
an eavesdropped communication session or executes a message-by-message
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 252
man-in-the-middle attack between the victim and a legitimate
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 253
reader. Although this is already disastrous from a cryptographic point of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 254
view, system integrators maintain that these attacks cannot be performed
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 255
undetected.\smallskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 256
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 257
This paper proposes four attacks that can be executed by an adversary having
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 258
only wireless access to just a card (and not to a legitimate reader). The
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 259
most serious of them recovers a secret key in less than a second on ordinary
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 260
hardware. Besides the cryptographic weaknesses, we exploit other weaknesses
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 261
in the protocol stack. A vulnerability in the computation of parity bits
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 262
allows an adversary to establish a side channel. Another vulnerability
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 263
regarding nested authentications provides enough plaintext for a speedy
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 264
known-plaintext attack.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 265
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 266
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 267
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 269
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 270
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 271
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 272
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 273
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 274
\begin{frame}<1->[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 275
\frametitle{Another Example}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 276
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 277
In an email from Ross Anderson\bigskip\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 278
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 279
\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 280
From: Ross Anderson <Ross.Anderson@cl.cam.ac.uk>\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 281
Sender: cl-security-research-bounces@lists.cam.ac.uk\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 282
To: cl-security-research@lists.cam.ac.uk\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 283
Subject: Birmingham case\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 284
Date: Tue, 13 Aug 2013 15:13:17 +0100\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 285
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 287
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 288
\only<2>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 289
\begin{textblock}{12}(0.5,0.5)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 290
\begin{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 291
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 292
{\color{darkgray}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 293
\begin{minipage}{11cm}\raggedright\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
As you may know, Volkswagen got an injunction against the University of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 295
Birmingham suppressing the publication of the design of a weak cipher
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 296
used in the remote key entry systems in its recent-model cars. The paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 297
is being given today at Usenix, minus the cipher design.\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 298
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 299
I've been contacted by Birmingham University's lawyers who seek to prove
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 300
that the cipher can be easily obtained anyway. They are looking for a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 301
student who will download the firmware from any newish VW, disassemble
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 302
it and look for the cipher. They'd prefer this to be done by a student
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 303
rather than by a professor to emphasise how easy it is.\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 304
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 305
Volkswagen's argument was that the Birmingham people had reversed a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 306
locksmithing tool produced by a company in Vietnam, and since their key
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 307
fob chip is claimed to be tamper-resistant, this must have involved a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 308
corrupt insider at VW or at its supplier Thales. Birmingham's argument
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 309
is that this is nonsense as the cipher is easy to get hold of. Their
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 310
lawyers feel this argument would come better from an independent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 311
outsider.\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 312
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 313
Let me know if you're interested in having a go, and I'll put you in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 314
touch
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 315
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 316
Ross
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 317
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 318
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 319
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 320
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 321
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 322
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 323
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 324
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 325
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 326
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 327
\frametitle{Authentication Protocols}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 328
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 329
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 330
Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 331
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 332
Passwords:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 333
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 334
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 335
\bl{$B \rightarrow A: K_{AB}$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 336
\end{center}\pause\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 337
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 338
Problems: Eavesdropper can capture the secret and replay it; \bl{$A$} cannot confirm the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 339
identity of \bl{$B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 340
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 341
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 342
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
52
+ − 343
+ − 344
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 345
\mode<presentation>{
+ − 346
\begin{frame}[c]
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 347
\frametitle{Authentication Protocols}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 348
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 349
Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 351
Simple Challenge Response:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 352
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 353
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 354
\begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 355
\bl{$A \rightarrow B:$} & \bl{$N$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 356
\bl{$B \rightarrow A:$} & \bl{$\{N\}_{K_{AB}}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 357
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 358
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 359
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 360
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 361
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 362
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
52
+ − 363
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 364
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 365
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 366
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 367
\frametitle{Authentication Protocols}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 368
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 369
Alice (\bl{$A$}) and Bob (\bl{$B$}) share a secret key \bl{$K_{AB}$}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 370
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 371
Mutual Challenge Response:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 372
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 373
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 374
\begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 375
\bl{$A \rightarrow B:$} & \bl{$N_A$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 376
\bl{$B \rightarrow A:$} & \bl{$\{N_A, N_B\}_{K_{AB}}$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 377
\bl{$A \rightarrow B:$} & \bl{$N_B$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 378
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 379
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 380
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 381
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 382
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 383
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 384
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 385
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 386
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 387
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 388
\frametitle{One Time Passwords}
52
+ − 389
+ − 390
\begin{center}
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 391
\bl{$B \rightarrow A: C, C_{K_{AB}}$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 392
\end{center}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 393
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 394
A counter \bl{$C$} increases with each transmission; \bl{$A$} will not accept a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395
\bl{$C$} which has already been accepted (used in car key fob).
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 396
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 397
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 399
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 400
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 401
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 402
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 403
\frametitle{Person-in-the-Middle}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 404
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 405
``Normal'' protocol run:\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 406
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 407
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 408
\item \bl{$A$} sends public key to \bl{$B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 409
\item \bl{$B$} sends public key to \bl{$A$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 410
\item \bl{$A$} sends message encrypted with \bl{$B$}'s public key, \bl{$B$} decrypts it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 411
with its private key
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 412
\item \bl{$B$} sends message encrypted with \bl{$A$}'s public key, \bl{$A$} decrypts it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 413
with its private key
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 414
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 415
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 416
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 417
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 418
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 419
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 420
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 421
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 422
\frametitle{Person-in-the-Middle}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 423
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 424
Attack:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 425
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 426
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 427
\item \bl{$A$} sends public key to \bl{$B$} --- \bl{$C$} intercepts this message and send his own public key
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 428
\item \bl{$B$} sends public key to \bl{$A$} --- \bl{$C$} intercepts this message and send his own public key
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 429
\item \bl{$A$} sends message encrypted with \bl{$C$}'s public key, \bl{$C$} decrypts it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 430
with its private key, re-encrypts with \bl{$B$}'s public key
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 431
\item similar
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 432
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 433
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 434
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 435
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 436
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 437
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 438
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 439
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 440
\frametitle{Person-in-the-Middle}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 441
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 442
Prevention:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 443
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 444
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 445
\item \bl{$A$} sends public key to \bl{$B$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 446
\item \bl{$B$} sends public key to \bl{$A$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 447
\item \bl{$A$} encrypts message with \bl{$B$}'s public key, send's {\bf half} of the message
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 448
\item \bl{$B$} encrypts message with \bl{$A$}'s public key, send's {\bf half} of the message
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 449
\item \bl{$A$} sends other half, \bl{$B$} can now decrypt entire message
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 450
\item \bl{$B$} sends other half, \bl{$A$} can now decrypt entire message
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 451
\end{itemize}\pause
52
+ − 452
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 453
\bl{$C$} would have to invent a totally new message
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 454
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 455
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 456
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 457
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 458
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 459
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 460
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 461
\frametitle{Motivation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 462
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 463
The ISO/IEC 9798 specifies authentication mechanisms which use security
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 464
techniques. These mechanisms are used to corroborate that an entity is the one
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 465
that is claimed. An entity to be authenticated proves its identity by showing its
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 466
knowledge of a secret. The mechanisms are defined as exchanges of information
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 467
between entities and, where required, exchanges with a trusted third party.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 468
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 469
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 470
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 471
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 472
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 473
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 474
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 475
\frametitle{Motivation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 476
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 477
But\ldots\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 478
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 479
The ISO/IEC 9798 standard neither specifies a threat model nor defines the security properties that the protocols should satisfy.\pause\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 480
Unfortunately, there are no general precise definitions for the goals of protocols.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 481
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 482
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 483
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 484
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 485
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 486
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 487
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 488
\frametitle{Best Practices}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 489
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 490
{\bf Principle 1:} Every message should say what it means: the interpretation of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 491
a message should not depend on the context.\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 492
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 493
{\bf Principle 2:} If the identity of a principal is essential to the meaning of a message, it is prudent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 494
to mention the principal’s name explicitly in the message (though difficult).\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 495
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 496
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 497
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 498
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 499
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 500
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 501
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 502
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 503
\frametitle{Best Practices}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 504
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 505
{\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.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 506
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 507
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 508
Possible Uses of Encryption
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 509
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 510
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 511
\item Preservation of confidentiality: \bl{$\{X\}_K$} only those that have \bl{$K$} may recover \bl{$X$}.
\item Guarantee authenticity: The partner is indeed some particular principal.
\item Guarantee confidentiality and authenticity: binds two parts of a message ---
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 512
\bl{$\{X,Y\}_K$} is not the same as \bl{$\{X\}_K$} and \bl{$\{Y\}_K$}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 513
\end{itemize}
52
+ − 514
\end{center}
+ − 515
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 516
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 517
52
+ − 518
\end{frame}}
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 519
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 520
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 521
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 522
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 523
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 524
\frametitle{Best Practices}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 525
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 526
{\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
52
+ − 527
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 528
Example Certification Authorities: CAs are trusted to certify a key only after proper steps
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 529
have been taken to identify the principal that owns it.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 530
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 531
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 532
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 533
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 534
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 535
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 536
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
52
+ − 537
+ − 538
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 539
\mode<presentation>{
+ − 540
\begin{frame}[c]
+ − 541
\frametitle{Access Control Logic}
+ − 542
+ − 543
Ross Anderson about the use of Logic:\bigskip
+ − 544
+ − 545
\begin{quote}
+ − 546
Formal methods can be an excellent way of finding
+ − 547
bugs in security protocol designs as they force the designer
53
+ − 548
to make everything explicit and thus confront dif$\!$ficult design
52
+ − 549
choices that might otherwise be fudged.
+ − 550
\end{quote}
+ − 551
+ − 552
\end{frame}}
+ − 553
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 554
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 555
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 556
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 557
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 558
\frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 559
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 560
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 561
\item Formulas
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 562
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 563
\begin{center}\color{blue}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 564
\begin{tabular}{rcl@ {\hspace{10mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 565
\isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 566
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 567
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 568
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 569
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F} & \textcolor{black}{implies}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 570
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F} & \textcolor{black}{negation}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 571
& \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}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 572
& \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 573
\onslide<2->{\textcolor{black}{forall quantification}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 574
& \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 575
\onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 576
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 577
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 578
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 579
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 580
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 581
\begin{textblock}{12}(1,14)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 582
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}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 583
\end{textblock}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 584
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 585
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 586
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 587
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 588
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 589
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 590
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 591
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 592
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
{\lstset{language=Scala}\fontsize{10}{12}\selectfont
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 594
\texttt{\lstinputlisting{../programs/formulas.scala}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 595
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 596
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 597
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 598
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 599
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 600
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 601
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 602
\frametitle{Judgements}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 603
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 604
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 605
\LARGE
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 606
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 607
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 608
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 609
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 610
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 611
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 612
\item Example\mbox{}\\[-3mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 613
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 614
\only<2>{\begin{center}\tiny
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 615
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 616
\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 617
\isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 618
\isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 619
\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}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 620
\end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 621
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 622
\only<3>{\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 623
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 624
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 625
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 626
\infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 627
{\mbox{\begin{tabular}{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 628
\isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 629
\isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 630
\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}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 631
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 632
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 633
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 634
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 635
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
\only<4>{\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 637
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 638
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 639
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 640
\infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 641
{\mbox{\begin{tabular}{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
\isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
\isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 644
\isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 645
\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}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 646
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 647
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 648
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 649
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 650
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 651
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 653
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 654
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 655
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 656
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 657
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 658
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 659
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 660
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 661
{\lstset{language=Scala}\fontsize{10}{12}\selectfont
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 662
\texttt{\lstinputlisting{../programs/judgement.scala}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 663
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 664
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 665
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 666
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 667
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 668
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 669
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 670
\frametitle{Inference Rules}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 671
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 672
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 673
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 674
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 675
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 676
\infer{\mbox{\isa{conclusion}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 677
{\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 678
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 679
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 680
The conlusion and premises are judgements\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 681
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 682
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 683
\item Examples
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 684
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 685
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 686
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 687
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 688
{\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}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 689
\end{center}}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 690
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 691
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 692
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 693
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 694
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 695
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 696
\hspace{10mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 697
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 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}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 699
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 700
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 701
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 702
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 703
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 704
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 705
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 706
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 707
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 708
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 709
\frametitle{Implication}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 710
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 711
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 712
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 713
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 714
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 715
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 716
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 717
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 718
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 719
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 720
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 721
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 722
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 723
{\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}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 724
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 725
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 726
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 727
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 728
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 729
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 730
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 731
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 732
\frametitle{Universal Quantification}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 733
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 734
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 735
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 736
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 737
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 738
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{$\isacharbrackleft$}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{$\isacharbrackright$}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 739
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 740
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 741
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 742
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 743
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 744
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 745
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 746
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 747
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 748
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 749
\frametitle{Start Rules / Axioms}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 750
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 751
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 752
\alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 753
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 754
\textcolor{blue}{\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 755
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 756
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 757
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 758
\end{center}}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 759
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 760
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 761
Also written as:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 762
\textcolor{blue}{\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 763
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 764
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 765
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 766
\end{center}}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 767
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 768
\textcolor{blue}{\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 769
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 770
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 771
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 772
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 773
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 774
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 775
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 776
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 777
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 778
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 779
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 780
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 781
\frametitle{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 782
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 783
\begin{minipage}{1.1\textwidth}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 784
Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 785
\isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 786
\isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 787
\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}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 788
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 789
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 790
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 791
\only<2>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 792
\begin{textblock}{12}(4,3)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 793
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 794
\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}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 795
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 796
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 797
\only<3->{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 798
\begin{textblock}{12}(4,3)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 799
\mbox{\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 800
\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}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 801
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 802
\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 803
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 804
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 805
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 806
\only<4>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 807
\begin{textblock}{14}(0.5,6)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 808
\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}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 809
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 810
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 811
\only<5->{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 812
\begin{textblock}{14}(0.5,6)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 813
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 814
\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}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 815
\hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 816
{\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}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 817
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 818
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 819
\only<6->{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 820
\begin{textblock}{14}(5,10)\footnotesize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 821
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 822
\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}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 823
{\vdots & \hspace{30mm} \vdots}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 824
\end{textblock}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 825
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 826
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 827
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 828
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 829
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 830
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 831
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 832
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 833
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 834
\frametitle{Access Control}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 835
\Large
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 836
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 837
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 838
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 839
\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 840
\end{center}}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 841
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 842
\normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 843
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 844
\item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 845
\item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 846
\end{itemize}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 847
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 848
\begin{minipage}{1.1\textwidth}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 849
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 850
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 851
\isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 852
\isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 853
\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}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 854
\end{tabular}}\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 855
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 856
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 857
\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 858
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 859
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 860
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 861
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 862
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 863
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 864
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 865
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 866
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 867
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 868
\frametitle{The Access Control Problem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 869
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 870
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 871
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 872
\begin{tikzpicture}[scale=1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 873
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 874
\draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 875
\draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 876
\draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 877
\draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 878
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 879
\draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 880
\draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 881
\draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 882
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 883
\draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 884
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 885
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 886
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 887
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 888
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 889
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 890
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 891
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 892
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 893
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 894
\frametitle{Bad News}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 895
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 896
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 897
\item We introduced (roughly) first-order logic. \bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 898
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 899
\item Judgements
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 900
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 901
\textcolor{blue}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 902
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 903
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 904
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 905
are in general \alert{undecidable}.\pause\medskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 906
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 907
The problem is \alert{semi-decidable}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 908
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 909
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 910
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 911
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 912
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 913
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 914
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 915
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 916
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 917
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 918
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 919
\frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 920
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 921
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 922
\item[]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 923
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 924
\begin{center}\color{blue}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 925
\begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 926
\isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 927
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 928
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 929
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 930
& \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 931
& \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}}} \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 932
& \isa{{\isaliteral{7C}{\isacharbar}}} & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 933
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 934
\end{center}\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 935
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 936
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 937
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 938
\item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 939
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 940
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 941
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 942
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 943
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 944
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 945
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 946
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 947
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 948
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 949
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 950
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 951
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 952
{\lstset{language=Scala}\fontsize{10}{12}\selectfont
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 953
\texttt{\lstinputlisting{../programs/formulas1.scala}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 954
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 955
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 956
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 957
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 958
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 959
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 960
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 961
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 962
\frametitle{Rules about Says}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 963
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 964
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 965
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 966
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 967
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 968
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 969
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 970
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 971
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 972
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 973
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 974
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 975
{\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}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 976
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 977
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 978
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 979
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 980
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 981
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 982
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 983
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 984
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 985
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 986
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 987
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 988
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 989
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 990
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 991
\frametitle{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 992
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 993
Consider the following scenario:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 994
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 995
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 996
\item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 997
should be deleted, then this file must be deleted.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 998
\item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 999
\textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1000
\item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1001
\end{itemize}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1002
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1003
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1004
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1005
\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}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1006
\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}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1007
\isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1008
\end{tabular}}\medskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1009
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1010
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1011
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1012
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1013
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1014
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1015
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1016
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1017
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1018
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1019
\frametitle{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1020
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1021
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1022
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1023
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1024
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1025
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1026
\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1027
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1028
{\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}}}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1029
\end{center}}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1030
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1031
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1032
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1033
\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}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1034
\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}}},\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1035
\isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1036
\end{tabular}}\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1037
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1038
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1039
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1040
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1041
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1042
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1043
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1044
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1045
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1046
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1047
\frametitle{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1048
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1049
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1050
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1051
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1052
\only<1>{$ \underbrace{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1053
\mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1054
{\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1055
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1056
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1057
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1058
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1059
\only<1>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1060
$ \underbrace{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1061
\mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1062
{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1063
&
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1064
\deduce[$\vdots$]{X}{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1065
}}}_{Y}$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1066
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1067
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1068
\textcolor{blue}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1069
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1070
\only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1071
{\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1072
&
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1073
\deduce[$\vdots$]{Y}{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1074
}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1075
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1076
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1077
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1078
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1079
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1080
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1081
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1082
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1083
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1084
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1085
\frametitle{Controls}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1086
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1087
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1088
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1089
\item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1090
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1091
\item its meaning ``\bl{P} is entitled to do \bl{F}''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1092
\item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1093
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1094
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1095
\bl{\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1096
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1097
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1098
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1099
\end{center}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1100
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1101
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1102
\bl{\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1103
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1104
{\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}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1105
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1106
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1107
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1108
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1109
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1110
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1111
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1112
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1113
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1114
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1115
\frametitle{Speaks For}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1116
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1118
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1119
\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}}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1121
\item its meaning ``\bl{P} speaks for \bl{Q}''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1122
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1124
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1125
\bl{\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1126
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1127
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1128
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1129
\end{center}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1131
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1132
\bl{\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1133
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1134
{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1135
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1136
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1137
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1138
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1139
\bl{\mbox{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1140
\infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1141
{\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}}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1142
}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1143
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1144
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1146
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1147
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1148
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1149
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1150
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1151
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1152
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1153
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1154
\frametitle{Security Levels}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1155
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1156
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1157
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1158
\item Top secret (\bl{$T\!S$})
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1159
\item Secret (\bl{$S$})
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1160
\item Public (\bl{$P$})
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1161
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1162
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1163
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1164
\bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1165
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1167
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1168
\item Bob has a clearance for ``secret''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1169
\item Bob can read documents that are public or sectret, but not top secret
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1170
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1171
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1172
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1173
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1174
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1175
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1176
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1177
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1178
\frametitle{Reading a File}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1179
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1180
\bl{\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1181
\begin{tabular}{c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1182
\begin{tabular}{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1183
\only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1184
\only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1185
Bob says Permitted $($File, read$)$\only<2->{\\}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1186
\only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1187
\only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1188
\only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1189
\only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1190
\end{tabular}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1191
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1192
Permitted $($File, read$)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1193
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1194
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1195
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1196
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1197
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1198
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1199
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1200
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1201
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1202
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1203
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1204
\frametitle{Substitution Rule}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1205
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1206
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1207
\bl{\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1208
\begin{tabular}{c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1209
$\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1210
\hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1211
$\Gamma \vdash slev(P) < slev(Q)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1212
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1213
\end{center}}\bigskip\pause
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1214
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1215
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1216
\item \bl{$slev($Bob$)$ $=$ $S$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1217
\item \bl{$slev($File$)$ $=$ $P$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1218
\item \bl{$slev(P) < slev(S)$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1219
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1220
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1221
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1222
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1223
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1224
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1225
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1226
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1227
\frametitle{Reading a File}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1228
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1229
\bl{\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1230
\begin{tabular}{c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1231
\begin{tabular}{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1232
$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1233
\hspace{3cm}Bob controls Permitted $($File, read$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1234
Bob says Permitted $($File, read$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1235
$slev($File$)$ $=$ $P$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1236
$slev($Bob$)$ $=$ $T\!S$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1237
\only<1>{\textcolor{red}{$?$}}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1238
\only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1239
\only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1240
\end{tabular}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1241
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1242
Permitted $($File, read$)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1243
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1244
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1245
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1246
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1247
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1248
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1249
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1250
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1251
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1252
\frametitle{Transitivity Rule}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1253
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1254
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1255
\bl{\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1256
\begin{tabular}{c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1257
$\Gamma \vdash l_1 < l_2$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1258
\hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1259
$\Gamma \vdash l_1 < l_3$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1260
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1261
\end{center}}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1262
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1263
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1264
\item \bl{$slev(P) < slev (S)$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1265
\item \bl{$slev(S) < slev (T\!S)$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1266
\item[] \bl{$slev(P) < slev (T\!S)$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1267
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1269
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1270
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1271
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1272
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1273
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1274
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1275
\frametitle{Reading Files}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1276
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1277
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1278
\item Access policy for reading
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1279
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1280
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1281
\bl{\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1282
\begin{tabular}{c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1283
\begin{tabular}{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1284
$\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1285
\hspace{3cm}Bob controls Permitted $(f$, read$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1286
Bob says Permitted $($File, read$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1287
$slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1288
$slev($Bob$)$ $=$ $T\!S$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1289
$slev(P) < slev(S)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1290
$slev(S) < slev(T\!S)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1291
\end{tabular}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1292
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1293
Permitted $($File, read$)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1294
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1295
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1296
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1297
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1298
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1299
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1300
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1301
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1302
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1303
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1304
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1305
\frametitle{Writing Files}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1306
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1307
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1308
\item Access policy for \underline{writing}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1309
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1310
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1311
\bl{\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1312
\begin{tabular}{c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1313
\begin{tabular}{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1314
$\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1315
\hspace{3cm}Bob controls Permitted $(f$, write$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1316
Bob says Permitted $($File, write$)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1317
$slev($File$)$ $=$ $T\!S$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1318
$slev($Bob$)$ $=$ $S$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1319
$slev(P) < slev(S)$\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1320
$slev(S) < slev(T\!S)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1321
\end{tabular}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1322
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1323
Permitted $($File, write$)$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1324
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1325
\end{center}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1326
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1327
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1328
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1329
%
52
+ − 1330
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1331
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1332
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1333
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1334
\frametitle{Point to Take Home}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1335
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1336
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1337
\item Formal methods can be an excellent way of finding
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1338
bugs as they force the designer
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1339
to make everything explicit and thus confront difficult design
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1340
choices that might otherwise be fudged.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1341
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1342
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1343
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1344
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1345
241
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1346
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1347
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1348
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1349
\frametitle{\begin{tabular}{@ {}c@ {}}Schneier: Step 1\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1351
{\bf What assets are you trying to protect?}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1352
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1353
This question might seem basic, but a surprising number of people never ask it. The question involves understanding the scope of the problem. For example, securing an airplane, an airport, commercial aviation, the transportation system, and a nation against terrorism are all different security problems, and require different solutions.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1354
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1355
\only<2>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1356
\begin{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1357
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1358
{\begin{minipage}{10cm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1359
\small You like to prevent: ``It would be terrible if this sort of attack ever happens; we need to do everything in our power to prevent it.''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1360
\end{minipage}};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1361
\end{tikzpicture}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1362
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1363
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1364
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1365
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1366
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1367
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1368
\frametitle{\begin{tabular}{@ {}c@ {}}Schneier: Step 2\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1369
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1370
{\bf What are the risks to these assets?}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1371
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1372
Here we consider the need for security. Answering it involves understanding what is being defended, what the consequences are if it is successfully attacked, who wants to attack it, how they might attack it, and why.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1373
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1374
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1375
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1376
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1377
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1378
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1379
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1380
\frametitle{\begin{tabular}{@ {}c@ {}}Schneier: Step 3\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1381
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1382
{\bf How well does the security solution mitigate those risks?}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1383
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1384
Another seemingly obvious question, but one that is frequently ignored. If the security solution doesn't solve the problem, it's no good. This is not as simple as looking at the security solution and seeing how well it works. It involves looking at how the security solution interacts with everything around it, evaluating both its operation and its failures.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1385
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1386
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1387
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1388
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1389
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1390
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1391
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1392
\frametitle{\begin{tabular}{@ {}c@ {}}Schneier: Step 4\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1393
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1394
{\bf What other risks does the security solution cause?}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1395
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1396
This question addresses what might be called the problem of unintended consequences. Security solutions have ripple effects, and most cause new security problems. The trick is to understand the new problems and make sure they are smaller than the old ones.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1397
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1398
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1399
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1400
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1401
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1402
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1403
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1404
\frametitle{\begin{tabular}{@ {}c@ {}}Schneier: Step 5\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1405
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1406
{\bf What costs and trade-offs does the security solution impose?}\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1407
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1408
Every security system has costs and requires trade-offs. Most security costs money, sometimes substantial amounts; but other trade-offs may be more important, ranging from matters of convenience and comfort to issues involving basic freedoms like privacy. Understanding these trade-offs is essential.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1409
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1410
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1411
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1412
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1413
52
+ − 1414
\end{document}
+ − 1415
+ − 1416
%%% Local Variables:
+ − 1417
%%% mode: latex
+ − 1418
%%% TeX-master: t
+ − 1419
%%% End:
+ − 1420