%
% 1. process this file with pdflatex
% 2. remind to process it twice otherwise cross-references will be wrong
%
\documentclass[a4paper,12pt]{article}
%
% This is to create hyperlinks for index, URLs and citations
% (now we can use the command \url{...} to create URL with hyperlink)
% 
\usepackage{color}
\usepackage[a4paper,colorlinks=true,urlcolor=blue,citecolor=blue,linkcolor=blue,bookmarks=false]{hyperref}
%
% This allows inclusion of pictures.
% Create figures with PowerPoint and then export them individually
% in PDF, PNG, JPEG, or GIF format (in order of preference)
%
\usepackage[pdftex]{graphicx}
\DeclareGraphicsExtensions{.pdf,.png,.jpg,.gif}
%
% phantom space (for abbreviations)
%
\usepackage{xspace}
%
% Definition of margins
%
\usepackage[top=2cm,bottom=2cm,left=2cm,right=2cm]{geometry}
%
% This is needed if you write the report in Italian
%
\usepackage[latin1]{inputenc}% IMPORTANTE! usare codifica ISO-8859-1 per le lettere accentate

\usepackage[british,UKenglish,USenglish,english,american]{babel}
\usepackage{listings}
%
% Paragraph skip and indent
%
\setlength\parskip{\medskipamount}
\setlength\parindent{0pt}
%
% Frequently used abbreviations.
% - example1: \ie this is an example
% - example2: the \ipsec protocol
%
\def\myfigure#1{Figure ~#1\xspace}
\def\myfig#1{Fig.~#1\xspace}
\def\mytab#1{Tab.~#1\xspace}
%
\begin{document}

\title{Implementation and verification of webinos authentication protocols
\\
{\normalsize Report for the Computer Security exam at the Politecnico di Torino}
}
\author{Teodoro Montanaro (188924)
\\
{\normalsize tutor: Andrea Atzeni}
}
\date{September 2013}
\maketitle

\vfill

\rule{\textwidth}{1pt}

\tableofcontents

\rule{\textwidth}{1pt}

\vfill

\newpage

\section{Introduction}

The aim of this work is to develop unambiguous methods to verify algorithmically that webinos authentication methods do not contain deadlocks or similar critical states that can cause system crashes.

One of the major problems encountered developing software, especially when the software is made up of a lot of components, is to verify that it does exactly what we expect from it.
For this reason, the best way to verify the correctness of each module that makes up the software is to check out each part as a stand-alone component, and it is exactly what we did for webinos.

Webinos is a project that wants to enable web applications and services to be used and shared consistently and securely over a broad spectrum of converged and connected devices, including mobile, PC, home media (TV) and in-car units.
\\It is made up of a lot of different modules and, more specifically, it plans to introduce some novel authentication methods, which should at the same time introduce user-friendly SSO (Single Sign-On) and preserve user privacy. 
So, this homework have the task to analyze algorithmically only the behaviour of the authentication modules and methods from a security point of view.

This purpose can be achieved using model checking, which is just a method created to let developers analyze algorithmically their own software.
The verification is achieved by the definition of precise mathematical languages representing the system, its states, its transitions and its properties that can be verified by the model checker: a software that is able to check whether the properties are satisfied in a logic point of view.

\section{Webinos}

\subsection{What is webinos}
Webinos is an EU-funded project and affiliate program that have the aim to define and develop an Open Source Platform for the Future Internet (in the form of web runtime extensions), to enable web applications and services to be used and shared consistently and securely over a broad spectrum of converged and connected devices, including mobile, PC, home media (TV) and in-car units. 

\subsection{Webinos purposes and applications}
The webinos project intends to provide a platform to allow developers to only have to create their own applications once, but to distribute them on every operating system and on every device.
Moreover, it intends to let devices find each other and discover and use the services each of them offer.

Using webinos will bring advantages both for users and developers:
the users will have the possibility to know exactly how their information will be treated and everyone will be able to test the accuracy, efficiency and efficacy of algorithms used, for example, for security. On the other hand, the developers will have the opportunity to focus their efforts only on the development of ideas and not on all the other aspects that have to be considered now (like security, connection to other devices, and so on ... ).


\subsection{General Architecture description}
The webinos architecture is centered around the concept of Personal Zone, which is a way to organise personal devices and services and that provides a basis for managing the user's devices, together with the services running on them.
The Personal zone supports:
\begin{itemize}
\item Single Sign-On: Through authentication on a device and/or on an application, the user will be authenticated on the Personal Zone too. This avoids the need for establishing direct peering relationships between each pair of devices and allows stronger authentication with the services the user uses. Obviously the architecture also allows situations in which the user is offline.
\item Shared model of the context, which enables applications to dynamically adapt to changes, and to increase usability exploiting the context.
\item Synchronisation across the devices in the zone: this includes support for distributed authentication, as well as personal preferences, and replication of service-specific data, e.g. social contacts, and appointments. Synchronisation is essential for supporting offline usage.
\item Discovery and access to services: The high level discovery API allows Web developers to search for all local services, or to filter by service type and context, or even to locate a named service instance. Remote discovery is based on existing user names and Email addresses, resolving to a URI for a Personal Zone.
\end{itemize}
\begin{figure}[htbp]
\centerline{\includegraphics[keepaspectratio]{immagini/architecture.png}}
\caption{Personal Zones - reprinted from \cite{Webinos_authentication}}
\label{fig:personal_zones}
\end{figure}

As shown in \myfig{\ref{fig:personal_zones}}, a Personal Zone is implemented on a distributed basis, consisting of a single Personal Zone Hub (PZH) and multiple Personal Zone Proxies (PZPs).


There is a Personal Zone Hub for each user, which is identified by a URL and is associated with a one-to-one correlation to a Personal Zone. It is a service accessible via the Internet that contains all the information and data associated to the user.


This service is always accessible and operative so the user can use it by any device.


Moreover, a policy associated to every information is essential: everyone can specify what the other users can see about him/her.


On the device we need a software that interacts with the PZH and it is the Personal Zone Proxy. 

There is a PZP on each device used by the user and it is able to work even if there is not an Internet connection.


For this reason, the PZP is responsible for the synchronization of all the data and information to let user use services even when the connection is not available.

All the services are accessible through a simple browser.

\subsection{Authentication in webinos}

