# HG changeset patch # User Christian Urban # Date 1417487377 0 # Node ID 0e78c809b17f7170ca7544508cabdf16c7aef034 # Parent f1491e0d7be0acf55887182a086e9af878fd774a updated diff -r f1491e0d7be0 -r 0e78c809b17f handouts/ho08.pdf Binary file handouts/ho08.pdf has changed diff -r f1491e0d7be0 -r 0e78c809b17f handouts/ho08.tex --- a/handouts/ho08.tex Mon Dec 01 06:50:25 2014 +0000 +++ b/handouts/ho08.tex Tue Dec 02 02:29:37 2014 +0000 @@ -44,7 +44,7 @@ \noindent is signed by Satoshi Nakamoto, which however is likely only a pen name. There is a lot of speculation who could be the inventor, or inventors, but we simply do not -know. This part of Bitcoins is definitely anonymous. The paper +know. This part of Bitcoins is definitely anonymous so far. The paper above is from the end of 2008; the first Bitcoin transaction was made in January 2009. The rules in Bitcoin are set up so that there will only ever be 21 Million Bitcoins with the @@ -77,8 +77,8 @@ already used addresses. If you start with a random number to generate a public-private key pair it is very unlikely that you step on somebody else's shoes. Compare this with the -email-addresses you always wanted to register with, say -Gmail, but which are already taken. +email-addresses you wanted to register with, say +Gmail, but which are always already taken. One major difference between Bitcoins and traditional banking is that you do not have a place, or places, that record the @@ -143,7 +143,7 @@ \noindent But for this banks would need to be trusted and would also be an easy target for any government interference, for example. Think of the early days of music sharing where -the company Napster was the single point of ``failure'' which +the company Napster was the trusted third-party but also the single point of ``failure'' which was taken offline by law enforcement. Bitcoins is more like a system such as BitTorrent without a single central entity that can be taken offline.\footnote{There is some Bitcoin @@ -151,9 +151,9 @@ for example Bitcoin exchanges, HQs of Bitcoin mining pools, Bitcoin developers and so on.} -Bitcoin solves the problem of not being able to rely on a bank +Bitcoins solve the problem of not being able to rely on a bank by making everybody the ``bank''. Everybody who cares can have -the entire transactions history starting with the first +the entire transaction history starting with the first transaction made in January 2009. This history of transactions is called the \emph{blockchain}. Bob, for example, can use his copy of the blockchain for determining whether Alice owned the @@ -220,7 +220,7 @@ Consider again the rightmost transactions in Figure~\ref{txngraph} and suppose Alice is a coffeeshop owner selling coffees for 1 Bitcoin. Charles received a transaction -from Zack over 5 Bitcoins, say. How does he pay for the +from Zack over 5 Bitcoins, say. How does Charles pay for the coffee? There is no explicit notion of \emph{change} in the Bitcoin system. What Charles has to do instead is to make one single transaction with 1 Bitcoin to Alice and with 4 Bitcoins @@ -252,7 +252,7 @@ I think this is a good time for you to pause to let this concept of transactions to really sink in\ldots{}You should -see that there is really no need for a central ledger and no +come to the conclusion that there is really no need for a central ledger and no need for an account balance as familiar from traditional banking. The closest what Bitcoin has to offer for the notion of a balance in a bank account are the unspend transactions diff -r f1491e0d7be0 -r 0e78c809b17f slides/slides05.tex --- a/slides/slides05.tex Mon Dec 01 06:50:25 2014 +0000 +++ b/slides/slides05.tex Tue Dec 02 02:29:37 2014 +0000 @@ -424,12 +424,12 @@ \frametitle{Car Transponder (HiTag2)} \begin{enumerate} -\item \bl{$C$} generates a random number \bl{$r$} -\item \bl{$C$} calculates \bl{$(F,G) = \{r\}_K$} -\item \bl{$C \to T$}: \bl{$r, F$} -\item \bl{$T$} calculates \bl{$(F',G') = \{r\}_K$} +\item \bl{$C$} generates a random number \bl{$N$} +\item \bl{$C$} calculates \bl{$(F,G) = \{N\}_K$} +\item \bl{$C \to T$}: \bl{$N, F$} +\item \bl{$T$} calculates \bl{$(F',G') = \{N\}_K$} \item \bl{$T$} checks that \bl{$F = F'$} -\item \bl{$T \to C$}: \bl{$r, G'$} +\item \bl{$T \to C$}: \bl{$N, G'$} \item \bl{$C$} checks that \bl{$G = G'$} \end{enumerate}\pause diff -r f1491e0d7be0 -r 0e78c809b17f slides/slides10.pdf Binary file slides/slides10.pdf has changed diff -r f1491e0d7be0 -r 0e78c809b17f slides/slides10.tex --- a/slides/slides10.tex Mon Dec 01 06:50:25 2014 +0000 +++ b/slides/slides10.tex Tue Dec 02 02:29:37 2014 +0000 @@ -1,47 +1,10 @@ \documentclass[dvipsnames,14pt,t]{beamer} -\usepackage{proof} -\usepackage{beamerthemeplaincu} -\usepackage{mathpartir} -\usepackage{isabelle} -\usepackage{isabellesym} -\usepackage[absolute,overlay]{textpos} -\usepackage{ifthen} -\usepackage{tikz} -\usepackage{courier} -\usepackage{listings} -\usetikzlibrary{arrows} -\usetikzlibrary{positioning} -\usetikzlibrary{calc} -\usepackage{graphicx} -\usetikzlibrary{shapes} -\usetikzlibrary{shadows} -\usetikzlibrary{plotmarks} -\setmonofont[Scale=MatchLowercase]{Consolas} -\newfontfamily{\consolas}{Consolas} - -\isabellestyle{rm} -\renewcommand{\isastyle}{\rm}% -\renewcommand{\isastyleminor}{\rm}% -\renewcommand{\isastylescript}{\footnotesize\rm\slshape}% -\renewcommand{\isatagproof}{} -\renewcommand{\endisatagproof}{} -\renewcommand{\isamarkupcmt}[1]{#1} - -% Isabelle characters -\renewcommand{\isacharunderscore}{\_} -\renewcommand{\isacharbar}{\isamath{\mid}} -\renewcommand{\isasymiota}{} -\renewcommand{\isacharbraceleft}{\{} -\renewcommand{\isacharbraceright}{\}} -\renewcommand{\isacharless}{$\langle$} -\renewcommand{\isachargreater}{$\rangle$} -\renewcommand{\isasymsharp}{\isamath{\#}} -\renewcommand{\isasymdots}{\isamath{...}} -\renewcommand{\isasymbullet}{\act} +\usepackage{../slides} +\usepackage{../langs} +\usepackage{../graphics} % beamer stuff -\renewcommand{\slidecaption}{APP 09, King's College London, 10 December 2013} -\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions +\renewcommand{\slidecaption}{APP 10, King's College London} \newcommand{\bl}[1]{\textcolor{blue}{#1}} \begin{document} @@ -302,155 +265,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile,t] -\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}} - -Bell-LaPadula access model: - - \begin{itemize} - \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if - \bl{$P$}'s security level is at least as high as \bl{$O$}'s. - \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if - \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip - - \item Meta-Rule: All principals in a system should have a sufficiently high security level - in order to access an object. - \end{itemize}\bigskip - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile,t] -\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}} - -Biba (data integrity) - - \begin{itemize} - \item Biba: {\bf `no read down'} - {\bf `no write up'} - \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if - \bl{$P$}'s security level is lower or equal than \bl{$O$}'s. - \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if - \bl{$O$}'s security level is lower or equal than \bl{$P$}'s. - \end{itemize} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile,t] -\frametitle{\begin{tabular}{c}4th Lecture:\\ Protocols\end{tabular}} - -A mutual authentication protocol - -\begin{center} -\begin{tabular}{ll} -\bl{$A \rightarrow B$:} & \bl{$N_a$}\\ -\bl{$B \rightarrow A$:} & \bl{$\{N_a, N_b\}_{K_{ab}}$}\\ -\bl{$A \rightarrow B$:} & \bl{$N_b$}\\ -\end{tabular} -\end{center} - - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile,t] -\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}} - - -\begin{itemize} -\item formulas -\item judgements -\end{itemize}\pause - -\begin{center} - \begin{tikzpicture}[scale=1] - - \draw[line width=1mm] (-.3, 0) rectangle (1.5,2); - \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}}; - \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}}; - \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}}; - - \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); - \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1); - \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); - - \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}}; - - \end{tikzpicture} -\end{center} - - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile,t] -\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}} - -\begin{center} -\begin{tikzpicture}[scale=1] - - \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}}; - \onslide<1->{ - \draw (-1,-0.3) node (X) {}; - \draw (-2.0,-2.0) node (Y) {}; - \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}}; - \draw[red, ->, line width = 2mm] (Y) -- (X); - - \draw (1.2,-0.1) node (X1) {}; - \draw (2.8,-0.1) node (Y1) {}; - \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}}; - \draw[red, ->, line width = 2mm] (Y1) -- (X1); - - \draw (-0.1,0.1) node (X2) {}; - \draw (0.5,1.5) node (Y2) {}; - \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}}; - \draw[red, ->, line width = 2mm] (Y2) -- (X2);} - - \end{tikzpicture} -\end{center} - - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\mode{ -\begin{frame}[c] -\frametitle{\begin{tabular}{c}5th Lecture:\\ Inference Rules\end{tabular}} - - -\begin{center} -\begin{tikzpicture}[scale=1] - - \draw (0.0,0.0) node - {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}}; - - \draw (-0.1,-0.7) node (X) {}; - \draw (-0.1,-1.9) node (Y) {}; - \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}}; - \draw[red, ->, line width = 2mm] (Y) -- (X); - - \draw (-1,0.6) node (X2) {}; - \draw (0.0,1.6) node (Y2) {}; - \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}}; - \draw[red, ->, line width = 2mm] (Y2) -- (X2); - \draw (1,0.6) node (X3) {}; - \draw (0.0,1.6) node (Y3) {}; - \draw[red, ->, line width = 2mm] (Y3) -- (X3); - \end{tikzpicture} -\end{center} - - -\end{frame}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] \frametitle{\begin{tabular}{c}8th Lecture: Privacy\end{tabular}}