
\def\babelopt{english,italian}
%% admissible values: bach, mst, phd.
\documentclass[table,target=mst,babel=\babelopt]{thud}

\title{Fenrir: a verified protocol for federated authentication and authorization}
\author{Luca Fulchir}
\date{2014-2015}
\supervisor{Prof.\ Marino Miculan}
%\cosupervisor{}
%% various: \referee, \chair, \address (default:uniud address).
%% use `\and' in \author, \supervisor, \cosupervisor, \referee to put multiple names
%% phd
%\phdnumber{666}
%\rights{Tutti i diritti riservati a me stesso e basta.}
%\homepage{https://www.fenrirproject.org}
%\email{luker@fenrirproject.org}
%\telephone{+39 012 3456789}


\usepackage{tabularx}
\usepackage[utf8]{inputenc}
\usepackage{graphicx}
\usepackage{linkinclude}
\usepackage{hyperref}
\usepackage{listings}
\usepackage{soul}
\usepackage{caption}
\usepackage{mwe}
\usepackage{tikz}
\usetikzlibrary{arrows,shadows,automata,positioning}
\usepackage{amsmath}
\usepackage{framed}
\usepackage{wrapfig}


\usepackage{lettrine}


\makeindex

\begin{document}


\maketitle

%\begin{dedication}random randomness is random..\end{dedication}

\acknowledgements
\begin{figure}[h]
    \centering
    \includegraphics[width=0.6\textwidth]{xkcd/team_effort.png}
    \caption*{[xkcd.org] Given the role they play in every process in my body, really, they deserve this award more than me. Just gotta figure out how to give it to them. Maybe I can cut it into pieces to make it easier to swallow ...}
    \label{fig:So standard}
\end{figure}
%Sed vel lorem a arcu faucibus aliquet eu semper tortor. Aliquam dolor lacus, semper vitae ligula sed, blandit iaculis leo. Nam pharetra lobortis leo nec auctor. Pellentesque habitant morbi tristique senectus et netus et malesuada fames ac turpis egestas. Fusce ac risus pulvinar, congue eros non, interdum metus. Mauris tincidunt neque et aliquam imperdiet. Aenean ac tellus id nibh pellentesque pulvinar ut eu lacus. Proin tempor facilisis tortor, et hendrerit purus commodo laoreet. Quisque sed augue id ligula consectetur adipiscing. Vestibulum libero metus, lacinia ac vestibulum eu, varius non arcu. Nam et gravida velit.

\abstract
\begin{figure}[h]
    \centering
    \includegraphics[width=0.8\textwidth]{xkcd/authorization.png}
    \caption*{[xkcd.org] What we'll end up solving!}
    \label{fig:So standard}
\end{figure}

\lettrine{W}{hen} programs needs secure communications they authenticate, then use an encrypted stream on top of an unauthenticated connection.\\
Stacking up protocols can weaken the security properties of the connection, and limit the flexibility of both transmission and authentication.\\
New protocols like Google's QUIC have tried to solve parts of these limitations, but there still are no federated authentication schemes integrated in
any protocol, authorization is almost completely ignored. The result is that both the programmers and the end users have a very limited choice on both the
security and flexibility of the communication.

After analyzing current authentication and encryption solutions, we will construct a formally verified protocol which includes encryption, authentication, authorization
and is aimed at federated environments.

Thanks to handling authorization and authentication together, we will be able to give the user unprecedented control over its accounts and applications.
The federation will grant the user the ability to login everywhere without remembering hundreds of different usernames and passwords, remotely block
lost accounts or whole devices. The programmers will find multiple levels of multiplexing already in place, high flexibility in connection properties (reliability,
priorities, multihoming...). The federation will also split the authentication data, and thus the user database, from the main application, so that compromising the latter will not reveal user data.



\tableofcontents

%\listoftables

%\listoffigures

\mainmatter

\input{Analysis.tex}

\input{Project.tex}

\input{Formal_Verification.tex}

\input{Implementation.tex}

% C++ code, doesn't get validated.
%\input{Validation.tex}

\input{Conclusions.tex}

\appendix

\input{Appendix.tex}

%% bibliography, analytical index etc...
\backmatter

%\summary
%\begin{figure}[h]
%    \centering
%    \includegraphics[width=1\textwidth]{paper.png}
%    \caption{so... yeah... this paper is really about...uh...}
%    \label{fig:Hope it doesn't happen...}
%\end{figure}


\newpage
\bibliographystyle{plain_\languagename}
%% recommended

% xkcd as bibliography title
\renewcommand{\chapter}[2]{
\begin{figure}[h]
    \centering
    \includegraphics[width=0.5\textwidth]{xkcd/citogenesis.png}
    \caption*{[xkcd.org]}
    \label{fig:So standard}
\end{figure}}
\bibliography{thud}
%% use `thebibliography' environment for manual bibliography

\printindex

\end{document}