\subsubsection{How does it work?}

There are three types of authentication available in webinos: device authentication, user authentication and authentication with third party services (for example Twitter).


\setcounter{secnumdepth}{5}
\paragraph{User authentication} % level 4 - equivalent to subsubsubsection

\label{para_user_auth}

Users are primarily authenticated through their OpenID credentials. This involves them connecting to their PZH web interface and logging in with their own account.

This first authentication is a pre-requisite for many sensitive operations, but is not sufficient for accessing webinos APIs or other device features. It only allows a user to connect through the PZH web interface. Applications do not have access to any enhanced privileges through this.

Alternatively, on some devices users may log into the PZH web interface using just client-side X509 certificates. This is possible only when that device has been configured within the personal zone (based on a configuration file at the personal zone hub) to support this.


\begin{figure}[htbp]
\centering
\includegraphics[width=0.8\paperwidth]{immagini/OpenID_Authentication.png}
\caption{Sequence diagram relative to OpenID Authentication - reprinted from \cite{Webinos_authentication}}
\label{fig:OpenID_Authentication}
\end{figure}

As we can see in \myfig{\ref{fig:OpenID_Authentication}} (showing the sequence diagram of the method described above) there are 3 main system components: one that contains the User Agent and the javascript library, one that contains the PZH server and the OpenID Module and another one that contains the Identity Provider.

Let us analyze the sequence diagram, looking for the point in which it is important to guarantee high level security.
The component containing the user agent is essentially a web browser in which the user opens the login page and presses the ``Login'' button.
As result of this action an HTML page is loaded with its linked scripts and one of them is the \emph{webinos javascript library}, which allows the web browser to load the authentication function contained in it. 
After that, this function sends a message to the \emph{PZH webserver} saying that there is a login request.
This is the first point in which we have to analyze if the security is at the right level: there is communication between 2 different components that could be located in different locations.

Due to what is reported in the documentation, in this method (\emph{User authentication}) security is guaranteed by an \emph{OpenID Provider Authentication Policy Extension over HTTPS}, which can provide:

\begin{itemize}

\item Authentication (simple / mutual): depending on the security methods available on the server and on the device, they can ask each other to demonstrate that they are exactly who they say they are.
\item Integrity: if someone intercepts their messages and modifies them, the use of keyed digest and message identifiers guarantees that the system can detect these modifications.
\item Confidentiality: The system cyphers all the data sent by each part of the communication.
\end{itemize}

For this reason the only feasible attack in the list considered (\ref{para_security_in_webinos}) is the DoS one (as shown in the results provided by the model checker \ref{results_analysis}).

Then, the \emph{PZH webserver}, talking to the \emph{OpenID module}, prepares the OpenID authentication parameters and URL and sends them to the \emph{javascript library}.
This is the second point in which we have to check for security.

After that the web browser contacts the \emph{identity provider} (and here it is again important to test the efficiency of the security: the considerations are the same as discussed for the last point) and after some interactions with the user, the system will authenticate him on the \emph{PZH server}.

As it is easy to understand looking at the above explanation of the diagram, security analysis is important in every case in which communication is established between 2 or more actors that are not in the same subsystem; the reason is that an intruder could modify or intercept any kind of message exchanged between them and could cause system crashes and/or program deadlocks.

\setcounter{secnumdepth}{5}
\paragraph{Device authentication} % level 4 - equivalent to subsubsubsection

\label{para_device_auth}
Devices are authenticated through the possession and use of an RSA private key. Having this key is a pre-requisite for a PZP connecting to a personal zone and sharing data with other devices, since it can be used to sign in and to prove device identity.

In \myfig{\ref{fig:held_private_key}} we can see the sequence diagram describing how a device can hold a private key.


\begin{figure}[htb]
\centerline{\includegraphics[width=\textwidth,keepaspectratio]{immagini/held_private_key.png}}
\caption{Sequence diagram relative to private key acquisition - reprinted from \cite{Webinos_authentication}}
\label{fig:held_private_key}
\end{figure}

As we can see, in this situation all the interactions and messages are exchanged within the same subsystem, so the only security problems could come from inside, but they are avoided by the use of the RSA private key (in addition to the use of HTTPS protocol, which is instead used to communicate with the PZH server at the end of the procedure) that lets the user cypher all the data.


Moreover, in order to make sure that a private key is used appropriately it must be integrated with the policy system and with the local device authentication. For instance, the private key will be held in a key storage, which requires the user to prove their presence unlocking it. Furthermore, it can interact with the authentication API, such that an application can work out whether the user is still present or not.




\setcounter{secnumdepth}{6}
\paragraph{Presence} 
There are different ways of interaction between devices and users: sometimes presence is assumed (smartphones) and sometimes it is not (shared TVs, home servers).
\begin{itemize}
\item Devices with assumed presence are defined as ``private'' devices. Their keys are marked as such. Use of these device keys implies that the user is present.
	\begin{itemize}
		\item If a policy refers to just the end user, and not a specific device, then these devices will automatically match this policy. E.g. ``Peter can access file X'' would allow Peter to access file X from his ``private'' device.
	\end{itemize}

\item Devices without assumed presence (and this is the default) are defined as ``shared'' devices. Use of a shared device does not imply that the user is necessarily present.

	\begin{itemize}
		\item If a policy refers to just the end user, and is about access to a local device API, then the user must re-authenticate using the Authentication API or OpenID.
		\item If a policy refers to just the end user, and is about access to a remote API, the user must re-authenticate using OpenID.
	\end{itemize}
\end{itemize}


For these reasons every time a user wants to access resources the system has to check the user's presence, and it works as illustrated in \myfig{\ref{fig:presence}}:
depending on the kind of assumed presence the system interacts with different entities that in any case ask the user to demonstrate that he is present (typing in his credentials).


\begin{figure}[htbp]
\centerline{\includegraphics[width=0.95\textwidth,keepaspectratio]{immagini/presence.png}}
\caption{Presence: authenticating to the local device - reprinted from \cite{Webinos_authentication}}
\label{fig:presence}
\end{figure}

In this situation security is managed using RSA private keys over HTTPS, so all the security properties shown at the previous point (Authentication, Integrity and Confidentiality) are sa- tisfied and in addition the non repudiation property is guaranteed, because using RSA private keys we can certificate who the owner of every message/data sent is.



