This repository has been archived on 2024-01-04. You can view files and clone it, but cannot push or open issues or pull requests.
ComputerSecurity/secondcw/ag01598_6644818_1_5.spdl
Andre Henriques 37e7b11a7f
All checks were successful
continuous-integration/drone/push Build is passing
Started working on question 2
2023-12-13 20:47:17 +00:00

95 lines
2.2 KiB
Plaintext

/*
* 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);
}
}