ComputerSecurity/secondcw/cw/cw.tex

%%% 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.

	\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 all the roles to guarantee that  all the roles, 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 10 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}