\begin{figure}[htbp]
\centerline{\includegraphics[width=0.9\textwidth,keepaspectratio]{immagini/OpenID_authentication_from_PZP_part1.png}}
\caption{OpenID authentication from the PZP part n.1 - reprinted from \cite{Webinos_authentication}}
\label{fig:openid_sequence_diagram_1}
\end{figure}

\begin{figure}[htb]
\centerline{\includegraphics[width=0.9\textwidth,keepaspectratio]{immagini/OpenID_authentication_from_PZP_part2.png}}
\caption{OpenID authentication from the PZP part n.2 - reprinted from \cite{Webinos_authentication}}
\label{fig:openid_sequence_diagram_2}
\end{figure}

\myfigure{\ref{fig:openid_sequence_diagram_1}} and \myfigure{\ref{fig:openid_sequence_diagram_2}} show what the system does when a user attempts to perform a privileged action on the PZP:
After the request the \emph{PZP} forwards this request to the \emph{PZH}, which replies requiring authentication. The message contains the URL for this authentication.
Then, the \emph{PZP} opens a web browser and directs the user to the URL provided. He must log into this URL and then the page presents an authorisation prompt explaining the action requested and the impact of the action on the personal zone.
The user approves or rejects the prompt and the action is carried out or not, depending on the decision made.

In this situation the security properties (Authentication, Integrity, Confidentiality and non Repudiation) are guaranteed using RSA private key over HTTPS.


\setcounter{secnumdepth}{5}
\paragraph{Third party authentication} % level 4 - equivalent to subsubsubsection
\label{para_third_party}

Third party services should interact with webinos using OAuth 1.0. This method provides a process for end-users to authorize third-party access to their server resources without sharing their credentials, through user-agent redirections.

The solution described consists on the use of an additional developer-provided server (\emph{devServer}) which is trusted to hold on to developer OAuth credentials. This is accessed by the client-side JavaScript of a webinos application in order to sign OAuth requests and gain access to resources. Storing credentials on a server, misuse of these credentials can be prevented through rate-limiting or other mechanisms.

A practical implementation of this is described in \myfig{\ref{fig:twitter_sequence_diagram}}.
\\ The diagram shown is related to a webinos application (that is running within the widget runtime (WRT) or browser) attempting to connect to Twitter (or any similar OAuth 1.0 service).
The first section describes how the application requests that the \emph{devServer} authenticate to Twitter on the application behalf. Following this, an example of using the \emph{devServer} to make access requests (tweets, in this case) is shown.



\begin{figure}[htbp]
\centerline{\includegraphics[width=\textwidth,keepaspectratio]{immagini/twitter_authentication.png}}
\caption{Third party authentication - reprinted from \cite{Webinos_OAuth_service}}
\label{fig:twitter_sequence_diagram}
\end{figure}


\subsubsection{Security implementation in Authentication methods}
\label{para_security_in_webinos}
As discussed previously, in the webinos authentication method security is implemented in different ways depending on the authentication required.
\\In the \emph{\nameref{para_user_auth}} security is guaranteed using the OpenID Provider Authentication Policy Extension (OpenID PAPE) over HTTPS that provides a mechanism by which a Relying Party can request that particular authentication policies be applied by the OpenID Provider when authenticating an End User.

On the other hand, the security for \emph{\nameref{para_device_auth}} and \emph{\nameref{para_third_party}} is guaranteed using RSA private keys.
Through these methods we can guarantee the following security properties:
\begin{itemize}
\item Authentication (simple / mutual): depending on the security methods available on the server and on the device, and on the kind of certificates available, every part of the communication can ask each other to demonstrate that they are exactly who they say they are.

\item Integrity: if someone intercepts our messages and modifies them, the use of keyed digest and message identifiers (offered by HTTPS) guarantees that the system can detect these modifications.

\item Confidentiality: The system cyphers all the data sent by each part of the communication and so, even if someone intercepts them, they cannot understand the content. However this is not an absolute assumption: The use of RSA private key is not an absolute warranty, because the level of security offered by this method depends on the length of the key used to cypher data, on the exponent used for the 2 keys (if the exponent contains a little number of 1, it could be simple to decipher data for an hypothetical attacker) and on the use that the user makes of the private key (if, for example, the user stores the key in a place that is easy accessible for anyone, all efforts are pointless) .
\item Non repudiation: Using RSA private keys we can certificate who the owner of every message/data is. However, care must be taken even for this point: if the RSA keys are not generated carefully and the user does not store the private key in an appropriate place, the property becomes false.
\end{itemize}

Considering these properties we can avoid a lot of security attacks:
\begin{itemize}
\item Packet sniffing: Even if someone intercepts our communications, he/she cannot understand what we are saying because in both the situations (user authentication by PAPE methods or using RSA private key) the data are cyphered.
\item Data spoofing: Even if someone tries to modify the content of messages the system detects these modifications.
\item Replay attacks: Using HTTPS (SSL on HTTP) this attacks are avoided using a sequence number.
\item Shadow server: Using RSA private keys, a server authentication for all the communications is always required.
\item Man in the middle: Ensuring the properties of authentication, integrity, confidentiality and using sequence numbers this attack is avoided.
\end{itemize}

The only attack not avoided by the use of these methods is the DOS (Denial of Service) attack and we demonstrate that the system is actually exposed to this type of attacks \footnote{ This study is based only on the available webinos documentation (see \cite{Webinos_architecture} , \cite{Webinos_authentication} , \cite{Webinos_OAuth_service} for details), so it is possible that in the real implementation of webinos the developers adopt some other kind of solutions to solve this problem.}.

Specifically, considering all the methods just described and all the security controls made by webinos, this attack is applicable only in communications between 2 different entities.
If we look at the first sequence diagram (\myfig{\ref{fig:OpenID_Authentication}}) we can identify the situations in which a DoS attack is applicable in the following situations:
\begin{itemize}
\item When a message is sent from the \emph{webinos javascript libary} to the \emph{PZH webserver} or viceversa (messages n. 3, 6)
\item When a message is sent from the \emph{User agent} to the \emph{Identity provider} or viceversa (messages n. 8, 9, 12, 13, 16)
\item When a message is sent from the \emph{Identity provider} to the \emph{PZH webserver} or viceversa (messages n. 17)
\item When a message is sent from the \emph{PZH webserver} to the \emph{User agent} or viceversa (messages n. 19)
\end{itemize}

