Compare commits
16 Commits
first-cw-w
...
a2ca86c82e
| Author | SHA1 | Date | |
|---|---|---|---|
| a2ca86c82e | |||
| 5597311f67 | |||
| c3149da051 | |||
| 6911a16ab1 | |||
| c7f331cb56 | |||
| c8acc8a00d | |||
| 0afb4d093a | |||
| aac17e07fb | |||
| 506076f5a4 | |||
| 2374a814b5 | |||
| 64be075085 | |||
| ac6f905357 | |||
| 866b5dbbfa | |||
| 545b8c9957 | |||
| 39a6fbde61 | |||
| d21224ac4c |
123
.drone.yml
123
.drone.yml
@@ -4,69 +4,76 @@ type: exec
|
||||
name: Build and deploy
|
||||
|
||||
steps:
|
||||
- name: Linting
|
||||
commands:
|
||||
- bash linting.sh
|
||||
- name: Build Cw1
|
||||
commands:
|
||||
- cd firstcw/cw
|
||||
- pdflatex cw.tex
|
||||
# Prepare bib
|
||||
- /usr/bin/vendor_perl/biber cw
|
||||
# Compile twice for the table of contents and for bib text
|
||||
- pdflatex cw.tex
|
||||
- pdflatex cw.tex
|
||||
- cd -
|
||||
|
||||
- name: Build UPDS-1
|
||||
commands:
|
||||
- cd cw
|
||||
- pdflatex cw.tex
|
||||
# Prepare bib
|
||||
- /usr/bin/vendor_perl/biber cw
|
||||
# Compile twice for the table of contents and for bib text
|
||||
- pdflatex cw.tex
|
||||
- pdflatex cw.tex
|
||||
- cd -
|
||||
- name: Build Cw2
|
||||
commands:
|
||||
- cd secondcw/cw
|
||||
- pdflatex cw.tex
|
||||
# Prepare bib
|
||||
- /usr/bin/vendor_perl/biber cw
|
||||
# Compile twice for the table of contents and for bib text
|
||||
- pdflatex cw.tex
|
||||
- pdflatex cw.tex
|
||||
- mv cw.pdf cw2.pdf
|
||||
- cd -
|
||||
|
||||
# - name: Build Report
|
||||
# commands:
|
||||
# - cd report
|
||||
# - cp ../upds-1/UPDS-content.tex UPDS-1-content.tex
|
||||
# - cp ../upds-2/UPDS-content.tex UPDS-2-content.tex
|
||||
# - pdflatex report.tex
|
||||
# # Prepare bib
|
||||
# - /usr/bin/vendor_perl/biber report
|
||||
# # Compile twice for the table of contents and for bib text
|
||||
# - pdflatex report.tex
|
||||
# - cd -
|
||||
#
|
||||
# - name: Generate text
|
||||
# commands:
|
||||
# - pnpm i
|
||||
# - pnpm ts-node main.ts report/report.tex
|
||||
# - name: Build Report
|
||||
# commands:
|
||||
# - cd report
|
||||
# - cp ../upds-1/UPDS-content.tex UPDS-1-content.tex
|
||||
# - cp ../upds-2/UPDS-content.tex UPDS-2-content.tex
|
||||
# - pdflatex report.tex
|
||||
# # Prepare bib
|
||||
# - /usr/bin/vendor_perl/biber report
|
||||
# # Compile twice for the table of contents and for bib text
|
||||
# - pdflatex report.tex
|
||||
# - cd -
|
||||
#
|
||||
# - name: Generate text
|
||||
# commands:
|
||||
# - pnpm i
|
||||
# - pnpm ts-node main.ts report/report.tex
|
||||
|
||||
- name: gitea_release
|
||||
environment:
|
||||
TOKEN:
|
||||
from_secret: token
|
||||
commands:
|
||||
- tea login add --url https://git.andr3h3nriqu3s.com --token "$TOKEN"
|
||||
- tea r rm -y current || echo "Release not found"
|
||||
# - tea r c --title "Latest Report" --asset report/report.pdf --asset upds-1/UPDS12-1.pdf --asset upds-2/UPDS12-2.pdf --asset results.txt --asset poster/poster.pdf current
|
||||
- tea r c --title "1st cw work" --asset cw/cw.pdf first-cw-work
|
||||
- name: gitea_release
|
||||
environment:
|
||||
TOKEN:
|
||||
from_secret: token
|
||||
commands:
|
||||
- tea login add --url https://git.andr3h3nriqu3s.com --token "$TOKEN"
|
||||
- tea r rm -y latest || echo "Release not found"
|
||||
- tea r c --title "Latest" --asset firstcw/cw/cw.pdf --asset secondcw/cw/cw2.pdf latest
|
||||
|
||||
- name: Remove current on failure
|
||||
environment:
|
||||
TOKEN:
|
||||
from_secret: token
|
||||
commands:
|
||||
- tea login add --url https://git.andr3h3nriqu3s.com --token "$TOKEN"
|
||||
- tea r rm -y current || echo "Release not found"
|
||||
trigger:
|
||||
status:
|
||||
- failure
|
||||
when:
|
||||
status:
|
||||
- failure
|
||||
- name: Remove current on failure
|
||||
environment:
|
||||
TOKEN:
|
||||
from_secret: token
|
||||
commands:
|
||||
- tea login add --url https://git.andr3h3nriqu3s.com --token "$TOKEN"
|
||||
- tea r rm -y latest || echo "Release not found"
|
||||
trigger:
|
||||
status:
|
||||
- failure
|
||||
when:
|
||||
status:
|
||||
- failure
|
||||
|
||||
#- name: latest
|
||||
# environment:
|
||||
# TOKEN:
|
||||
# from_secret: token
|
||||
# commands:
|
||||
# - tea r rm -y "3rd-metting" || echo "Release not found"
|
||||
# - tea r c --title "Last Metting Report" --asset report/report.pdf --asset upds-1/UPDS12-1.pdf --asset upds-2/UPDS12-2.pdf "3rd-metting"
|
||||
# - name: latest
|
||||
# environment:
|
||||
# TOKEN:
|
||||
# from_secret: token
|
||||
# commands:
|
||||
# - tea r rm -y "3rd-metting" || echo "Release not found"
|
||||
# - tea r c --title "Last Metting Report" --asset report/report.pdf --asset upds-1/UPDS12-1.pdf --asset upds-2/UPDS12-2.pdf "3rd-metting"
|
||||
|
||||
trigger:
|
||||
branch:
|
||||
|
||||
0
pnpm-lock.yaml → firstcw/pnpm-lock.yaml
generated
0
pnpm-lock.yaml → firstcw/pnpm-lock.yaml
generated
74
secondcw/ag01598_6644818_1_1.spdl
Normal file
74
secondcw/ag01598_6644818_1_1.spdl
Normal file
@@ -0,0 +1,74 @@
|
||||
/*
|
||||
* Coursework 2 PI protocol
|
||||
*/
|
||||
usertype String;
|
||||
usertype Timestamp;
|
||||
usertype Sessionkey;
|
||||
|
||||
hashfunction Mac;
|
||||
|
||||
protocol protocolPI(Network, Application, Phone) {
|
||||
|
||||
/* Role R - Phone
|
||||
*
|
||||
* has keys k(N,R)
|
||||
*
|
||||
*/
|
||||
role Phone {
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
recv_keysPhone(Network, Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
|
||||
|
||||
var mApp: String;
|
||||
|
||||
recv_1(Application,Phone, {mApp}SesK);
|
||||
|
||||
fresh mPhone: String;
|
||||
|
||||
send_2(Phone,Application, {mApp, mPhone}SesK);
|
||||
}
|
||||
|
||||
/* Role S - Application
|
||||
*
|
||||
* has keys k(N,S)
|
||||
*
|
||||
*/
|
||||
role Application {
|
||||
|
||||
send_refreshKeys(Application,Network, Application, Phone);
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
recv_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
|
||||
|
||||
fresh mApp: String;
|
||||
var mPhone: String;
|
||||
|
||||
send_1(Application,Phone, {mApp}SesK);
|
||||
|
||||
recv_2(Phone,Application, {mApp, mPhone}SesK);
|
||||
}
|
||||
|
||||
/* Role N - Network
|
||||
*
|
||||
* has keys k(N,R) and k(N,S)
|
||||
*
|
||||
*/
|
||||
role Network {
|
||||
|
||||
recv_refreshKeys(Application,Network, Application, Phone);
|
||||
|
||||
fresh SesK: SessionKey;
|
||||
fresh tl: Timestamp;
|
||||
|
||||
send_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
|
||||
|
||||
send_keysPhone(Network,Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
93
secondcw/ag01598_6644818_1_2.spdl
Normal file
93
secondcw/ag01598_6644818_1_2.spdl
Normal file
@@ -0,0 +1,93 @@
|
||||
/*
|
||||
* Coursework 2 PI protocol
|
||||
*/
|
||||
usertype String;
|
||||
usertype Timestamp;
|
||||
usertype Sessionkey;
|
||||
|
||||
hashfunction Mac;
|
||||
|
||||
protocol protocolPI(Network, Application, Phone) {
|
||||
|
||||
/* Role R - Phone
|
||||
*
|
||||
* has keys k(N,R)
|
||||
*
|
||||
*/
|
||||
role Phone {
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
recv_keysPhone(Network, Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
|
||||
|
||||
var mApp: String;
|
||||
|
||||
recv_1(Application,Phone, {mApp}SesK);
|
||||
|
||||
fresh mPhone: String;
|
||||
|
||||
claim_phone1(Phone, Running, Application, mApp);
|
||||
|
||||
send_2(Phone,Application, {mApp, mPhone}SesK);
|
||||
|
||||
claim_phone2(Phone, Secret, SesK);
|
||||
claim_application1(Phone, Commit, Application, mApp);
|
||||
claim_network2(Phone, Commit, Network, SesK, tl);
|
||||
claim_phone3(Phone, Nisynch);
|
||||
}
|
||||
|
||||
/* Role S - Application
|
||||
*
|
||||
* has keys k(N,S)
|
||||
*
|
||||
*/
|
||||
role Application {
|
||||
|
||||
send_refreshKeys(Application,Network, Application, Phone);
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
recv_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
|
||||
|
||||
fresh mApp: String;
|
||||
var mPhone: String;
|
||||
|
||||
claim_application1(Application, Running, Phone, mApp);
|
||||
|
||||
send_1(Application,Phone, {mApp}SesK);
|
||||
|
||||
recv_2(Phone,Application, {mApp, mPhone}SesK);
|
||||
|
||||
claim_application2(Application, Secret, SesK);
|
||||
claim_phone1(Application, Commit, Phone, mApp);
|
||||
claim_network1(Application, Commit, Network, SesK, tl);
|
||||
|
||||
claim_application3(Application, Nisynch);
|
||||
}
|
||||
|
||||
/* Role N - Network
|
||||
*
|
||||
* has keys k(N,R) and k(N,S)
|
||||
*
|
||||
*/
|
||||
role Network {
|
||||
|
||||
recv_refreshKeys(Application,Network, Application, Phone);
|
||||
|
||||
fresh SesK: SessionKey;
|
||||
fresh tl: Timestamp;
|
||||
|
||||
claim_netwrok1(Network, Running, Application, SesK, tl);
|
||||
send_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
|
||||
|
||||
claim_network2(Network, Running, Phone, SesK, tl);
|
||||
send_keysPhone(Network,Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
|
||||
|
||||
claim_network3(Network, Secret, SesK);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
99
secondcw/ag01598_6644818_1_3.spdl
Normal file
99
secondcw/ag01598_6644818_1_3.spdl
Normal file
@@ -0,0 +1,99 @@
|
||||
/*
|
||||
* Coursework 2 PI protocol
|
||||
*/
|
||||
usertype String;
|
||||
usertype Timestamp;
|
||||
usertype Sessionkey;
|
||||
|
||||
hashfunction H1;
|
||||
|
||||
protocol protocolPI(Network, Application, Phone) {
|
||||
|
||||
/* Role R - Phone
|
||||
*
|
||||
* has keys k(N,R)
|
||||
*
|
||||
*/
|
||||
role Phone {
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
recv_keysPhone(Network,Phone, {H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone));
|
||||
|
||||
var mApp: String;
|
||||
|
||||
recv_1(Application,Phone, {mApp, Application, Phone }SesK);
|
||||
|
||||
fresh mPhone: String;
|
||||
|
||||
claim_phone1(Phone, Running, Application, mApp, SesK);
|
||||
|
||||
send_2(Phone,Application, {mApp, mPhone}SesK);
|
||||
|
||||
claim_phone2(Phone, Secret, SesK);
|
||||
claim_application1(Phone, Commit, Application, mApp, SesK);
|
||||
claim_network2(Phone, Commit, Network, SesK, tl);
|
||||
claim_phone3(Phone, Nisynch);
|
||||
|
||||
}
|
||||
|
||||
/* Role S - Application
|
||||
*
|
||||
* has keys k(N,S)
|
||||
*
|
||||
*/
|
||||
role Application {
|
||||
|
||||
fresh nApp: Nonce;
|
||||
|
||||
send_refreshKeys(Application,Network, Application, Phone, nApp);
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
recv_keysApp(Network,Application, {H1(SesK, tl, nApp, Phone)}k(Network, Application), {SesK, tl, nApp, Phone}k(Network, Application));
|
||||
|
||||
fresh mApp: String;
|
||||
var mPhone: String;
|
||||
|
||||
claim_application1(Application, Running, Phone, mApp, SesK);
|
||||
|
||||
send_1(Application,Phone, {mApp, Application, Phone}SesK);
|
||||
|
||||
recv_2(Phone,Application, {mApp, mPhone}SesK);
|
||||
|
||||
claim_application2(Application, Secret, SesK);
|
||||
claim_phone1(Application, Commit, Phone, mApp, SesK);
|
||||
claim_network1(Application, Commit, Network, SesK, tl);
|
||||
|
||||
claim_application3(Application, Nisynch);
|
||||
}
|
||||
|
||||
/* Role N - Network
|
||||
*
|
||||
* has keys k(N,R) and k(N,S)
|
||||
*
|
||||
*/
|
||||
role Network {
|
||||
|
||||
var nApp: Nonce;
|
||||
|
||||
recv_refreshKeys(Application,Network, Application, Phone, nApp);
|
||||
|
||||
fresh SesK: SessionKey;
|
||||
fresh tl: Timestamp;
|
||||
|
||||
claim_netwrok1(Network, Running, Application, SesK, tl);
|
||||
|
||||
send_keysApp(Network,Application, { H1(SesK, tl, nApp, Phone) }k(Network, Application) , {SesK, tl, nApp, Phone}k(Network, Application));
|
||||
|
||||
claim_network2(Network, Running, Phone, SesK, tl);
|
||||
send_keysPhone(Network,Phone, {H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone));
|
||||
|
||||
claim_network3(Network, Secret, SesK);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
113
secondcw/ag01598_6644818_1_3_complex_solution.spdl
Normal file
113
secondcw/ag01598_6644818_1_3_complex_solution.spdl
Normal file
@@ -0,0 +1,113 @@
|
||||
/*
|
||||
* Coursework 2 PI protocol
|
||||
*/
|
||||
usertype String;
|
||||
usertype Timestamp;
|
||||
usertype Sessionkey;
|
||||
|
||||
hashfunction H1;
|
||||
|
||||
protocol protocolPI(Network, Application, Phone) {
|
||||
|
||||
/* Role R - Phone
|
||||
*
|
||||
* has keys k(N,R)
|
||||
*
|
||||
*/
|
||||
role Phone {
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
var TApp: Ticket;
|
||||
|
||||
recv_keysPhone(Network,Phone, {H1(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone), TApp);
|
||||
|
||||
var mApp: String;
|
||||
|
||||
var temp: Ticket;
|
||||
|
||||
recv_1(Application,Phone, {mApp, {Network, Application, Phone, tl}k(Network, Phone), Application, Phone }SesK);
|
||||
|
||||
fresh mPhone: String;
|
||||
|
||||
claim_phone1(Phone, Running, Application, mApp);
|
||||
|
||||
fresh nApp3: Nonce;
|
||||
|
||||
send_2(Phone,Application, {mApp, mPhone, TApp, nApp3}SesK);
|
||||
|
||||
recv_3(Application,Phone, {nApp3}SesK);
|
||||
|
||||
claim_phone2(Phone, Secret, SesK);
|
||||
claim_application1(Phone, Commit, Application, mApp);
|
||||
claim_network2(Phone, Commit, Network, SesK, tl);
|
||||
claim_phone3(Phone, Nisynch);
|
||||
|
||||
}
|
||||
|
||||
/* Role S - Application
|
||||
*
|
||||
* has keys k(N,S)
|
||||
*
|
||||
*/
|
||||
role Application {
|
||||
|
||||
fresh nApp: Nonce;
|
||||
|
||||
send_refreshKeys(Application,Network, Application, Phone, nApp);
|
||||
|
||||
var SesK: SessionKey;
|
||||
var tl: Timestamp;
|
||||
|
||||
var TPhone: Ticket;
|
||||
|
||||
recv_keysApp(Network,Application, {H1(SesK, tl)}k(Network, Application), {SesK, tl, nApp}k(Network, Application), TPhone);
|
||||
|
||||
fresh mApp: String;
|
||||
var mPhone: String;
|
||||
|
||||
claim_application1(Application, Running, Phone, mApp);
|
||||
|
||||
send_1(Application,Phone, {mApp, TPhone, Application, Phone}SesK);
|
||||
|
||||
var nApp3: Nonce;
|
||||
|
||||
recv_2(Phone,Application, {mApp, mPhone, {Network, Application, Phone, tl}k(Network, Application), nApp3}SesK);
|
||||
|
||||
send_3(Application,Phone, {nApp3}SesK);
|
||||
|
||||
claim_application2(Application, Secret, SesK);
|
||||
claim_phone1(Application, Commit, Phone, mApp);
|
||||
claim_network1(Application, Commit, Network, SesK, tl);
|
||||
|
||||
claim_application3(Application, Nisynch);
|
||||
}
|
||||
|
||||
/* Role N - Network
|
||||
*
|
||||
* has keys k(N,R) and k(N,S)
|
||||
*
|
||||
*/
|
||||
role Network {
|
||||
|
||||
var nApp: Nonce;
|
||||
|
||||
recv_refreshKeys(Application,Network, Application, Phone, nApp);
|
||||
|
||||
fresh SesK: SessionKey;
|
||||
fresh tl: Timestamp;
|
||||
|
||||
claim_netwrok1(Network, Running, Application, SesK, tl);
|
||||
|
||||
send_keysApp(Network,Application, { H1(SesK, tl) }k(Network, Application) , {SesK, tl, nApp}k(Network, Application), {Network, Application, Phone, tl}k(Network, Phone));
|
||||
|
||||
claim_network2(Network, Running, Phone, SesK, tl);
|
||||
send_keysPhone(Network,Phone, {H1(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone), {Network, Application, Phone, tl}k(Network, Application));
|
||||
|
||||
claim_network3(Network, Secret, SesK);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
115
secondcw/cw/cw.tex
Normal file
115
secondcw/cw/cw.tex
Normal file
@@ -0,0 +1,115 @@
|
||||
%%% Preamble
|
||||
\documentclass[11pt, a4paper]{article}
|
||||
|
||||
\usepackage[english]{babel} % English language/hyphenation
|
||||
\usepackage{url}
|
||||
\usepackage{tabularx}
|
||||
\usepackage{pdfpages}
|
||||
\usepackage{float}
|
||||
\usepackage{amsmath, amssymb}
|
||||
\usepackage{systeme}
|
||||
|
||||
\usepackage{graphicx}
|
||||
\graphicspath{ {../images for report/} }
|
||||
\usepackage[margin=2cm]{geometry}
|
||||
|
||||
\usepackage{hyperref}
|
||||
\hypersetup{
|
||||
colorlinks,
|
||||
citecolor=black,
|
||||
filecolor=black,
|
||||
linkcolor=black,
|
||||
urlcolor=black
|
||||
}
|
||||
|
||||
\usepackage{cleveref}
|
||||
|
||||
%%% Custom headers/footers (fancyhdr package)
|
||||
\usepackage{fancyhdr}
|
||||
\pagestyle{fancyplain}
|
||||
\fancyhead{} % No page header
|
||||
\fancyfoot[L]{} % Empty
|
||||
\fancyfoot[C]{\thepage} % Pagenumbering
|
||||
\fancyfoot[R]{} % Empty
|
||||
\renewcommand{\headrulewidth}{0pt} % Remove header underlines
|
||||
\renewcommand{\footrulewidth}{0pt} % Remove footer underlines
|
||||
\setlength{\headheight}{13.6pt}
|
||||
|
||||
% numeric
|
||||
\usepackage[style=ieee,sorting=none,backend=biber]{biblatex}
|
||||
\addbibresource{../main.bib}
|
||||
|
||||
% Write the approved title of your dissertation
|
||||
\title{Automated image classification with expandable models}
|
||||
|
||||
% Write your full name, as in University records
|
||||
\author{Andre Henriques, 6644818}
|
||||
|
||||
\date{}
|
||||
|
||||
%%% Begin document
|
||||
\begin{document}
|
||||
\section*{1}
|
||||
\subsection*{1.1}
|
||||
The file ag01598\_6644818\_1\_1.spdl contains the base model of $\text{protocol}\Pi$.
|
||||
|
||||
I choose the names of the roles based on their functions since it would make the file more readable so R is Phone, S is Application, N is Network.
|
||||
|
||||
As the diagram shows the first message is sent from the phone do the network to request the generation of a new session key.
|
||||
|
||||
The keys where modeled using a custom usertype called ``SessionKey'' and the time to live has modeled using a custom usertype called ``Timestamp''
|
||||
|
||||
The Network then aswers to the Phone and the Application the keys and the time to live and the hashed value of that using a hash function named ``Mac''.
|
||||
|
||||
The Phone and the Application verify the Mac and then the phone sends a nonce to the phone and the phone answers back with a new nonce and the original nonce.
|
||||
|
||||
The Mac was modeled as a hashing function then encryption this was done this way because scyther does not have a way of creating a mac function with keys so the hashing is done first followed by the encrypted so that an attacker can not modify it.
|
||||
|
||||
\subsection*{1.2}
|
||||
The file ag01598\_6644818\_1\_2.spdl contains the base model of $\text{protocol}\Pi$ and the claims.
|
||||
|
||||
I added non-injective synchronization(nisynch) to the Phone and Network, at least, some roles communicated as described by the protocol.
|
||||
I added a secret claim to SesK (Session key) to all roles, as the session key should be private.
|
||||
Furthermore, I added Commit and Running claims between some roles to check for agreement between some variables:
|
||||
\begin{itemize}
|
||||
\item{Agreement between Phone and Network over the time to live and the session key}
|
||||
\item{Agreement between Application and Network over the time to live and the session key}
|
||||
\item{Agreement between Application and Phone over the message and the message m}
|
||||
\end{itemize}
|
||||
|
||||
There are 9 overall claims, where only three do not fail. The secrecy of SesK from the perspective of the Network. And agreement over the SesK and the time to live between the Phone and the Network, and the Application and the Network.
|
||||
|
||||
The protocol as it stands does not guarantee secrecy and agreement.
|
||||
|
||||
\subsection*{1.3}
|
||||
The file ag01598\_6644818\_1\_3.spdl contains the fixed version of $\text{protocol}\Pi$
|
||||
|
||||
The first change was to require the refresh keys request was to require the application to send a nounce, this nonce is then sent back to application to verify that the key was generated, was requested to the application and not by the attacker.
|
||||
|
||||
The second change was to make the network send the identity of the other party to party that is reciving the message. i.e. Sending the identity of the Phone to the Application encrypted with the key Network,Application. This is done to guarantee that the Party reciving the communication is using a key that was intended for this communication.
|
||||
|
||||
\subsection*{1.4}
|
||||
|
||||
The original $\text{protocol}\Pi$ is not an apropiate solution of the the third party problem as it can not guarantee the secresy of the session key, and since an attacker can obtain the session key, $\text{protocol}\Pi$ is not an appropiate solution to the present problem.As scyther showed the are attacks in the Dolev-Yao model. There are also some attacks in outside of Dolev-Yao model.
|
||||
|
||||
For example:
|
||||
|
||||
With the assumptions that:
|
||||
\begin{itemize}
|
||||
\item{Dolev-Yao attacker.}
|
||||
\item{Strong cryptographic primitives}
|
||||
\item{The time to live is implemented as a counter not an endate timetamp.}
|
||||
\item{One of the previous keys where the encrypted version of the key and timestamp were recorded and leaked.}
|
||||
\end{itemize}
|
||||
|
||||
In this senario an attacker can record the messages where the key and the time to live were encrypted. Then when the key gets leaked, the attacker can perform a replay attack.
|
||||
|
||||
The attacker resends the previously recorded keys to the application server and the phone, because the time to live is based on a counter and not on a timestamp the phone and the server accept the ``new'' key, and since the attacker already knows this key the protocol failed at guarantee, the secrecy of the session key.
|
||||
|
||||
% Other possible attacks are possible, for example a senario where the time to live is large, and the cryptographic primitives are weak for that time frame, i.e. RSA with 100 decimal digits and time to live of 2 days, an attacter with enought computer power would be abble to obtain the key
|
||||
|
||||
But it can be improved, as we saw in the answers for the question 1.3 by modifing the protocol slightly we can achive secrecy of the session key in the dolev-yao model. Although it does not resolve issues related with the time to live if the protocol was implemented with counters for time to live instead of timestamp.
|
||||
|
||||
\end{document}
|
||||
|
||||
|
||||
68
secondcw/lab9.spdl
Normal file
68
secondcw/lab9.spdl
Normal file
@@ -0,0 +1,68 @@
|
||||
/*usertype Timestamp;
|
||||
|
||||
protocol LaTe(C, S)
|
||||
{
|
||||
role C {
|
||||
fresh nc: Nonce;
|
||||
|
||||
var ts: Timestamp;
|
||||
|
||||
send_1(C,S, C, nc);
|
||||
|
||||
recv_2(S,C, nc, ts, {nc, ts}k(S, C));
|
||||
|
||||
claim_C1(C,Nisynch);
|
||||
claim_C2(C,Niagree);
|
||||
claim_C3(C,Alive);
|
||||
claim_C4(C,Weakagree);
|
||||
claim_C5(C, Commit, S, nc, ts);
|
||||
}
|
||||
|
||||
role S {
|
||||
var nc: Nonce;
|
||||
|
||||
fresh ts: Timestamp;
|
||||
|
||||
//send_!timestampSet(S,S, ts);
|
||||
|
||||
recv_1(C,S, C, nc);
|
||||
|
||||
claim_C5(S, Running, C, nc, ts);
|
||||
|
||||
send_2(S,C, nc, ts, {nc, ts}k(S, C));
|
||||
|
||||
claim_S1(S,Nisynch);
|
||||
claim_S2(S,Niagree);
|
||||
claim_S3(S,Alive);
|
||||
claim_S4(S,Weakagree);
|
||||
}
|
||||
}*/
|
||||
|
||||
usertype TimeStamp;
|
||||
hashfunction H1;
|
||||
|
||||
|
||||
protocol LATe(I,R)
|
||||
{
|
||||
role I # Time Client - Initiator
|
||||
{
|
||||
fresh Na : Nonce;
|
||||
var T : TimeStamp;
|
||||
send_1(I,R,I,Na);
|
||||
recv_2(R,I,Na,T,H1({Na,T}k(I,R)));#encrypt-then-hash
|
||||
claim_I1(I,Nisynch); #encrypt-then-hash
|
||||
claim_I2(I,Niagree);
|
||||
claim_I3(I,Alive);
|
||||
claim_I4(I,Weakagree);
|
||||
claim_I5(I, Commit, R, Na, T);
|
||||
}
|
||||
|
||||
role R # Time Server - Responder
|
||||
{
|
||||
var Na : Nonce;
|
||||
fresh T : TimeStamp;
|
||||
recv_1(I,R,I,Na);
|
||||
claim_C5(R, Running, I, Na, T);
|
||||
send_2(R,I,Na,T,H1({Na,T}k(I,R)));#encrypt-then-hash
|
||||
}
|
||||
}
|
||||
8
secondcw/main.bib
Normal file
8
secondcw/main.bib
Normal file
@@ -0,0 +1,8 @@
|
||||
@misc{cadonfs,
|
||||
author={The CADO-NFS Development Team},
|
||||
title={{CADO-NFS}, An Implementation of the Number Field Sieve
|
||||
Algorithm},
|
||||
note={Release 2.3.0},
|
||||
year={2017},
|
||||
url={http://cado-nfs.inria.fr/}
|
||||
}
|
||||
Reference in New Issue
Block a user