%%% Preamble
\documentclass[11pt, a4paper]{article}

\usepackage[english]{babel} % English language/hyphenation
\usepackage{url}
\usepackage{tabularx}
\usepackage{pdfpages}
\usepackage{float}
\usepackage{amsmath, amssymb}
\usepackage{systeme}

\usepackage{graphicx}
\graphicspath{ {../images for report/} }
\usepackage[margin=2cm]{geometry}

\usepackage{hyperref}
\hypersetup{
    colorlinks,
    citecolor=black,
    filecolor=black,
    linkcolor=black,
    urlcolor=black
}

\usepackage{cleveref}

%%% Custom headers/footers (fancyhdr package)
\usepackage{fancyhdr}
\pagestyle{fancyplain}
\fancyhead{}							% No page header
\fancyfoot[L]{}							% Empty 
\fancyfoot[C]{\thepage}					% Pagenumbering		
\fancyfoot[R]{}						    % Empty
\renewcommand{\headrulewidth}{0pt}		% Remove header underlines
\renewcommand{\footrulewidth}{0pt}		% Remove footer underlines
\setlength{\headheight}{13.6pt}

% numeric
\usepackage[style=ieee,sorting=none,backend=biber]{biblatex}
\addbibresource{../main.bib}

% Write the approved title of your dissertation
\title{Automated image classification with expandable models}

% Write your full name, as in University records
\author{Andre Henriques, 6644818}

\date{}

%%% Begin document
\begin{document}
	\section*{1}
	\subsection*{1.1}
		The file ag01598\_6644818\_1\_1.spdl contains the base model of $\text{protocol}\Pi$.

		I choose the names of the roles based on their functions since it would make the file more readable so R is Phone, S is Application, N is Network.

		As the diagram shows the first message is sent from the phone do the network to request the generation of a new session key.

		The keys where modeled using a custom usertype called ``SessionKey'' and the time to live has modeled using a custom usertype called ``Timestamp''

		The Network then aswers to the Phone and the Application the keys and the time to live and the hashed value of that using a hash function named ``Mac''.

		The Phone and the Application verify the Mac and then the phone sends a nonce to the phone and the phone answers back with a new nonce and the original nonce.

		The Mac was modeled as a hashing function then encryption this was done this way because scyther does not have a way of creating a mac function with keys so the hashing is done first followed by the encrypted so that an attacker can not modify it.

	\subsection*{1.2}
		The file ag01598\_6644818\_1\_2.spdl contains the base model of $\text{protocol}\Pi$ and the claims.

		I added non-injective synchronization(nisynch) to the Phone and Network, at least, some roles communicated as described by the protocol.
		I added a secret claim to SesK (Session key) to all roles, as the session key should be private.
 		Furthermore, I added Commit and Running claims between some roles to check for agreement between some variables:
		\begin{itemize}
			\item{Agreement between Phone and Network over the time to live and the session key}
			\item{Agreement between Application and Network over the time to live and the session key}
			\item{Agreement between Application and Phone over the message and the message m}
		\end{itemize}

		There are 9 overall claims, where only three do not fail. The secrecy of SesK from the perspective of the Network. And agreement over the SesK and the time to live between the Phone and the Network, and the Application and the Network.

		The protocol as it stands does not guarantee secrecy and agreement.

\end{document}