Then, in the diagram at \myfig{\ref{fig:held_private_key}} it is applicable only in the last message sent from the \emph{PZP Session Handler} to the \emph{PZH Provider}.

Moreover, in the diagram at \myfig{\ref{fig:presence}} it is applicable in the following situations:
\begin{itemize}
\item When a message is sent from \emph{PZP} to the \emph{OpenID Proxy} or viceversa (messages n. 6, 9, 10, 13)
\item When a message is sent from the \emph{User} to the \emph{OpenID Proxy} or viceversa (messages n. 7, 8, 11, 12)
\end{itemize}

And, at the end, in the diagrams related to the OpenID authentication from the PZP (\myfig{\ref{fig:openid_sequence_diagram_1}} and \myfig{\ref{fig:openid_sequence_diagram_2}}) and in the one related to the third party authentication (\myfig{\ref{fig:twitter_sequence_diagram}}) it is applicable in all the situations.

\section{Model checker}

\subsection{What is a model checker}

Software model checking is the algorithmic analysis of programs to prove properties of
their execution. 
Typically, when a software is made, programmers start from the specification and the definition of all the properties that the system should have for the specific task.
Before the real implementation of the code is essential to prove that the specifications wrote do not contain deadlocks, critical states, bugs and/or protocol weaknesses that can cause system crashes or some other kind of problem that could put user information at risk (we can think for example to privacy).

In order to solve such a problem algorithmically, both the model of the system and the specification are formulated in some precise mathematical language: To this purpose, it is formulated as a task in logic, namely to check whether a given structure satisfies a given logical formula.

\subsection{Model checkers analyzed }
There are a lot of software developed for model checking, and for this reason it was a little difficult to find the right for our purpose.
Considering the time available for this homework we considered the most diffused software:

\begin{itemize}
\item Casper \cite{casper_site}: it is a program that takes a description of a security protocol in a simple, abstract language, and produce a CSP description of the same protocol, suitable for checking using FDR2. It can be used either to find attacks upon protocols, or to show that no such attack exists. 

\item Promela - Spin \cite{spin_site}: Spin is a tool for analyzing the logical consistency of asynchronous systems, specifically distributed software and communication protocols. A verification model of the system is first specified in a guarded command language called Promela. This specification language allows for the modeling of dynamic creation of asynchronous processes, nondeterministic case selection, loops, gotos, local and global variables. It also allows for a concise specification of logical correctness requirements, including, but not restricted to requirements expressed in linear temporal logic. 
\item NuSMV \cite{NuSMV_tutorial}: it allows for the representation of synchronous and asynchronous finite state systems, and for the analysis of specifications expressed in Computation Tree Logic (CTL) and Linear Temporal Logic (LTL).
\end{itemize}


\subsection{Model checker chosen for our project}

Let us analyze with more details the positive and negative characteristics of every model checker analyzed.

\begin{itemize}
\item Casper:

Analyzing all the features (positive and negative) shown in the table \ref{tab:pro_cons_casper}, we can understand that Casper would be the perfect candidate for our purposes, but we had to consider that there were not a lot of examples and tutorials available for it, and moreover, that we had not enough information about the security relative to webinos to use in the definition of the regular grammar.
\begin{table}[htbp]
\begin{center}
\begin{tabular}{|p{8cm}|p{8cm}|} % twocentered columns (but you can also use 'r' for right or 'l' for left)
\hline


\multicolumn{2}{|c|}{} \tabularnewline
\multicolumn{2}{|c|}{\textbf{\Large Casper}}
 \tabularnewline

\multicolumn{2}{|c|}{} \tabularnewline
\hline
\rule[0cm]{0mm}{0,5cm}
\makebox[8,5cm][c]{\em PROS} & \makebox[8,5cm][c]{\em CONS}

\rule[0cm]{0mm}{0,5cm}
 \tabularnewline
\hline
\rule[0cm]{0mm}{1cm}
It is specifically created for security tests & We did not have the information about the keys used by the RSA algorithm\\

\rule[0cm]{0mm}{1cm}
It uses a simple abstract language & We did not have the information about the authentication methods available on each device (that should be negotiated in the OAuth procedure)\\

\rule[0cm]{0mm}{1cm}
  & There are not a lot of example projects explaining how to translate a sequence diagram to a formal language acceptable from Casper

 \tabularnewline
\hline
\end{tabular}
\end{center}
\caption{PROS and CONS of Casper model checker}
\label{tab:pro_cons_casper}
\end{table}

\item Promela - Spin:

As shown in the table \ref{tab:pro_cons_spin}, it is easy to see that the reason why we had not chosen this model checker is that there was not enough documentation about the behaviour of Spin, and, moreover, there were not enough projects from which we could take inspiration.
\begin{table}[htbp]
\begin{center}
\begin{tabular}{|p{8cm}|p{8cm}|} % twocentered columns (but you can also use 'r' for right or 'l' for left)
\hline

\multicolumn{2}{|c|}{} \tabularnewline
\multicolumn{2}{|c|}{\textbf{\Large Promela - Spin}}
 \tabularnewline

\multicolumn{2}{|c|}{} \tabularnewline
\hline
\rule[0cm]{0mm}{0,5cm}
\makebox[8,5cm][c]{\em PROS} & \makebox[8,5cm][c]{\em CONS}

\rule[0cm]{0mm}{0,5cm}
 \tabularnewline
\hline
\rule[0cm]{0mm}{1cm}
It is specifically created to test distributed software and communication protocols & There are not exhaustive free tutorials and/or manuals\\

\rule[0cm]{0mm}{1cm}
It allows to create dynamically asynchronous processes & There are not a lot of example projects explaining how to translate a sequence diagram to a formal language acceptable from Spin
 \tabularnewline
\hline
\end{tabular}
\end{center}
\caption{PROS and CONS of Spin model checker}
\label{tab:pro_cons_spin}
\end{table}

\item NuSMV:

It was the ideal candidate for our purposes because there were a lot of example project usable as references and a detailed documentation explaining exactly how it works.
We can see the properties analyzed for our choice in the table \ref{tab:pro_cons_nusmv}.
\begin{table}[htbp]
\begin{center}
\begin{tabular}{|p{8cm}|p{8cm}|} % twocentered columns (but you can also use 'r' for right or 'l' for left)
\hline

