diff --git a/secondcw/ag01598_6644818_1_3.spdl b/secondcw/ag01598_6644818_1_3.spdl index f77802c..8d4b4c9 100644 --- a/secondcw/ag01598_6644818_1_3.spdl +++ b/secondcw/ag01598_6644818_1_3.spdl @@ -9,7 +9,7 @@ hashfunction H1; protocol protocolPI(Network, Application, Phone) { - /* Role R - Phone + /* Role R - Phone * * has keys k(N,R) * @@ -19,25 +19,19 @@ protocol protocolPI(Network, Application, 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); + recv_keysPhone(Network,Phone, {H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone)); var mApp: String; var temp: Ticket; - recv_1(Application,Phone, {mApp, {Network, Application, Phone, tl}k(Network, Phone), Application, Phone }SesK); + recv_1(Application,Phone, {mApp, 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); + send_2(Phone,Application, {mApp, mPhone}SesK); claim_phone2(Phone, Secret, SesK); claim_application1(Phone, Commit, Application, mApp); @@ -60,22 +54,16 @@ protocol protocolPI(Network, Application, Phone) { 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); + 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); - send_1(Application,Phone, {mApp, TPhone, Application, Phone}SesK); + send_1(Application,Phone, {mApp, 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); + recv_2(Phone,Application, {mApp, mPhone}SesK); claim_application2(Application, Secret, SesK); claim_phone1(Application, Commit, Phone, mApp); @@ -100,10 +88,10 @@ protocol protocolPI(Network, Application, Phone) { 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)); + 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)}k(Network, Phone), {SesK, tl}k(Network, Phone), {Network, Application, Phone, tl}k(Network, Application)); + send_keysPhone(Network,Phone, {H1(SesK, tl, Application)}k(Network, Phone), {SesK, tl, Application}k(Network, Phone)); claim_network3(Network, Secret, SesK); } diff --git a/secondcw/ag01598_6644818_1_3_complex_solution.spdl b/secondcw/ag01598_6644818_1_3_complex_solution.spdl new file mode 100644 index 0000000..5f1112b --- /dev/null +++ b/secondcw/ag01598_6644818_1_3_complex_solution.spdl @@ -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); + } + + +} +