Started working on question 2
All checks were successful
continuous-integration/drone/push Build is passing

This commit is contained in:
Andre Henriques 2023-12-13 20:47:17 +00:00
parent a2ca86c82e
commit 37e7b11a7f
2 changed files with 159 additions and 0 deletions

View File

@ -0,0 +1,94 @@
/*
* 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 mApp: String;
recv_1(Application,Phone, ({H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, 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;
var T1: Ticket;
recv_keysApp(Network,Application, {H1(SesK, tl, nApp, Phone, T1)}k(Network, Application), {SesK, tl, nApp, Phone, T1}k(Network, Application));
fresh mApp: String;
var mPhone: String;
claim_application1(Application, Running, Phone, mApp, SesK);
send_1(Application,Phone, T1, {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, ({H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone))) }k(Network, Application) , {SesK, tl, nApp, Phone, ({H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone))}k(Network, Application));
claim_network3(Network, Secret, SesK);
}
}

View File

@ -110,6 +110,71 @@
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. 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.
\subsection*{1.5}
The file ag01598\_6644818\_1\_5.spdl contains the a more comunication efficient version of the $\text{protocol}\Pi$
This version trades off computational power for communication efficiency. This version creates bigger encrypted messages and as trade off reduces the number of messages that are sent.
The message that is removed is the message where the network sends the key to the phone. This data in this message is still send but it's send when the application sends the m message.
And the data is sent to the Application inside the encrypted packed that is already sent to the Application when the phone recives the keys from the network.
It sends the session key that was send by the network, to the phone, with the message m.
\section*{2}
\subsection*{2.1}
Using a system like gpg you can generate keys by running the command \begin{verbatim}gpg --gen-key\end{verbatim}.
The public key are then traded.
\subsection*{2.2}
There are multiple ways of securily exaging the keys.
For example if meeting up in person was a possiblity the keys cloud be put onto usb drives and the drives exchanged in person. And this would guarantee 100\% authentication, but meeting in person could not be feasable.
If meeting in person is not feasable an altertive method would be sending the public key via email, and then calling the collegue on the phone. Both parties would then hash key using for example \begin{verbatim}sha512sum key\end{verbatim} and both parties would readout their public keys hash to each other. Since the parties know eachother, and would recoginze the voice this would be a feazable way to exchange the public keys. With this they could verify that the password came from the correct person.
\subsection*{2.3}
Assuming that the peers were able to exchange public keys.
One of the Peer A would generate a random 256 bit key.
Peer A would then encrypt the key using Peer B's public key, and sign it using it's own private key.
Peer A would then send the signed and encrypted semetric key to Peer B in an insecure channel.
Peer B upon reciving the encrypted and signed semetric key, would verify the signature, and decrypt the message and obtain the key.
After this both A and B can comunicate using the semetric key.
Example:
Peer A:
\begin{verbatim}
head -c32 /dev/random > aes256key
gpg --output key.gpg --encrypt --recipient b@example.com aes256key
gpg --output key.gpg.sig --sign key.gpg
\end{verbatim}
send key.gpg.sig to peer b
Peer B:
\begin{verbatim}
gpg --output key.gpg.sig --decrypt key.gpg
gpg --output key.gpg --decrypt key
\end{verbatim}
Now both Peer A and Peer B have the same key and can start communicating between each other.
\end{document} \end{document}