\multicolumn{2}{|c|}{} \tabularnewline
\multicolumn{2}{|c|}{\textbf{\Large NuSMV}}
 \tabularnewline

\multicolumn{2}{|c|}{} \tabularnewline
\hline
\rule[0cm]{0mm}{0,5cm}
\makebox[8,5cm][c]{\em PROS} & \makebox[8,5cm][c]{\em CONS}

\rule[0cm]{0mm}{0,5cm}
 \tabularnewline
\hline
\rule[0cm]{0mm}{1cm}
It allows for the representation of synchronous and asynchronous finite state systems & By the version 2.5.2 NuSMV processes are still supported, but deprecated (to see more details go to the link \cite{processes_motivation} )\\

\rule[0cm]{0mm}{1cm}
 It allows for the analysis of specifications expressed in Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) &  \\

\rule[0cm]{0mm}{1cm}
It is possible to use variables (like in a sequence diagram) by which control the execution of the state machine &  \\

\rule[0cm]{0mm}{1cm}
There are a lot of examples and projects using NuSMV &  \\

\rule[0cm]{0mm}{1cm}
There is an easy understandable manual \cite{NuSMV_manual} and an easy understandable tutorial \cite{NuSMV_tutorial} &  

 \tabularnewline
\rule[0cm]{0mm}{1cm}
&
 \tabularnewline
\hline
\end{tabular}
\end{center}
\caption{PROS and CONS of NuSMV model checker}
\label{tab:pro_cons_nusmv}
\end{table}

\end{itemize}

After an hard work of analysis of all the available materials found for each model checker and of what every model checker was able to do, considering the time available and the workload that we should respect for an homework like this, the availability of comprehensive documentation and examples has been a key decision criterion;
So we decided to choose the NuSMV model checker, which was the one for which there were a lot of documentation and old example projects to use as reference.

\section{Properties of the webinos authentication system}

We started from the analysis of what the model checker would have to be able to verify.
\\We had to verify that the authentication methods were not affected by errors and/or deadlocks. For this reasons we decided to concentrate our efforts on the test of the procedures illustrated in the sequence diagrams reported in the first section of this report ( \myfig{\ref{fig:OpenID_Authentication}} - \myfig{\ref{fig:held_private_key}} - \myfig{\ref{fig:presence}} - \myfig{\ref{fig:openid_sequence_diagram_1}} - \myfig{\ref{fig:openid_sequence_diagram_2}} - \myfig{\ref{fig:twitter_sequence_diagram}} ) and to test if, based on the specification, the system was exposed to the DoS attack.
\\
Therefore, the properties to be checked was that all the states of the sequence diagrams were reachable and that even if someone has tried to occupy the system by a DoS attack it does not crash.
 
\subsection{Specific model for the webinos authentication system}

\subsubsection{Hypothesis and assumption}

ANNOTATION 1: Even if webinos accepts simultaneous asynchronous connection, we decided to simulate only one process at a time. The reasons are two:
\begin{itemize}
\item From the version 2.5.2 NuSMV processes are still supported, but deprecated (you can see more details to the link \cite{processes_motivation} ).
\item We assume that webinos has composed by a queue that stores all the messages arriving from each actor and so every process can be treated as unique.
\end{itemize}
As a result of this assumption we can't analyze all the situations in which a Denial of Service is achieved overloading resources, but it is not a real problem for us because there are not enough information about the amount of concurrent connections supported by each entity and/or the amount of time available for an answer, in the documentation. So, even if we had the possibility to execute more processes simultaneously, we would not have the necessary information to do it.
\\Moreover, even if we can see more than one process in all the results, they corresponds to the different situations reachable from each state depending on the variable values.

In this first part we will describe how a language accepted by the NuSMV model checker is made \footnote{ For more details about the languages accepted by NuSMV let us see \cite{NuSMV_manual} and \cite{NuSMV_tutorial}}.

First of all we need to know that all the languages (stored in files with ``smv'' extension) accepted by the NuSMV model checker has to be composed by MODULEs.
The module that has to be present in every language is the ``main'' module (MODULE main).
From it, it is possible to call and ``execute'' other modules passing variable to them.
In each module there are 2 main sections:
\begin{itemize}
\item VAR: in which we define the states of the language
\item ASSIGN: in which we define the rules followed by the model checker to pass from a state to another and in which we define the properties that must be verified (specified by the word SPEC);
\end{itemize}

\subsubsection{How to convert a sequence diagram into a formal language}

Now that we know how a language is made up we can pass to see how to define all the parts.

As we have already said, the procedure shown here was repeated for all the 5 diagrams reported in the first section of this report ( \myfig{\ref{fig:OpenID_Authentication}} - \myfig{\ref{fig:held_private_key}} - \myfig{\ref{fig:presence}} - (\myfig{\ref{fig:openid_sequence_diagram_1}} and \myfig{\ref{fig:openid_sequence_diagram_2}} treated as one) - \myfig{\ref{fig:twitter_sequence_diagram}} ).

Let us start from the section VAR. Looking at the first diagram ( \myfig{\ref{fig:OpenID_Authentication}} ) we can imagine that all the actors of the diagram are states container and then, every arrow of the diagram (that represents a method invocation or a message sent to the other part) can represents a state assumed by the system.

To better understand what we are saying let us see the diagram of our interest.
As shown in the table \ref{tab:actors_var_diag1}, there are 6 actors and so we created 6 variables.

\begin{table}[htbp]
\begin{center}
\begin{tabular}{|p{8cm}|p{8cm}|} % twocentered columns
\hline

\rule[0cm]{0mm}{0,5cm}
\makebox[8cm][c]{\em \textbf{Actors}} & \makebox[8cm][c]{\em \textbf{Corresponding variable}}\\
\hline

\rule[0cm]{0mm}{0,5cm}
\makebox[8cm][c]{\emph{User}} & \makebox[8cm][c]{\emph{User\_status}}\\
\makebox[8cm][c]{\emph{User agent}} & \makebox[8cm][c]{\emph{Useragent\_status}}\\
\makebox[8cm][c]{\emph{Webinos javascript library}} & \makebox[8cm][c]{\emph{Webinos\_javascript\_library\_status}}\\
\makebox[8cm][c]{\emph{PZH webserver}} & \makebox[8cm][c]{\emph{PZH\_webserver\_\_status}}\\
\makebox[8cm][c]{\emph{OpenID Module}} & \makebox[8cm][c]{\emph{OpenID\_Module\_\_status}}\\
\makebox[8cm][c]{\emph{Identity provider}} & \makebox[8cm][c]{\emph{Identity\_provider\_status}}\\

