slides07.tex
author Christian Urban <urbanc@in.tum.de>
Tue, 13 Nov 2012 04:50:22 +0000
changeset 65 8d3c4efb91b3
child 66 2895a7550754
permissions -rw-r--r--
added
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t]{beamer}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
\usepackage{proof}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
\usepackage{beamerthemeplainculight}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
\usepackage[T1]{fontenc}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
\usepackage[latin1]{inputenc}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
\usepackage{mathpartir}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
\usepackage{isabelle}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
\usepackage{isabellesym}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
\usepackage[absolute,overlay]{textpos}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
\usepackage{ifthen}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
\usepackage{tikz}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
\usepackage{courier}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
\usepackage{listings}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
\usetikzlibrary{arrows}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
\usetikzlibrary{positioning}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
\usetikzlibrary{calc}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
\usepackage{graphicx} 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
\isabellestyle{rm}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
\renewcommand{\isastyle}{\rm}%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
\renewcommand{\isastyleminor}{\rm}%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
\renewcommand{\isatagproof}{}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
\renewcommand{\endisatagproof}{}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
\renewcommand{\isamarkupcmt}[1]{#1}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
% Isabelle characters
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
\renewcommand{\isacharunderscore}{\_}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
\renewcommand{\isacharbar}{\isamath{\mid}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
\renewcommand{\isasymiota}{}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
\renewcommand{\isacharbraceleft}{\{}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
\renewcommand{\isacharbraceright}{\}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
\renewcommand{\isacharless}{$\langle$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
\renewcommand{\isachargreater}{$\rangle$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
\renewcommand{\isasymsharp}{\isamath{\#}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
\renewcommand{\isasymdots}{\isamath{...}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
\renewcommand{\isasymbullet}{\act}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
\definecolor{javared}{rgb}{0.6,0,0} % for strings
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
\lstset{language=Java,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
	basicstyle=\ttfamily,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
	stringstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
	commentstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
	numbers=left,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
	numberstyle=\tiny\color{black},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
	stepnumber=1,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
	numbersep=10pt,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
	tabsize=2,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
	showspaces=false,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
	showstringspaces=false}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
\lstdefinelanguage{scala}{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
  morekeywords={abstract,case,catch,class,def,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
    do,else,extends,false,final,finally,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
    for,if,implicit,import,match,mixin,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
    new,null,object,override,package,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
    private,protected,requires,return,sealed,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
    super,this,throw,trait,true,try,%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
    type,val,var,while,with,yield},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
  otherkeywords={=>,<-,<\%,<:,>:,\#,@},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
  sensitive=true,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
  morecomment=[l]{//},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
  morecomment=[n]{/*}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
  morestring=[b]",
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
  morestring=[b]',
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
  morestring=[b]"""
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
\lstset{language=Scala,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
	basicstyle=\ttfamily,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
	keywordstyle=\color{javapurple}\bfseries,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
	stringstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
	commentstyle=\color{javagreen},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
	morecomment=[s][\color{javadocblue}]{/**}{*/},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
	numbers=left,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
	numberstyle=\tiny\color{black},
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
	stepnumber=1,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
	numbersep=10pt,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
	tabsize=2,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
	showspaces=false,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
	showstringspaces=false}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
% beamer stuff 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
\renewcommand{\slidecaption}{APP 07, King's College London, 13 November 2012}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
\begin{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
\begin{frame}<1>[t]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
\frametitle{%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
  \begin{tabular}{@ {}c@ {}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
  \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
  \LARGE Access Control and \\[-3mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
  \LARGE Privacy Policies (7)\\[-6mm] 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
  \end{tabular}}\bigskip\bigskip\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
  %\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
  %\includegraphics[scale=1.3]{pics/barrier.jpg}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
  %\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
\normalsize
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
  \begin{tabular}{ll}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
  Email:  & christian.urban at kcl.ac.uk\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
  Of$\!$fice: & S1.27 (1st floor Strand Building)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
  Slides: & KEATS (also homework is there)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
\frametitle{Judgements}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
\begin{tikzpicture}[scale=1]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
  \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
  \onslide<2->{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
  \draw (-1,-0.3) node (X) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
  \draw (-2.0,-2.0) node (Y) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
  \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
  \draw[red, ->, line width = 2mm] (Y) -- (X);
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
  \draw (1.2,-0.1) node (X1) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
  \draw (2.8,-0.1) node (Y1) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
  \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
  \draw[red, ->, line width = 2mm] (Y1) -- (X1);
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
  \draw (-0.1,0.1) node (X2) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
  \draw (0.5,1.5) node (Y2) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
  \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
  \draw[red, ->, line width = 2mm] (Y2) -- (X2);}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
  \end{tikzpicture}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
\pause\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
\footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic) 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
\frametitle{Inference Rules}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
\begin{tikzpicture}[scale=1]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
  \draw (0.0,0.0) node 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
  {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
  \draw (-0.1,-0.7) node (X) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
  \draw (-0.1,-1.9) node (Y) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
  \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
  \draw[red, ->, line width = 2mm] (Y) -- (X);
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
  \draw (-1,0.6) node (X2) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
  \draw (0.0,1.6) node (Y2) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
  \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
  \draw[red, ->, line width = 2mm] (Y2) -- (X2);
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
   \draw (1,0.6) node (X3) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
  \draw (0.0,1.6) node (Y3) {};
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
  \draw[red, ->, line width = 2mm] (Y3) -- (X3);
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
  \end{tikzpicture}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
\frametitle{Trusted Third Party}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
Simple protocol for establishing a secure connection via a mutually
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
trusted 3rd party (server):
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
\end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
  \frametitle{Encrypted Messages}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
  \begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
  \item Alice sends a message \bl{$m$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
  \bl{Alice says $m$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
  \end{center}\medskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
  \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
  \bl{Alice says $\{m\}_K$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
  \end{center}\medskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
  \item Decryption of Alice's message\smallskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
  \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
              {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
  \end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   233
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   234
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   235
  \frametitle{Encryption}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   236
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
  \begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
  \item Encryption of a message\smallskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   240
  \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   241
              {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   242
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
  \end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   244
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   245
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   246
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   247
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   248
    
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   249
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   250
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   251
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   252
  \frametitle{Trusted Third Party}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   253
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   254
  \begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   255
  \item Alice calls Sam for a key to communicate with Bob
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   256
  \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   257
  \item Alice sends the message encrypted with the key and the second key it recieved
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   258
  \end{itemize}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   259
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   260
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   261
  \bl{\begin{tabular}{lcl}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   262
  $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   263
  $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   264
  $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   265
  $A$ sends $B$ &:& $\{m\}_{K_{AB}}$
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   266
  \end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   267
  \end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   268
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   269
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   270
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   271
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   273
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   274
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   275
  \frametitle{Sending Rule}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   276
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
  \bl{\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
  \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   279
              {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
  \end{center}}\bigskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   281
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   282
  \bl{$P \,\text{sends}\, Q : F \dn$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   283
  \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   284
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   286
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   287
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   288
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   289
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   290
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   291
  \frametitle{Trusted Third Party}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   292
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   293
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   294
  \bl{\begin{tabular}{l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   295
  $A$ sends $S$ : $\textit{Connect}(A,B)$\\  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   296
  \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   297
  \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   298
  \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   299
 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   300
  $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   301
  $A$ sends $B$ : $\{m\}_{K_{AB}}$
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   302
  \end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   303
  \end{center}\bigskip\pause
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   304
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
  \bl{$\Gamma \vdash B \,\text{says} \, m$}?
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   309
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   311
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
  \frametitle{Challenge-Response Protocol}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
 \begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
 \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
 \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
 \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
 \item if \bl{$E$} receives  \bl{$\{N\}_K$} from \bl{$T$} then starts engine
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
 \end{itemize}	
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
  \mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
  \begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
  \frametitle{Challenge-Response Protokol}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
  \begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
  \bl{\begin{tabular}{l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
  $E \;\text{says}\; N$\hfill(start)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
  $E \;\text{sends}\; T : N$\hfill(challenge)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
  $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
  \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
 $T \;\text{says}\; K$\hfill(key)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
 $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
  $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
   \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
  \end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
  \end{center}\bigskip 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
  \bl{$\Gamma \vdash \text{start\_engine}(T)$}?
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   344
  \end{frame}}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
     
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
\end{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
%%% Local Variables:  
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
%%% mode: latex
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
%%% TeX-master: t
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
%%% End: 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353