diff --git a/Final_Report__7_.pdf b/Final Report.pdf
similarity index 92%
rename from Final_Report__7_.pdf
rename to Final Report.pdf
index 451eb56db501aceac132cf8e2a6d4b49f3a24bd5..74f954af56299b5951bdbf117b62cf3c4ef0de3a 100644
Binary files a/Final_Report__7_.pdf and b/Final Report.pdf differ
diff --git a/Latex Files/Final_Report__5_.pdf b/Latex Files/Final Report.pdf
similarity index 69%
rename from Latex Files/Final_Report__5_.pdf
rename to Latex Files/Final Report.pdf
index 3b41c24cf16612c41a278b1249be35a28813d8fa..74f954af56299b5951bdbf117b62cf3c4ef0de3a 100644
Binary files a/Latex Files/Final_Report__5_.pdf and b/Latex Files/Final Report.pdf differ
diff --git a/Latex Files/Final_Report__3_.pdf b/Latex Files/Final_Report__3_.pdf
deleted file mode 100644
index 9af9554a972a3544029ce4b23029eb35d93414cb..0000000000000000000000000000000000000000
Binary files a/Latex Files/Final_Report__3_.pdf and /dev/null differ
diff --git a/Latex Files/latex.txt b/Latex Files/latex.txt
new file mode 100644
index 0000000000000000000000000000000000000000..02560a08c11178790ccea3de968b296633d686a2
--- /dev/null
+++ b/Latex Files/latex.txt
@@ -0,0 +1,731 @@
+\documentclass[twoside]{article}
+\usepackage[utf8]{inputenc}
+\usepackage{cite}
+\usepackage{graphicx}
+\usepackage[inner=24mm,outer=24mm,bottom=24mm,top=24mm]{geometry}
+\usepackage[parfill]{parskip}
+\usepackage[labelfont=bf]{caption}
+\usepackage[super]{nth}
+\usepackage{multirow}
+\usepackage{array}
+\usepackage{listings}
+\usepackage{color}
+\usepackage[acronym]{glossaries}
+\usepackage{enumitem}
+
+\definecolor{dkgreen}{rgb}{0,0.6,0}
+\definecolor{gray}{rgb}{0.5,0.5,0.5}
+\definecolor{mauve}{rgb}{0.58,0,0.82}
+
+\lstset{frame=tb,
+ language=Java,
+ aboveskip=3mm,
+ belowskip=3mm,
+ showstringspaces=false,
+ columns=flexible,
+ basicstyle={\small\ttfamily},
+ numbers=none,
+ numberstyle=\tiny\color{gray},
+ keywordstyle=\color{blue},
+ commentstyle=\color{dkgreen},
+ stringstyle=\color{mauve},
+ breaklines=true,
+ breakatwhitespace=true,
+ tabsize=3
+}
+\renewcommand{\arraystretch}{1.65}
+
+
+\author{Matthew Hutchings}
+\date{October 2019}
+\title{Recommending and modelling optimal security practices for smart grid connected IoT devices}
+
+\makeglossaries
+
+\newglossaryentry{Nonce}
+{
+ name=Nonce,
+ description={Mathematics is what mathematicians do}
+}
+
+\begin{document}
+
+\begin{centering}
+\large {
+
+ Electronics and Computer Science \\
+ Faculty of Physical Sciences and Engineering \\
+ University of Southampton \\
+ \vspace{1cm}
+ \textbf{Matthew Hutchings} \\
+ \nth{12} of May 2020 \\
+ \vspace{2cm}
+ }
+
+\noindent\rule{13cm}{0.4pt}
+
+\vspace{0.4cm}
+
+\LARGE{ \textbf{Recommending and modelling optimal security practices for smart grid connected IoT devices}}
+
+\noindent\rule{13cm}{0.4pt}
+
+\vspace{0.4cm}
+
+\large{
+\textbf{Project Supervisor:} Dr Nawfal Fadhel \\
+\textbf{\nth{2} Examiner:} Dr Xu Fang
+ \vspace{1.5cm}
+
+A report submitted for the award of \\
+MCOMP Information Technology in Organisations
+
+ }
+\end{centering}
+
+\newpage
+
+\newgeometry{inner=35mm,outer=24mm,bottom=24mm,top=24mm}
+
+\tableofcontents
+
+
+\newpage
+
+\textbf{Statement of Originality}
+\begin{itemize}
+ \item I have read and understood the ECS Academic Integrity information and the University’s \\Academic Integrity Guidance for Students.
+ \item I am aware that failure to act in accordance with the Regulations Governing Academic Integrity may lead to the imposition of penalties which, for the most serious cases, may include termination of programme.
+ \item I consent to the University copying and distributing any or all of my work in any form and using third parties (who may be based outside the EU/EEA) to verify whether my work contains plagiarised material, and for quality assurance purposes.
+\end{itemize}
+
+\textbf{I have acknowledged all sources, and identified any content taken from elsewhere.}
+
+\textbf{I have not used any resources produced by anyone else.}
+
+\textbf{I did all the work myself, or with my allocated group, and have not helped anyone else.}
+
+\textbf{The material in the report is genuine, and I have included all my data/code/designs. }
+
+\textbf{I have not submitted any part of this work for another assessment.}
+
+\textbf{My work did not involve human participants, their cells or data, or animals.}
+
+
+\newpage
+
+
+\section{Project Description}
+
+
+IoT devices present many exciting applications for both industrial and consumer use. However, increased dependence on these devices opens up new consequences and attack vectors that an adversary can use to attack a target. This is of particular importance in the case of IoT devices connected to smart grid infrastructure as cyberattacks could be used to disrupt critical national infrastructure. \\
+
+The scenario for my project is a IoT based smart grid with a focus on the IoT devices in the system and their interactions with the cloud layer.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.82]{ReferenceDiagram.PNG}
+ \caption{Reference diagram of my smart grid scenario}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+\newpage
+
+\subsection{Project Aims and Objectives}
+
+This project aims to produce, model and verify a collection of policies and protocols that are suitable for mitigating the threats that a IoT enabled smart grid may face. I wish to focus on the following goals within this project:
+
+\begin{itemize}
+
+\item Investigate and conduct a risk assessment on the main vulnerabilities and threats faced by IoT devices within smart grid environment.
+
+\item Recommend security policies that can mitigate these threats, justifying these policies by taking into account secondary factors including the cost to implement and any loss to productivity these policies might incur.
+
+\item Implement and verify that these communication protocols mitigate the identified vulnerabilities using Scyther, a formal method based protocol verification tool.
+
+\item Clearly explain the impact of each of my policies by comparing the possible attack vectors with and without each policy using Scyther.
+
+\item Create a purpose built, portable Scyther virtual machine environment allowing myself and others to quickly set up and start using Scyther on a new device.
+
+
+\end{itemize}
+
+
+
+\subsection{Project Scope}
+
+The scope of this project will be investigating, modelling and verifying the best policies and practices for IoT devices and their communications in my smart grid scenario. The project will focus mainly on IoT communication protocols and their configuration rather examine flaws in the hardware or firmware ran by these devices.
+
+\section{Glossary of terms}
+
+\begin{itemize}[label={}]
+ \item \textbf{Nonce} A randomly generated value that is used only a single time in a cryptographic protocol. Often used as a timestamp to prevent the reuse of old message credentials.
+ \item \textbf{Adversary} A term used to describe a party attempting to disrupt the security of a system.
+\end{itemize}
+
+\newpage
+
+\section{Literature Review}
+
+My literature review explores the IoT and smart grid landscape before looking into the cybersecurity issues that a smart grid implementation may face. Finally, the review discuss the verification of cryptographic protocols in the context of my scenario
+
+\subsection{Internet of Things (IoT) Devices}
+
+IoT as a general concept can be described as physical objects also being network identifiable devices that are able to communicate without the need for human interaction\cite{patel2016internet}. These devices can be used in a home or industrial context to automate processes or afford additional functionality. IoT devices can do this as they are able to leverage information by collecting/receiving it across a network. As an example of an IoT implementation in a chemical production plant, IoT monitoring devices could be used to monitor the temperature of a reaction. If the temperature fell outside of the requirement, the device could communicate with another IoT device that controls the coolant flow through the reaction and correct it without the need for any human interaction. \\
+
+These IoT networks can offer benefits for existing processes such as improved efficiency, fewer employees required to manage it and data which can be used to improve the process. However, it is important to consider from a cybersecurity perspective that the introduction of networked devices to a process opens it up to the possibility of cyberattacks.
+
+\subsection{Smart Grids}
+
+The term smart grid refers to the integration of technology into electrical grid systems allowing them to dynamically change to meet the current needs of consumers \cite{yu2011new}. Whilst the implementation of smart grids can vary significantly, several elements generally remain constant:
+
+\begin{itemize}
+ \item \textbf{Smart Meters and Monitors -} These IoT devices are used to measure and analyse the energy usage within a single home. Typically smart meters simply collect energy readings from a room and send this information to the smart monitor. This monitor relays energy information to a collection server and receives information on current energy prices. \cite{kuslitskiy_2019}
+
+ \item \textbf{Smart Hub -} This device allows the homeowner to track their electricity usage as well as view the current electricity price to help time their electricity usage to get the best price resulting in a better distribution of power demand across the power grid.
+
+ \item \textbf{Cloud Layer -} This layer communicates with the Smart Meter to receive electricity usage information and send electricity pricing information. This information can then be used by the rest of the smart grid system to adjust the routing and production of electricity based on current demand.
+
+\end{itemize}
+
+
+
+\subsection{IoT Smart Grid, the Threats, Attitudes and Best Practices}
+
+A key finding from my research, summarised by Robles \cite{robles2009assessment} is that one of the key differences between securing a traditional system compared with a national infrastructure system, such as smart grid, is the reduction in the effectiveness of standard security measures such as patches, password management and access control. Stating that this is due to the size and diverse combination of hardware and software that comprises this class of system. Whilst traditional controls do have their place in smart grid security Sajid \cite{7445139} identifies the need for specific security measures that directly mitigate the threats smart grids face. This point is further explored by Bere \cite{bere2015initial} which states that large industrial control systems are often the target of state-funded Advanced Persistent Threat(APT) groups whose capabilities and resources far outmatch the typical threat actors a system faces. \cite{bere2015initial} Bere goes onto recommend that the security protocols and controls implemented should be layered, providing a 'defence in depth' security approach which Virvilis \cite{Virvilis2013TrustedCV} states as a key countermeasure against APT groups as these groups have the ability to execute zero-day exploits. Zero-day exploits offer very little chance of mitigating an attack against part of a system as the vulnerability is only known to the adversary at the time of execution \cite{Bilge:2012:BWK:2382196.2382284}. However, a layered system means that in the event of such an attack, the entire system will not be compromised due to the presence of other security measures and protocols.
+\\
+
+Another area of difficulty when it comes to securing these systems is the perspective and attitudes of governments and other organisations when it comes to securing these systems. Wang \cite{wang2012sscada} states that many organisations do not see investing in the protection of these systems as economically viable. Virvilis \cite{Virvilis2013TrustedCV} adds that disruption to productivity and user experience due to the increase in latency or removal of features that hardened security protocols may necessitate is another factor in the lack of implemented protocols on these systems. Mcqueen \cite{mcqueen2006quantitative} suggests that it is difficult to quantify cyber risk using traditional risk assessment methods. This may further contribute to the reluctant attitude towards cybersecurity investment as it is difficult to quantify the reduction in risk to management.\\
+
+\subsection{Verification of Security Policies and Protocols}
+
+Creamers \cite{cremers2008scyther} states that it is very difficult for humans to analyse and find flaws in cryptographic protocols, as evidenced by the number of protocols that are found to have security flaws after their release. An example of this is the Needham-Schroeder key distribution protocol which even after extensive analysis and verification by hand was found to have a security flaw which allowed an adversary to pass off an old session key as a new and valid one \cite{meadows1994formal}. Meadows \cite{meadows1994formal} goes on to suggest that formal methods are a good choice for analysing these cryptographic protocols as they are enclosed enough to make modelling and verification feasible whilst also having the potential for subtle and counter-intuitive flaws that an informal analysis may miss. \\
+
+In order to verify a protocol using automated formal methods, it must first be modelled so that it can be interpreted by a protocol verification tool. In my research, I have found two tools that are the most suitable for this purpose; Pro-Verif and Scyther. In their comparative analysis of these two tools Dalal et al. \cite{dalal2010comparative} identifies that whilst the two tools share several similarities, there are several differences that make Scyther more suitable than Pro-Verif for my scenario and skillset.
+
+\begin{itemize}
+ \item \textbf{Modelling Language -} Scyther uses 'security protocol description language' (SPDL) described as "a mix between java and C" by creator Cas Creamers \cite{cremers2008scyther} to model protocols. Whereas Pro-Verif protocols are represented using horn clauses or pi calculus \cite{dalal2010comparative}. The SPDL used by Scyther is closer to pseudo-code than Pro-Verif making it more suitable for illustrating the implementation of protocols as well as being more fitting to my skillset.
+
+ \item \textbf{Attack Graphs -} Scyther automatically generates attack graphs when a flaw is found in verification, generating a visual flow diagram of the attack. Pro-Verif does not support this feature.
+
+\end{itemize}
+
+Based on these factors, the project will use Scyther for the modelling and verification of protocols.
+
+
+
+\newpage
+
+\section{Research and Design}
+
+When it comes to implementing a best practice cybersecurity strategy, NIST \cite{arnold2010nist} recommends a five step process for analysing and securing smart grid systems:
+
+\begin{itemize}
+ \item \textbf{1. Defining use cases -} The use cases of the system should be defined. This project defines use cases through the reference diagram.
+
+ \item \textbf{2. Risk Assessment -} The vulnerabilities, threats and the impact these threats can cause should be evaluated for the system. This project performs a risk assessment through the threat model and threat descriptions.
+
+ \item \textbf{3. Specification of Security Requirements -} The security requirements for the system should be stated and specified. This project specifies requirements through the list of policies that should be implemented for this scenario.
+
+ \item \textbf{4. Design and Development of a Security Architecture -} A security architecture to protect the smart grid system should be designed and implemented. Taking into account the use cases and security requirements outlined in the previous steps. This project aims to design and show implementations of policies and protocols in Scyther which meet the outlined security requirements.
+
+ \item \textbf{5. Assessment of implementation -} The architecture should be assessed against the defined security requirements to test if it is fit for purpose. This project will use Scyther's protocol verification tools to test the protocols against the requirements defined \cite{arnold2010nist}.
+
+\end{itemize}
+
+\newpage
+
+\subsection{Threat Model}
+
+The threat model below shows some of the attack vectors and vulnerabilities an adversary could exploit within my scenario:
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.85]{ThreatModel.PNG}
+ \caption{Threat Model of my smart grid scenario}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+A detailed breakdown of each threat and how they can be mitigated through the application of security protocols can be found in the preceding sections.
+
+\newpage
+
+\subsubsection{Weak/Default Password Fuzzing Attack}
+
+OWASP \cite{owasp} states than the most common vulnerability exploited in IoT devices is the use of weak or default passwords. These attacks are usually performed by automated scripts commonly referred to as bots that scan the internet for connected devices and run a list of common passwords. As an example of this, the Mirai botnet was able to infect and recruit over 500,000 IoT devices using a list of just 60 common passwords.
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.9]{PasswordManagement.PNG}
+ \caption{Adversary using a common password to compromise the network}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+In this scenario an adversary could exploit an internet connected smart hub with a weak or guessable password to recruit the device into a botnet or potentially use the compromised device as an attack vector to mount further attacks on the rest of the network.
+
+\subsubsection{Man In The Middle (MITM) Attack}
+
+Man in the middle attacks occur when an adversary is able to act as an intermediary or proxy between communication parties without their knowledge. This allows the adversary to view the contents of the messages sent between parties as well as silently modify the contents of messages.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.63]{MITM.PNG}
+ \caption{Adversary relaying and modifying smart monitor data}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+An Adversary could perform a MITM attack by secretly relaying and modifying the electricity usage information sent to the data model. A large scale attack of this kind effecting many monitor to model connections could cause false data injection attack on the smart grid system where false data could cause the system to make an incorrect decision when routing power.
+
+\newpage
+
+\subsubsection{Passive Eavesdropping}
+
+Low power IoT devices commonly use weak or no cryptography in their communications protocols, this means an adversary could use devices such as a wireless packet sniffer to intercept traffic sent between devices and read the contents of the communications sent. OWASP\cite{owasp} lists these insecure protocols as the \nth{2} most common IoT vulnerability.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.55]{Eavesdropping.PNG}
+ \caption{Adversary reading an insecure communication}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+This attack could occur anywhere in the scenario where devices communicate with each other without the use of an encrypted communication protocol. For example, the adversary could sniff packets between the smart meter and monitor to know if a home is occupied based on their current electricity usage or to gather information on the network for further attacks.
+
+\subsubsection{Replay Attack}
+
+Replay attacks occur when an adversary is able to identify and collect authentication credentials from a legitimate communication and use those credentials in a later communication to bypass authentication. This commonly occurs when communication partners do not make use of a unique identifier for each communication such as a session key.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.65]{Replay.PNG}
+ \caption{Adversary sniffing and reusing hashed authentication credentials}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+The adversary could sniff an encrypted communication between router and server used for the transmission of energy usage data. With this they could use the hashed authenticator code to send messages to the server posing as that home network without needing to know the actual authenticator code.
+
+
+\newpage
+
+\subsubsection{Impersonation Attack}
+
+An Impersonation attack occurs when an Adversary is able to pose as the identify of a legitimate party in a communication protocol allowing them to bypass authorisation or act on the legitimate user's behalf \cite{Adams2005}. Protocols that do not use unique tokens for each communication are particularly susceptible to this form of attack.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.65]{Impersonation.PNG}
+ \caption{Adversary posing as a legitimate smart meter}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+An adversary could use this attack to pose as a monitor communicating data model and may use this to report false energy readings reducing trust in the system or use this access to perform further attacks against the infrastructure.
+
+\subsubsection{Open Port Scanning}
+
+An open port refers to a device accepting packets from a certain port number. If ports are not configured correctly, adversaries can use a insecure port that has not been blocked as an attack vector. Botnet recruitment malwares such as Mirai scan these ports to identify IoT devices that can be compromised. \cite{yang2017survey}
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.65]{Openport.PNG}
+ \caption{Adversary using an open port to attack a device}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+This attack can occur in the scenario where any devices are configured to allow network traffic in from unnecessary communication protocols such as telnet (port 23) and SSH (port 22).
+\newpage
+
+\subsection{Recommendation of policies and practices}
+
+
+
+\subsubsection{Policy List}
+
+Based on the threat analysis of my scenario and my research I am recommending the following initial policies. These policies will be modelled in Scyther and the protocols that I create will be evaluated against them.
+\begin{centering}
+\begin{table}[h]
+\begin{tabular}{|c|m{3cm}|m{5cm}|m{5cm}|}
+
+\hline
+\textbf{Number} & \textbf{Policy} & \multicolumn{1}{c|}{\textbf{Description}} & \multicolumn{1}{c|}{\textbf{Reason for Inclusion}} \\ \hline
+1 & Suitable Password Management & 1. Default passwords must be changed
+
+2. Passwords should be a minimum of 8 characters and not feature common phrases & Will Mitigate the threat of default/weak password fuzzing attacks \\ \hline
+2 & Network Segregation & Smart Grid IoT devices should be segregated from the consumers home Wi-Fi network & Isolates system from the consumers potentially insecure home network \\ \hline
+3 & Patch Management & Security patches for devices and software in the system should be applied and tested in a timely fashion & Reduces exposure to known and patched vulnerabilities \\ \hline
+4 & Minimum design & The hardware design should include the minimum features required for operation of the hardware. Unnecessary ports should be closed & Unnecessary features and ports being enabled create additional attack vectors for adversaries \\ \hline
+5 & \multicolumn{3}{c|}{Communication between parties should be secure under the following sub standards} \\ \hline
+5.1 & Mutual Authentication & Mutual Authentication should be achieved by both communication parties & Increases the difficulty of an adversary posing as a communication party \\ \hline
+5.2 & Message Encryption & Information contained in communications should be encrypted & Encryption prevents an adversary sniffing information over an insecure network \\ \hline
+5.3 & Implicit key authentication & No entity other than the one specifically identified can gain access to the cryptographic key & Necessary for encryption to be robust \\ \hline
+5.4 & Unique Session Keys & Communication Parties should establish a unique session key valid for a single communication & Unique session keys prevent the re-use of authentication credentials \\ \hline
+\end{tabular}
+\caption{The initial policies recommended for the project.}
+\label{tbl:Policies}
+\end{table}
+\end{centering}
+
+\newpage
+
+\newpage
+
+\section{Design and implementation of a Scyther development environment}
+
+
+\section{Implementation and specification of non-communication IoT policies}
+
+\subsection{Smart Hub password management}
+
+In a study examining user behaviour toward password policies, Inglesant\cite{10.1145/1753326.1753384} found that excessively restrictive password policies with too much of a focus on password complexity caused users to adopt insecure workarounds such has writing down passwords or using the same password across multiple accounts. Therefore, a good password management policy should aim to balance the need for users to choose a password that is unique and complex enough to not fall victim to common password list and brute force attacks whilst also not being too restrictive or complicated that the user has to resort to insecure methods of remembering it.
+
+Based on this, the following key points are recommended for the implementation of an effective IoT password management policy:
+
+\begin{itemize}
+ \item Passwords must be at least 8 characters long
+ \item Before hashing, passwords should be checked against OWASP's top 10,000 password list\cite{TopPasswords}
+ \item Created passwords must only be used for the Smart Hub
+\end{itemize}
+
+\newpage
+
+\section{Implementation and modelling of communication protocol policies }
+
+
+\subsection{Message Encryption}
+
+The first policy to be implemented is message encryption. As this policy is designed to mitigate the threat of passive eavesdropping, I am defining the implementation successful if an adversary is unable to decrypt and read either the key or freshly generated message using a passive Eavesdropping attack.
+
+\subsubsection{Design}
+
+The design is a symmetric encryption/decryption protocol. The symmetric key design was chosen as it requires less computational power than asymmetric options and potential issues with key distribution are mitigated as communication parties remain constant therefore keys only have to be distributed once which can be in a controlled environment.
+
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.88]{01Graph.PNG}
+ \caption{Message encryption protocol design }
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+\newpage
+
+\subsubsection{Implementation}
+
+The implementation of the design in Scyther is a two-way communication where the Meter sends information to the Monitor and the Monitor sends back a confirmation of having received the message.
+
+\begin{figure}[h]
+\begin{lstlisting}[numbers=left,firstnumber=0,stepnumber=1]
+protocol smartExchange(Meter,Monitor)
+
+ {
+
+ role Meter {
+
+ fresh Message: Nonce;
+ var Confirm;
+
+ send_1(Meter,Monitor,{Message}k(k));
+ recv_2(Monitor,Meter,{Confirm}k(k));
+
+ claim_Meter1(Meter, Secret, (k));
+ claim_Meter2(Meter, Secret, Message);
+
+ }
+
+ role Monitor {
+
+ var Message;
+ fresh Confirm: Nonce;
+
+ recv_1(Meter,Monitor,{Message}k(k));
+ send_2(Monitor,Meter,{Confirm}k(k));
+
+ claim_Monitor1(Monitor, Secret, (k));
+ claim_Monitor2(Monitor, Secret, Message);
+
+ }
+
+}
+
+\end{lstlisting}
+\caption{Message encryption protocol design}
+\label{fig:my_label}
+\end{figure}
+
+
+
+\newpage
+
+\subsubsection{Review}
+
+To model the requirements of both the freshly generated value and the key not being disclosed, Scyther's Secret claim was made on the message which models an adversary attempting to eavesdrop on the message during communication.
+
+Without the implementation of the symmetric key encryption, running the secret claim generates a successful eavesdropping attack.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.6]{01Comparison.PNG}
+ \caption{Message encryption protocol test results }
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+The figure above shows by eavesdropping the message, demonstrated in this case by DataIntruder1 the adversary can read the contents of the message therefore disproving the secret claim.
+
+The first iteration of the protocol passed these tests successfully with Scyther showing that no attacks of this type are possible within the bounds of the protocol. Results using a wider range of claims however show that threats such as man-in-the-middle attacks can easily break this protocol demonstrating the need to iterate upon it and implement the remaining policies
+
+
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.9]{01Test.PNG}
+ \caption{Message encryption protocol test results }
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+\newpage
+
+\subsection{Implicit key authentication}
+
+Later policies will require the use of secret keys to create asymmetric encryption protocols, implicit key authentication must be enforced when these keys are distributed to prevent an adversary posing as a legitimate communication party using an intercepted secret key. To implement this policy a secure key distribution protocol is required.
+
+\subsubsection{Design}
+
+When looking to design this protocol, a decision had to be made on which style of key distribution was most suitable. These two styles being considered are best represented by the two popular key distribution protocols signed Diffie-Hellman and Needham-Schroeder.
+
+Needham-Schroeder makes use of a trusted 3rd party to securely establish authentication which can be used to exchange symmetric secret keys over an insecure network as shown in the figure below.
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.9]{Needham.PNG}
+ \caption{Illustration of the Needham Schroeder authentication process \cite{10.1007/3-540-61770-1_46}}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+In comparison, Diffie-Hellman does not require the use of a third party and instead relies on the concept of never actually sending a shared key over an insecure network but instead exchanging information that along with secret information both parties possess, allows the parties to generate the same key which becomes the shared secret key to be used in future communications.
+
+For the given IoT scenario a Diffie-Hellman style solution is the most appropriate based mainly on the fact that it does not require an additional third party. This makes the protocol less computational complex for the IoT devices as they only need to communicate with each other as well as negating the need infrastructure in the form of a server.
+
+
+\newpage
+
+\subsection{Unique Session Keys}
+
+Implementing session keys is one of the policies aimed at mitigating the threat of authentication based attacks such as impersonation and man in the middle attacks.
+
+
+\subsubsection{Design}
+
+
+
+
+
+
+\subsubsection{Implementation}
+
+The Scyther implementation uses the SessionKey usertype to model the session keys. Once both parties have sent each other an encrypted communication containing their session keys, the Meter sends the Monitor the message.
+
+
+\begin{lstlisting}[numbers=left,firstnumber=0,stepnumber=1]
+
+usertype SessionKey;
+usertype Message;
+
+protocol EncrpytedExchange(Meter,Monitor)
+
+ {
+
+ role Meter {
+
+ fresh M: Message;
+ fresh TokenA: SessionKey;
+ var TokenB;
+
+ send_1(Meter,Monitor,{TokenA}k(k));
+ recv_2(Monitor,Meter,{TokenB}k(k));
+ claim(Meter,Running,Monitor,M);
+ send_3(Meter,Monitor,{M}k(k));
+
+ claim_Meter1(Meter, Secret, (k));
+ claim_Meter2(Meter, Secret, M);
+ claim_Meter3(Meter,Niagree);
+ claim_Meter4(Meter,Nisynch);
+
+ }
+
+ role Monitor {
+
+ var M;
+ var TokenA;
+ fresh TokenB: SessionKey;
+
+ recv_1(Meter,Monitor,{TokenA}k(k));
+ send_2(Monitor,Meter,{TokenB}k(k));
+ recv_3(Meter,Monitor,{M}k(k));
+
+ claim_Monitor1(Monitor, Secret, (k));
+ claim_Monitor2(Monitor, Secret, M);
+ claim_Meter3(Monitor,Niagree);
+ claim_Meter4(Monitor,Nisynch);
+
+ }
+}
+
+\end{lstlisting}
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.8]{02Code.PNG}
+ \caption{Session Keys protocol in Scyther }
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+
+\newpage
+
+\subsubsection{Review}
+
+By using the Niagree and Nisynch claims, Scyther can verify if the roles within a protocol are able to authenticate the identity of a message sender. The Ni prefix denotes that the attack scope is limited to non-injective attacks, these are attacks that do not assume the adversary has knowledge from a previous run of the protocol.\cite{cas}
+
+As shown in the figure below, without the implementation of session keys it is trivial for an adversary to a pose as a meter which would allow them to send false readings in a message or potentially use the message as an attack vector for malware.
+
+
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.7]{02ComparisionBefore.PNG}
+ \caption{Niagree verification results before session key implementation}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+
+\newpage
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.6]{02ComparisonAfter.PNG}
+ \caption{Niagree verification results after session key implementation}
+ \label{fig:my_label}
+ \end{figure}
+\end{centering}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+\subsection{Mutual Authentication}
+
+
+
+
+
+
+
+
+\section{Plan for remaining work}
+
+When referring back to NIST's \cite{arnold2010nist} guidelines for the analysis and security implementation of a smart grid system, the first 3 phases defining use cases, risk assessment and specification of security requirements are reviewed in this report. Whilst the specification of security requirements will be further developed, the main focus of my remaining work is on the design and development of a security architecture and the assessment of the implementation of this architecture. This is reflected in my Gantt chart (fig:\ref{fig:Gantt}) which shows how I plan to break down this work into tasks and my expected timings for each of these tasks.
+
+
+\subsection{Risk Analysis}
+
+
+I have identified 5 risks as key risks which could impact on my delivery of the rest of the work. The grid below shows my plan to mitigate these risks and my assessment of any residual impact that may linger.
+
+
+
+\begin{table}[h]
+\begin{tabular}{|m{4cm}|c|m{6cm}|c|}
+
+\hline
+
+\multicolumn{1}{|c|}{\textbf{Risk}} & \textbf{Baseline} & \multicolumn{1}{c|}{\textbf{Mitigation}} & \textbf{Residual} \\
+
+\hline
+
+Scyther stops being supported on modern operating systems and I lose my access to the software & \begin{tabular}[c]{@{}c@{}}Impact: 5\\ Likelihood: 2\\ Score: 10\end{tabular} & I am using vagrant to set-up a box with Scyther and all the software required to run it installed so I always have it available, the vagrant box has a cloud backup & \begin{tabular}[c]{@{}c@{}}Impact: 5\\ Likelihood: 0\\ Score: 0\end{tabular} \\ \hline
+I fail to manage time correctly on the project and do not finish parts & \begin{tabular}[c]{@{}c@{}}Impact: 4\\ Likelihood: 3\\ Score: 10\end{tabular} & My Gantt chart will help when identifying if I am falling behind schedule on certain parts. Meeting weekly with my supervisor where I share my progress will also help me hold myself accountable for work. & \begin{tabular}[c]{@{}c@{}}Impact: 4\\ Likelihood: 1\\ Score: 4\end{tabular} \\ \hline
+My laptop is lost, stolen, or damaged causing me to lose all the content on the hard drive & \begin{tabular}[c]{@{}c@{}}Impact: 4\\ Likelihood: 2\\ Score: 8\end{tabular} & My project files are uploaded to Git and frequently pushed to the remote branch when I make changes. I can continue to work on my desktop and the university computers. & \begin{tabular}[c]{@{}c@{}}Impact: 3\\ Likelihood: 1\\ Score: 3\end{tabular} \\ \hline
+My remaining work is larger or more difficult than I anticipated meaning I fail to complete parts of it & \begin{tabular}[c]{@{}c@{}}Impact: 4\\ Likelihood: 3\\ Score: 12\end{tabular} & My background research and experience of learning Scyther in the last month has helped me estimate the difficulty of each task. & \begin{tabular}[c]{@{}c@{}}Impact: 3\\ Likelihood: 2\\ Score: 6\end{tabular} \\ \hline
+Personal/family issue & \begin{tabular}[c]{@{}c@{}}Impact: 3\\ Likelihood: 3\\ Score: 9\end{tabular} & Use the university support service when needed. Keep my supervisor informed & \begin{tabular}[c]{@{}c@{}}Impact: 2\\ Likelihood: 3\\ Score: 6\end{tabular} \\ \hline
+
+\end{tabular}
+
+\caption{Qualitative risk analysis and mitigation plan for the key risks}
+\label{tbl:Risk}
+
+\end{table}
+
+\newpage
+\subsection{Gantt Chart}
+
+My Gantt chart details my time management plan for the progress report and future plan for the rest of the project. \\
+
+\begin{centering}
+ \begin{figure}[h]
+ \centering
+ \includegraphics[scale = 0.49, angle=270]{Gantt.PNG}
+ \caption{Gantt chart for the project}
+ \label{fig:Gantt}
+ \end{figure}
+\end{centering}
+
+
+
+\newpage
+
+
+
+
+\newpage
+
+\bibliographystyle{unsrt}
+\bibliography{references.bib}
+
+
+\newpage
+
+
+
+
+
+
+
+\end{document}