\hline
\end{tabular}
\end{center}
\caption{Actors and variables corresponding to the first sequence diagram}
\label{tab:actors_var_diag1}
\end{table}

Then, we created another variable for the system (\emph{system\_status}) that can be considered as a general state indicating the point of the diagram in which the exchange of messages is in a particular moment.
After that we started to create a state for each arrow present in the diagram:

\begin{itemize}
\item \emph{login\_request}
\item \emph{auth\_agent\_req}
\item \emph{auth\_library\_req}
\item \emph{prepare\_openid\_auth}
\item \emph{openid\_url\_par\_from\_openid}
\item \emph{openid\_url\_par\_from\_pzh}
\item \emph{load\_auth\_url}
\item \emph{identity\_prov\_url}
\item \emph{identity\_prov\_webpage}
\item \emph{ask\_user\_pass}
\item \emph{insert\_pass}
\item \emph{auth2\_from\_agent}
\item \emph{auth\_req\_from\_identity\_prov}
\item \emph{auth\_req\_agent}
\item \emph{allow\_user}
\item \emph{allow\_agent}
\item \emph{pzh\_callback}
\item \emph{extract\_user\_attributes}
\item \emph{redirect\_pzh\_landing\_page}
\end{itemize}

These states are all the possible states that the system can assume.\\Depending on these states, all the other actors act in different ways and assume different values. Each value represents a particular message sent to other actors, and so we used the same name used in the system status to represent these states.
So, we distributed the states shown above to all the actors.
\\(
\\For esample, the user will assume the following states:

\begin{itemize}

\item \emph{send\_login\_request}
\item \emph{send\_right\_userpass}
\item \emph{send\_wrong\_userpass}
\item \emph{allow\_auth}
\item \emph{reject\_auth}
\item \emph{authenticated}
\end{itemize}
)

Moreover, we have inserted 2 more states with respect to those present in the ``system state'' variable because we would like to see what would happen when the user types a wrong password or rejects the authorization request.

Obviously we did the same thing for all the actors (so for all the variables) present in the system.

As we can easily understand, by the definition of the states described above it is not possible to simulate a DoS attack and, moreover, it is not possible to express an idle actor, so we added 2 more states to all the actors (even if, as described in \emph{\nameref{para_security_in_webinos}}, not all the interactions could be affected by a DoS attack, so it is important to take care in the next step of the language definition: \emph{\nameref{para_rules_def}}):

\begin{itemize}
\item \emph{idle}
\item \emph{busy}
\end{itemize}

The busy state is the key for the DoS attack: it simulates the situation in which some point of the system are engaged to answer to the attacker.

\subsubsection*{Definition of the rules (ASSIGN section)}
\label{para_rules_def}
After the definition of all the states of the system it is important to define the rules that let the system move between states.
Let us analyze one of the definition made for the grammar described above:

\lstset{breaklines=true,basicstyle=\footnotesize}
\begin{lstlisting}
	
	init(javascript_library_status):= idle;
	
next(javascript_library_status):= case
		system_status = auth_agent_req & (javascript_library_status
		   = idle | javascript_library_status = busy) :
		    send_auth_req;
		system_status = openid_url_par_from_pzh & (
		   javascript_library_status = idle | 
		   javascript_library_status = busy)
		   : {load_auth_url,busy};
		TRUE : idle;
	esac;
\end{lstlisting}

In this piece of code we say to model checker to initialize the variable \emph{javascript\_library\_status} to the value \emph{idle} and then we say how its value has to be updated:
\\ when the \emph{system\_status} is equal to \emph{auth\_agent\_req} AND the value of \emph{javascript\_library\_status} is \emph{idle} or \emph{busy}, the variable \emph{javascript\_library\_status} has to assume the value \emph{send\_auth\_req}.
\\ Then, when \emph{system\_status} is equal to \emph{openid\_url\_par\_from\_pzh} AND the value of \emph{javascript\_library \_status} is \emph{idle} or \emph{busy}, the variable \emph{javascript\_library\_status} has to assume the value \emph{load\_auth\_url} or the value \emph{busy}: as you can see in the diagram, the message \emph{openid\_url\_par\_from\_pzh} came from a component of the system that is out of the block that contains the \emph{javascript library}, so in this case there could be a DoS attack and for this reason we say to the model checker that in this situation the \emph{javascript library} can answer immediately (assuming the value \emph{load\_auth\_url}) or not (assuming the value \emph{busy}).
\\ Then, if neither the first and the second condition are satisfied the value of \emph{javascript\_library\_status} has to be \emph{idle}.

After that, we made this kind of definition for all the variables and then we had passed to the final part: the definition of the properties that have to be verified.


\subsubsection*{Properties to verify (ASSIGN section)}

To understand this part let us analyze one of the possible properties:

\lstset{breaklines=true,basicstyle=\footnotesize}
\begin{lstlisting}

SPEC AG (proc1.system_status = idle -> AF proc1.system_status = login_request)

\end{lstlisting}

The keyword \emph{SPEC} says that it is a property that has to be verified.
The keyword \emph{AG} says that the property has to be valid \emph{globally} and for \emph{all} the states of all the possible path.
After that we say that when the system status is \emph{idle} then the next state (\emph{AF} means \emph{All Future}) of \emph{system\_status} has to be \emph{login\_request}.

Let us see another property:

\lstset{breaklines=true,basicstyle=\footnotesize}
\begin{lstlisting}

SPEC AG (proc1.user_status = send_login_request -> EF proc1.useragent_status = send_auth_req)

\end{lstlisting}

It says that for \emph{all the states} of \emph{all the possible path} (AG) when the \emph{user\_status} is \emph{send\_login\_request} then one of the possible future state (\emph{EF} means that \emph{Exist} some \emph{Future} path) of \emph{useragent\_status} should be \emph{send\_auth\_req}.

For all the NuSMV code produced for this project let us see to the appendix section in which is described where you can find it.

\section{Results}
\subsection{Results from the Model checker}

The results produced by the model checker tells us if the properties defined are satisfied or not, and if they are not satisfied it shows a counter example that demonstrates it.
Let us see this 2 first parts of the results reported in Appendix B:


\definecolor{myyellow}{rgb}{1,1,0.7}

\lstset{breaklines=true,basicstyle=\footnotesize,backgroundcolor=\color{myyellow},moredelim=[is][\color{red}]{@@}{@@}}
\begin{lstlisting}

-- specification AG (proc1.system_status = idle -> AF proc1.system_status = login_request) is true
-- specification AG (proc1.system_status = login_request -> AF proc1.system_status = auth_agent_req) is true
-- specification AG (proc1.system_status = auth_agent_req -> AF proc1.system_status = auth_library_req) is true
@@-- specification AG (proc1.system_status = auth_library_req -> AF proc1.system_status = prepare_openid_auth) is false@@
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  proc1.system_status = idle
  proc1.user_status = send_login_request
  proc1.useragent_status = idle
  proc1.javascript_library_status = idle
  proc1.pzh_webserver_status = idle
  proc1.openid_module_status = idle
  proc1.identity_provider_status = idle
  proc2.system_status = idle
  proc2.user_status = send_login_request
  proc2.useragent_status = idle
  proc2.javascript_library_status = idle
  proc2.pzh_webserver_status = idle
  proc2.openid_module_status = idle
  proc2.identity_provider_status = idle
  proc3.system_status = idle
  proc3.user_status = send_login_request
  proc3.useragent_status = idle
  proc3.javascript_library_status = idle
  proc3.pzh_webserver_status = idle
  proc3.openid_module_status = idle
  proc3.identity_provider_status = idle
-> State: 1.2 <-
  proc1.system_status = login_request
  proc1.user_status = idle
  proc2.system_status = login_request
  proc2.user_status = idle
  proc3.system_status = login_request
  proc3.user_status = idle
-> State: 1.3 <-
  proc1.useragent_status = send_auth_req
  proc2.useragent_status = send_auth_req
  proc3.useragent_status = send_auth_req
-> State: 1.4 <-
  proc1.system_status = auth_agent_req
  proc1.useragent_status = idle
  proc2.system_status = auth_agent_req
  proc2.useragent_status = idle
  proc3.system_status = auth_agent_req
  proc3.useragent_status = idle
-> State: 1.5 <-
  proc1.javascript_library_status = send_auth_req
  proc2.javascript_library_status = send_auth_req
  proc3.javascript_library_status = send_auth_req
-> State: 1.6 <-
  proc1.system_status = auth_library_req
  proc1.javascript_library_status = idle
  proc2.system_status = auth_library_req
  proc2.javascript_library_status = idle
  proc3.system_status = auth_library_req
  proc3.javascript_library_status = idle
-- Loop starts here
@@-> State: 1.7 <-
  proc1.pzh_webserver_status = busy
  proc2.pzh_webserver_status = busy
  proc3.pzh_webserver_status = busy@@
-> State: 1.8 <-

\end{lstlisting}

As we can see, the first 3 properties are satisfied, instead the fourth is not.
\\To be precise, the counterexample says us that that if an intruder tries to occupy the \emph{pzh\_webserver} with a DoS attack, the system will crash.

Another interesting example is the following:

\lstset{breaklines=true,basicstyle=\footnotesize}
\begin{lstlisting}

@@-- specification AG (proc1.system_status = ask_user_pass -> AF proc1.system_status = insert_pass) is false@@
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 4.1 <-
  proc1.system_status = idle
  proc1.user_status = send_login_request
  proc1.useragent_status = idle
  proc1.javascript_library_status = idle
  proc1.pzh_webserver_status = idle
  proc1.openid_module_status = idle
  proc1.identity_provider_status = idle
  proc2.system_status = idle
  proc2.user_status = send_login_request
  proc2.useragent_status = idle
  proc2.javascript_library_status = idle
  proc2.pzh_webserver_status = idle
  proc2.openid_module_status = idle
  proc2.identity_provider_status = idle
  proc3.system_status = idle
  proc3.user_status = send_login_request
  proc3.useragent_status = idle
  proc3.javascript_library_status = idle
  proc3.pzh_webserver_status = idle
  proc3.openid_module_status = idle
  proc3.identity_provider_status = idle
-> State: 4.2 <-
  ...

  ...
-- Loop starts here
-> State: 4.23 <-
  proc1.user_status = send_wrong_userpass
  @@proc2.identity_provider_status = busy
  proc3.identity_provider_status = busy@@
-> State: 4.24 <-
  proc1.user_status = idle
@@-> State: 4.25 <-
  proc1.user_status = send_wrong_userpass@@
\end{lstlisting}

Analyzing the last line of the result shown, it is easy to understand that the system will crash if the user types a wrong password instead of a right one. Moreover, on the other hand, the error obtained in the previous example is already present, in fact just one step before the last passage, the \emph{proc2} and the \emph{proc3} crashes for a DoS attack.

For all the results obtained from the model checker let us see the Appendix B.

\subsection{Results analysis with suggestions for future development}
\label{results_analysis}

Analyzing the results obtained from all the formal languages made to represent all the possible transitions in the authentication process, we can see that the system has the following 2 main problems:

\begin{itemize}
\item It is exposed to DoS attacks
\item The system crashes when the user does something that is not expected and reported in the diagrams
\end{itemize}

Obviously these considerations are the results made implementing what is reported in the specification.
As we can see, there are not information about what happens when, for example, the user inserts a wrong password, or when he rejects an authentication request.
Furthermore, we do not know how many time is spent by every actors waiting an answer or a command from other actors, so, as we can see in all the results, assuming that the real system works exactly as described in the documentation, the system could be exposed to a DoS attack.

It is demonstrated in all the counter examples in which the system enter in a loop depending on the fact that from a busy state it could continue to remain in this situation for an infinite time.

Moreover, we can see that every time the user does something that is not expected, the system does not respect the normal sequence of action: it remains in the state caused by the action, so it crashes.

Even if the problems just illustrated are not so trivial, we can observe, on the other hand, that all the other properties are satisfied and so all the other activities are not affected by errors or deadlocks.

\section{Conclusions}


For future works we would like to suggest to the developers to write a more detailed documentation and then, if actually the system does not implement anything to solve the 2 problems exposed in the previous section we can suggest to implement some functions to solve it.


All the code developed for this project and the results obtained by the model checker are attached to this document and is organized as described below.
\\There is a folder for each diagram analyzed:

\begin{itemize}
\item webinos\_1\_OpenID\_Authentication -$>$ related to \myfig{\ref{fig:OpenID_Authentication}}
\item webinos\_2\_dev\_held\_priv\_key -$>$ related to \myfig{\ref{fig:held_private_key}}
\item webinos\_3\_local\_dev\_auth -$>$ related to \myfig{\ref{fig:presence}}
\item webinos\_4\_openid\_auth\_from\_pzp -$>$ related to \myfig{\ref{fig:openid_sequence_diagram_1}} and \myfig{\ref{fig:openid_sequence_diagram_2}}
\item webinos\_5\_oauth\_service\_twitter -$>$ related to \myfig{\ref{fig:twitter_sequence_diagram}}
\end{itemize}
In each folder we can find a file with ``smv'' extension, which contains the formal languages and the properties that have to be verified;
\\and a file with ``txt'' extension, which contains the results.

\appendix
\section{User manual}
\lstset{breaklines=true,basicstyle=\footnotesize,backgroundcolor=\color{white},}
In order to use the source code produced for this homework, we have to follow the steps listed below:
\begin{itemize}
\item Download NuSMV software from the official site (following this link: \cite{NuSMV_program})
\item Choose the right version (looking for the right operating system) and after the download, install it on the computer.
\\Let us assume that we are working under a linux distribution, so we can follow the ``NuSMV source'' link and after entering the required information we can download the ``tar.gz'' archive.
\item Uncompress the content of the archive in a directory of your choice (/temp for example)
\item Then, open the terminal window
\item Enter the directory in which you have extracted the files (/temp)
\item Enter the directory ``cudd-2.4.1.1''
	\begin{lstlisting}
	cd cudd-2.4.1.1
	\end{lstlisting}

\item Run ``\emph{make}''
\item Enter the directory ``../nusmv''
\item Run ``configure'':
	\begin{lstlisting}
	./configure
	\end{lstlisting}
\item Run ``\emph{make}''
		
\end{itemize}

Now, let us assume that the formal language defined is in the file ``example.smv'' and that we want to store the results in the file ``results.txt''.
To let the model checker do it we have to run the following command:
	\begin{lstlisting}
	NuSMV example.smv > results.txt
	\end{lstlisting}
	
After a few seconds we will have the results stored in the file ``results.txt''.

\section{NuSMV code implemented for the first sequence diagram (OpenID Authentication)}

\lstset{breaklines=true,basicstyle=\footnotesize,backgroundcolor=\color{myyellow}}
\lstinputlisting{webinos_model_checker/webinos_1_OpenID_Authentication/openid_auth_EF.smv}

\section{First part of Results obtained by the first model checker (OpenID Authentication)}

\lstset{breaklines=true,basicstyle=\footnotesize}
\lstinputlisting[firstline=1,lastline=300]{webinos_model_checker/webinos_1_OpenID_Authentication/result_openid_auth_EF.txt}

\begin{thebibliography}{99}
%
% Citations will be numbered according to the order
% in which they are listed in this section.
%

% citation of the site used for the introduction
\bibitem{introduction}
\url{https://developer.webinos.org/introduction},
``Introduction to webinos'', 

\bibitem{what is webinos and why do i want one}
\url{http://www.webinos.org/blog/2011/11/04/what-is-webinos-\%E2\%80\%93-and-why-do-i-want-one/} ,
``What is webinos - and why do I want one?'', 

\bibitem{Webinos_architecture}
\url{http://www.webinos.org/content/html/D033/Architecture\_Overview.htm} ,
``Webinos architecture'', 

\bibitem{Webinos_authentication}
\url{http://www.webinos.org/content/html/D033/Authentication.htm} ,
``Authentication in webinos'', 

\bibitem{Webinos_OAuth_service}
\url{http://www.webinos.org/content/html/D033/OAuth\_Service.htm} ,
``OAuth Service -$>$ Authentication by third party application'', 

\bibitem{OpenID Provider Authentication Policy Extension}
\url{http://openid.net/specs/openid-provider-authentication-policy-extension-1\_0.html} ,
``OpenID Provider Authentication Policy Extension'',

\bibitem{Model checking introduction}
\url{https://en.wikipedia.org/wiki/Model\_checking} ,
``An introduction to Model checking'',

\bibitem{mondo_digitale}
A.~Fantechi, S.~Gnesi,
``Model Checking: cos'e' e come si applica'',
Journal ``Mondo Digitale'',
No.~2-3,
June - September 2011,
pp.~29--39

\bibitem{a_servey_of_regular_model_checking}
P.A.~Abdulla, B.~Jonsson, M.~Nilsson,M.~Saksena,
``A Survey of Regular Model Checking'',
pp.~1--14



\bibitem{casper_site}
\url{http://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/index.html} ,
``Casper model checker'',

\bibitem{spin_site}
\url{http://spinroot.com/spin/Man/} ,
``Spin model checker'',


\bibitem{NuSMV_manual}
\url{http://nusmv.fbk.eu/NuSMV/userman/v25/nusmv.pdf} ,
``NuSMV manual'',

\bibitem{NuSMV_tutorial}
\url{http://nusmv.fbk.eu/NuSMV/tutorial/v25/tutorial.pdf} ,
``NuSMV tutorial'',

% sample citation from a journal/magazine
\bibitem{NuSMV_on_kerberos}
M.~Panti, L.~Spalazzi, S. Tacconi
``Document from which we learn to translate a sequence diagram to a formal language: Using the NuSMV Model Checker to verify the Kerberos Protocol'',
pp.~1--7

\bibitem{processes_motivation}
\url{http://nusmv.fbk.eu/faq.html\#012} ,
``Why processes are deprecated in NuSMV'',

\bibitem{NuSMV_program}
\url{http://nusmv.fbk.eu/NuSMV/download/getting-v2.html} ,
``NuSMV program'',


\end{thebibliography}

\end{document}
%
% Before delivering your report, don't forget to run a spell checker,
% such as aspell (with a UK-english dictionary)
%
