Added IKE .spdl files (auto-generated from the .cpp files) for reference.

gui/Protocols/IKE/ikev1-pk-a1.spdl

@@ -0,0 +1,129 @@
+# 1 "ikev1-pk-a1.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk-a1.cpp"
+# 17 "ikev1-pk-a1.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-pk-a1.cpp" 2
+# 27 "ikev1-pk-a1.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I) );
+  send_!O4( O, O, prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-pk-a1(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), {I}pk(R), {Ni}pk(R) );
+  recv_!2( R, I, Ci, Cr, algo, Gr, {R}pk(I), {Nr}pk(I), prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, {I}pk(R), {Ni}pk(R) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!2( R, I, Ci, Cr, algo, g(r), {R}pk(I), {Nr}pk(I), prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk-a12.spdl

@@ -0,0 +1,128 @@
+# 1 "ikev1-pk-a12.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk-a12.cpp"
+# 17 "ikev1-pk-a12.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-pk-a12.cpp" 2
+# 27 "ikev1-pk-a12.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+
+protocol ikev1-pk-a12(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), {I}pk(R), {Ni}pk(R) );
+  recv_!2( R, I, Ci, Cr, algo, Gr, {R}pk(I), {Nr}pk(I), prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!3( I, R, Ci, Cr, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, {I}pk(R), {Ni}pk(R) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!2( R, I, Ci, Cr, algo, g(r), {R}pk(I), {Nr}pk(I), prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk-a2.spdl

@@ -0,0 +1,129 @@
+# 1 "ikev1-pk-a2.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk-a2.cpp"
+# 18 "ikev1-pk-a2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 19 "ikev1-pk-a2.cpp" 2
+# 28 "ikev1-pk-a2.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I) );
+  send_!O4( O, O, prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-pk-a2(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), {I,Ni}pk(R) );
+  recv_!2( R, I, Ci, Cr, algo, Gr, {R,Nr}pk(I), prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, {I,Ni}pk(R) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!2( R, I, Ci, Cr, algo, g(r), {R,Nr}pk(I), prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk-a22.spdl

@@ -0,0 +1,128 @@
+# 1 "ikev1-pk-a22.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk-a22.cpp"
+# 17 "ikev1-pk-a22.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-pk-a22.cpp" 2
+# 27 "ikev1-pk-a22.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+
+protocol ikev1-pk-a22(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), {I,Ni}pk(R) );
+  recv_!2( R, I, Ci, Cr, algo, Gr, {R,Nr}pk(I), prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!3( I, R, Ci, Cr, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, {I,Ni}pk(R) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!2( R, I, Ci, Cr, algo, g(r), {R,Nr}pk(I), prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk-m.spdl

@@ -0,0 +1,136 @@
+# 1 "ikev1-pk-m.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk-m.cpp"
+# 16 "ikev1-pk-m.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 17 "ikev1-pk-m.cpp" 2
+# 27 "ikev1-pk-m.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O2( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+
+ }
+
+
+}
+
+
+protocol ikev1-pk-m(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, g(i), {I}pk(R), {Ni}pk(R) );
+  recv_4( R, I, Ci, Cr, Gr, {R}pk(I), {Nr}pk(I) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+  recv_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, Gi, {I}pk(R), {Ni}pk(R) );
+  send_4( R, I, Ci, Cr, g(r), {R}pk(I), {Nr}pk(I) );
+  recv_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk-m2.spdl

@@ -0,0 +1,135 @@
+# 1 "ikev1-pk-m2.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk-m2.cpp"
+# 17 "ikev1-pk-m2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-pk-m2.cpp" 2
+# 27 "ikev1-pk-m2.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O2( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+
+ }
+
+
+}
+
+protocol ikev1-pk-m2(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, g(i), {I,Ni}pk(R) );
+  recv_4( R, I, Ci, Cr, Gr, {R,Nr}pk(I) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+  recv_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, Gi, {I,Ni}pk(R) );
+  send_4( R, I, Ci, Cr, g(r), {R,Nr}pk(I) );
+  recv_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk2-a.spdl

@@ -0,0 +1,129 @@
+# 1 "ikev1-pk2-a.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk2-a.cpp"
+# 16 "ikev1-pk2-a.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 17 "ikev1-pk2-a.cpp" 2
+# 28 "ikev1-pk2-a.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I) );
+  send_!O4( O, O, prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-pk2-a(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, {Ni}pk(R), {g(i)}prf(Ni, Ci), {I}prf(Ni, Ci) );
+  recv_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {Gr}prf(Nr, Cr), {R}prf(Nr, Cr), prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, {Ni}pk(R), {Gi}prf(Ni, Ci), {I}prf(Ni, Ci) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {g(r)}prf(Nr, Cr), {R}prf(Nr, Cr), prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk2-a2.spdl

@@ -0,0 +1,128 @@
+# 1 "ikev1-pk2-a2.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk2-a2.cpp"
+# 17 "ikev1-pk2-a2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-pk2-a2.cpp" 2
+# 29 "ikev1-pk2-a2.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I) );
+  send_!O4( O, O, prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I) );
+
+ }
+
+
+}
+
+protocol ikev1-pk2-a2(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, {Ni}pk(R), {g(i),I}prf(Ni, Ci) );
+  recv_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {Gr,R}prf(Nr, Cr), prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, {Ni}pk(R), {Gi,I}prf(Ni, Ci) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {g(r),R}prf(Nr, Cr), prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk2-m.spdl

@@ -0,0 +1,136 @@
+# 1 "ikev1-pk2-m.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk2-m.cpp"
+# 16 "ikev1-pk2-m.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 17 "ikev1-pk2-m.cpp" 2
+# 28 "ikev1-pk2-m.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O2( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+
+ }
+
+
+}
+
+
+protocol ikev1-pk2-m(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, {Ni}pk(R), {g(i)}prf(Ni, Ci), {I}prf(Ni, Ci) );
+  recv_4( R, I, Ci, Cr, {Nr}pk(I), {Gr}prf(Nr, Cr), {R}prf(Nr, Cr) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+  recv_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, {Ni}pk(R), {Gi}prf(Ni, Ci), {I}prf(Ni, Ci) );
+  send_4( R, I, Ci, Cr, {Nr}pk(I), {g(r)}prf(Nr, Cr), {R}prf(Nr, Cr) );
+  recv_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-pk2-m2.spdl

@@ -0,0 +1,136 @@
+# 1 "ikev1-pk2-m2.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-pk2-m2.cpp"
+# 17 "ikev1-pk2-m2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-pk2-m2.cpp" 2
+# 30 "ikev1-pk2-m2.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O2( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+
+ }
+
+
+}
+
+
+protocol ikev1-pk2-m2(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, {Ni}pk(R), {g(i),I}prf(Ni, Ci) );
+  recv_4( R, I, Ci, Cr, {Nr}pk(I), {Gr,R}prf(Nr, Cr) );
+  claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr );
+  send_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+  recv_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, g(i),Gr,Ci,Cr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, {Ni}pk(R), {Gi,I}prf(Ni, Ci) );
+  send_4( R, I, Ci, Cr, {Nr}pk(I), {g(r),R}prf(Nr, Cr) );
+  recv_!5( I, R, Ci, Cr, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr );
+  send_!6( R, I, Ci, Cr, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Gi,g(r),Ci,Cr,Ni,Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-psk-a.spdl

@@ -0,0 +1,125 @@
+# 1 "ikev1-psk-a.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-psk-a.cpp"
+# 16 "ikev1-psk-a.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+
+
+
+  var Ci, Cr: Nonce;
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, prf(k(I,R), Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, prf(k(R,I), Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 17 "ikev1-psk-a.cpp" 2
+# 25 "ikev1-psk-a.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(k(R,I), Ni, Nr, g(r), g(i), Cr, Ci, list, R) );
+  send_!O2( O, O, prf(k(I,R), Ni, Nr, g(r), g(i), Cr, Ci, list, R) );
+
+
+  recv_!O3( O, O, prf(k(I,R), Ni, Nr, g(i), g(r), Ci, Cr, list, I) );
+  send_!O4( O, O, prf(k(R,I), Ni, Nr, g(i), g(r), Ci, Cr, list, I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-psk-a(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), Ni, I );
+  recv_!2( R, I, Ci, Cr, algo, Gr, Nr, R, prf(k(I,R), Ni, Nr, Gr, g(i), Cr, Ci, list, R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!3( I, R, Ci, Cr, prf(k(I,R), Ni, Nr, g(i), Gr, Ci, Cr, list, I) );
+
+
+  claim( I, SKR, prf(k(I,R), Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, Ni, I );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!2( R, I, Ci, Cr, algo, g(r), Nr, R, prf(k(R,I), Ni, Nr, g(r), Gi, Cr, Ci, list, R) );
+  recv_!3( I, R, Ci, Cr, prf(k(R,I), Ni, Nr, Gi, g(r), Ci, Cr, list, I) );
+
+
+  claim( R, SKR, prf(k(R,I), Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-psk-m-perlman.spdl

@@ -0,0 +1,131 @@
+# 1 "ikev1-psk-m-perlman.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-psk-m-perlman.cpp"
+# 17 "ikev1-psk-m-perlman.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+
+
+
+  var Ci, Cr: Nonce;
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, prf(k(I,R), Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, prf(k(R,I), Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-psk-m-perlman.cpp" 2
+# 26 "ikev1-psk-m-perlman.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {I, prf(k(I,R), Ni, Nr, g(i), g(r), Ci, Cr, list, I)}h(g(r),i) );
+  send_!O2( O, O, {I, prf(k(R,I), Ni, Nr, g(i), g(r), Ci, Cr, list, I)}h(g(i),r) );
+
+
+  recv_!O3( O, O, {R, prf(k(R,I), Ni, Nr, g(r), g(i), Cr, Ci, list, R)}h(g(i),r) );
+  send_!O4( O, O, {R, prf(k(I,R), Ni, Nr, g(r), g(i), Cr, Ci, list, R)}h(g(r),i) );
+
+ }
+
+
+}
+
+
+protocol ikev1-psk-m-perlman(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, g(i), Ni );
+  recv_4( R, I, Ci, Cr, Gr, Nr );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!5( I, R, Ci, Cr, {I, prf(k(I,R), Ni, Nr, g(i), Gr, Ci, Cr, list, I)}h(Gr,i) );
+  recv_!6( R, I, Ci, Cr, {R, prf(k(I,R), Ni, Nr, Gr, g(i), Cr, Ci, list, R)}h(Gr,i) );
+
+
+  claim( I, SKR, prf(k(I,R), Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, Gi, Ni );
+  send_4( R, I, Ci, Cr, g(r), Nr );
+  recv_!5( I, R, Ci, Cr, {I, prf(k(R,I), Ni, Nr, Gi, g(r), Ci, Cr, list, I)}h(Gi,r) );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!6( R, I, Ci, Cr, {R, prf(k(R,I), Ni, Nr, g(r), Gi, Cr, Ci, list, R)}h(Gi,r) );
+
+
+  claim( R, SKR, prf(k(R,I), Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-psk-m.spdl

@@ -0,0 +1,130 @@
+# 1 "ikev1-psk-m.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-psk-m.cpp"
+# 16 "ikev1-psk-m.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+
+
+
+  var Ci, Cr: Nonce;
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, prf(k(I,R), Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, prf(k(R,I), Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 17 "ikev1-psk-m.cpp" 2
+# 26 "ikev1-psk-m.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {I, prf(k(I,R), Ni, Nr, g(i), g(r), Ci, Cr, list, I)}prf(k(I,R), Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O2( O, O, {I, prf(k(R,I), Ni, Nr, g(i), g(r), Ci, Cr, list, I)}prf(k(R,I), Ni, Nr, h(g(i),r), Ci, Cr) );
+
+
+  recv_!O3( O, O, {R, prf(k(R,I), Ni, Nr, g(r), g(i), Cr, Ci, list, R)}prf(k(R,I), Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O4( O, O, {R, prf(k(I,R), Ni, Nr, g(r), g(i), Cr, Ci, list, R)}prf(k(I,R), Ni, Nr, h(g(r),i), Ci, Cr) );
+
+ }
+
+
+}
+
+protocol ikev1-psk-m(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, g(i), Ni );
+  recv_4( R, I, Ci, Cr, Gr, Nr );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!5( I, R, Ci, Cr, {I, prf(k(I,R), Ni, Nr, g(i), Gr, Ci, Cr, list, I)}prf(k(I,R), Ni, Nr, h(Gr,i), Ci, Cr) );
+  recv_!6( R, I, Ci, Cr, {R, prf(k(I,R), Ni, Nr, Gr, g(i), Cr, Ci, list, R)}prf(k(I,R), Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, prf(k(I,R), Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, Gi, Ni );
+  send_4( R, I, Ci, Cr, g(r), Nr );
+  recv_!5( I, R, Ci, Cr, {I, prf(k(R,I), Ni, Nr, Gi, g(r), Ci, Cr, list, I)}prf(k(R,I), Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!6( R, I, Ci, Cr, {R, prf(k(R,I), Ni, Nr, g(r), Gi, Cr, Ci, list, R)}prf(k(R,I), Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, prf(k(R,I), Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-quick-noid.spdl

@@ -0,0 +1,124 @@
+# 1 "ikev1-quick-noid.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-quick-noid.cpp"
+# 16 "ikev1-quick-noid.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 126 "common.h"
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(k(I,R),h(g(r),i),Ni,Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(k(R,I),h(g(i),r),Ni,Nr) );
+
+ }
+
+
+}
+# 17 "ikev1-quick-noid.cpp" 2
+# 27 "ikev1-quick-noid.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var mid, i, r, Ni, Nr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(k(I,R), mid, list, Ni, g(i)), list, Ni, g(i)}k(I,R) );
+  send_!O2( O, O, {prf(k(R,I), mid, list, Ni, g(i)), list, Ni, g(i)}k(R,I) );
+
+
+  recv_!O3( O, O, {prf(k(R,I), mid, Ni, algo, Nr, g(r)), algo, Nr, g(r)}k(R,I) );
+  send_!O4( O, O, {prf(k(I,R), mid, Ni, algo, Nr, g(r)), algo, Nr, g(r)}k(I,R) );
+
+
+  recv_!O5( O, O, {prf(k(I,R), mid, Ni, Nr)}k(I,R) );
+  send_!O6( O, O, {prf(k(R,I), mid, Ni, Nr)}k(R,I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-quick-noid(I, R)
+{
+ role I {
+  fresh i, Ni, Ci, mid: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_!1( I, R, mid, {prf(k(I,R), mid, list, Ni, g(i)), list, Ni, g(i)}k(I,R) );
+  recv_!2( R, I, mid, {prf(k(I,R), mid, Ni, algo, Nr, Gr), algo, Nr, Gr}k(I,R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr );
+  send_!3( I, R, mid, {prf(k(I,R), mid, Ni, Nr)}k(I,R) );
+
+
+  claim( I, SKR, KDF(k(I,R),h(Gr,i),Ni,Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci, mid: Nonce;
+  var Gi: Ticket;
+
+  recv_!1( I, R, mid, {prf(k(R,I), mid, list, Ni, Gi), list, Ni, Gi}k(R,I) );
+  claim( R, Running, I, Ni, Nr, Gi, g(r) );
+  send_!2( R, I, mid, {prf(k(R,I), mid, Ni, algo, Nr, g(r)), algo, Nr, g(r)}k(R,I) );
+  recv_!3( I, R, mid, {prf(k(R,I), mid, Ni, Nr)}k(R,I) );
+
+
+
+  claim( R, SKR, KDF(k(R,I),h(Gi,r),Ni,Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r) );
+
+ }
+}

gui/Protocols/IKE/ikev1-quick-nopfs.spdl

@@ -0,0 +1,118 @@
+# 1 "ikev1-quick-nopfs.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-quick-nopfs.cpp"
+# 16 "ikev1-quick-nopfs.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 129 "common.h"
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(k(I,R),Ni,Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(k(R,I),Ni,Nr) );
+
+ }
+
+
+}
+# 17 "ikev1-quick-nopfs.cpp" 2
+# 27 "ikev1-quick-nopfs.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+protocol @executability(O) {
+ role O {
+  var mid, Ni, Nr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(k(I,R), mid, list, Ni), list, Ni}k(I,R) );
+  send_!O2( O, O, {prf(k(R,I), mid, list, Ni), list, Ni}k(R,I) );
+
+
+  recv_!O3( O, O, {prf(k(R,I), mid, Ni, algo, Nr), algo, Nr}k(R,I) );
+  send_!O4( O, O, {prf(k(I,R), mid, Ni, algo, Nr), algo, Nr}k(I,R) );
+
+
+  recv_!O5( O, O, {prf(k(I,R), mid, Ni, Nr)}k(I,R) );
+  send_!O6( O, O, {prf(k(R,I), mid, Ni, Nr)}k(R,I) );
+
+ }
+}
+
+
+protocol ikev1-quick-nopfs(I, R)
+{
+ role I {
+  fresh i, Ni, Ci, mid: Nonce;
+  var Nr, Cr: Nonce;
+
+  send_!1( I, R, mid, {prf(k(I,R), mid, list, Ni), list, Ni}k(I,R) );
+  recv_!2( R, I, mid, {prf(k(I,R), mid, Ni, algo, Nr), algo, Nr}k(I,R) );
+  claim( I, Running, R, Ni, Nr );
+  send_!3( I, R, mid, {prf(k(I,R), mid, Ni, Nr)}k(I,R) );
+
+
+  claim( I, SKR, KDF(k(I,R),Ni,Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci, mid: Nonce;
+
+  recv_!1( I, R, mid, {prf(k(R,I), mid, list, Ni), list, Ni}k(R,I) );
+  claim( R, Running, I, Ni, Nr );
+  send_!2( R, I, mid, {prf(k(R,I), mid, Ni, algo, Nr), algo, Nr}k(R,I) );
+  recv_!3( I, R, mid, {prf(k(R,I), mid, Ni, Nr)}k(R,I) );
+
+
+
+  claim( R, SKR, KDF(k(R,I),Ni,Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr );
+
+ }
+}

gui/Protocols/IKE/ikev1-quick.spdl

@@ -0,0 +1,91 @@
+# 1 "ikev1-quick.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-quick.cpp"
+# 16 "ikev1-quick.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 126 "common.h"
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(k(I,R),h(g(r),i),Ni,Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(k(R,I),h(g(i),r),Ni,Nr) );
+
+ }
+
+
+}
+# 17 "ikev1-quick.cpp" 2
+# 28 "ikev1-quick.cpp"
+protocol ikev1-quick(I, R)
+{
+ role I {
+  fresh i, Ni, Ci, mid, list: Nonce;
+  var Nr, Cr, algo: Nonce;
+  var Gr: Ticket;
+
+  send_!1( I, R, mid, {prf(k(I,R), mid, list, Ni, g(i), I, R), list, Ni, g(i), I, R}k(I,R) );
+  recv_!2( R, I, mid, {prf(k(I,R), mid, Ni, algo, Nr, Gr, I, R), algo, Nr, Gr, I, R}k(I,R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr );
+  send_!3( I, R, mid, {prf(k(I,R), mid, Ni, Nr)}k(I,R) );
+
+
+  claim( I, SKR, KDF(k(I,R),h(Gr,i),Ni,Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr, algo: Nonce;
+  var Ni, Ci, mid, list: Nonce;
+  var Gi: Ticket;
+
+  recv_!1( I, R, mid, {prf(k(R,I), mid, list, Ni, Gi, I, R), list, Ni, Gi, I, R}k(I,R) );
+  claim( R, Running, I, Ni, Nr, Gi, g(r) );
+  send_!2( R, I, mid, {prf(k(R,I), mid, Ni, algo, Nr, g(r), I, R), algo, Nr, g(r), I, R}k(I,R) );
+  recv_!3( I, R, mid, {prf(k(R,I), mid, Ni, Nr)}k(I,R) );
+
+
+
+  claim( R, SKR, KDF(k(R,I),h(Gi,r),Ni,Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r) );
+
+ }
+}

gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl

@@ -0,0 +1,130 @@
+# 1 "ikev1-sig-a-perlman1.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-sig-a-perlman1.cpp"
+# 18 "ikev1-sig-a-perlman1.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 19 "ikev1-sig-a-perlman1.cpp" 2
+# 29 "ikev1-sig-a-perlman1.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {R}KDF(Ni, Nr, h(g(i),r), Ci, Cr), {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+  send_!O2( O, O, {R}KDF(Ni, Nr, h(g(r),i), Ci, Cr), {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+
+
+  recv_!O3( O, O, {I}KDF(Ni, Nr, h(g(r),i), Ci, Cr), {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}sk(I) );
+  send_!O4( O, O, {I}KDF(Ni, Nr, h(g(i),r), Ci, Cr), {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}sk(I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-sig-a-perlman1(I, R)
+{
+
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), Ni );
+  recv_!2( R, I, (Ci,Cr), algo, Gr, Nr, {R}KDF(Ni, Nr, h(Gr,i), Ci, Cr), {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}sk(R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!3( I, R, (Ci,Cr), {I}KDF(Ni, Nr, h(Gr,i), Ci, Cr), {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}sk(I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, Ni );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!2( R, I, (Ci,Cr), algo, g(r), Nr, R, {R}KDF(Ni, Nr, h(Gi,r), Ci, Cr), {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}sk(R) );
+  recv_!3( I, R, (Ci,Cr), {I}KDF(Ni, Nr, h(Gi,r), Ci, Cr), {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}sk(I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl

@@ -0,0 +1,130 @@
+# 1 "ikev1-sig-a-perlman2.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-sig-a-perlman2.cpp"
+# 18 "ikev1-sig-a-perlman2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 19 "ikev1-sig-a-perlman2.cpp" 2
+# 29 "ikev1-sig-a-perlman2.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {R}KDF(Ni, Nr, h(g(i),r), Ci, Cr), {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+  send_!O2( O, O, {R}KDF(Ni, Nr, h(g(r),i), Ci, Cr), {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+
+
+  recv_!O3( O, O, {I, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O4( O, O, {I, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+
+
+protocol ikev1-sig-a-perlman2(I, R)
+{
+
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), Ni );
+  recv_!2( R, I, (Ci,Cr), algo, Gr, Nr, {R}KDF(Ni, Nr, h(Gr,i), Ci, Cr), {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}sk(R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!3( I, R, (Ci,Cr), {I, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, Ni );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!2( R, I, (Ci,Cr), algo, g(r), Nr, R, {R}KDF(Ni, Nr, h(Gi,r), Ci, Cr), {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}sk(R) );
+  recv_!3( I, R, (Ci,Cr), {I, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-sig-a1.spdl

@@ -0,0 +1,130 @@
+# 1 "ikev1-sig-a1.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-sig-a1.cpp"
+# 17 "ikev1-sig-a1.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-sig-a1.cpp" 2
+# 28 "ikev1-sig-a1.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+  send_!O2( O, O, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+
+
+  recv_!O3( O, O, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}sk(I) );
+  send_!O4( O, O, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}sk(I) );
+
+ }
+
+
+}
+
+
+protocol ikev1-sig-a1(I, R)
+{
+
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), Ni, I );
+  recv_!2( R, I, (Ci,Cr), algo, Gr, Nr, R, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}sk(R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!3( I, R, (Ci,Cr), {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}sk(I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, Ni, I );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!2( R, I, (Ci,Cr), algo, g(r), Nr, R, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}sk(R) );
+  recv_!3( I, R, (Ci,Cr), {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}sk(I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-sig-a2.spdl

@@ -0,0 +1,130 @@
+# 1 "ikev1-sig-a2.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-sig-a2.cpp"
+# 17 "ikev1-sig-a2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-sig-a2.cpp" 2
+# 29 "ikev1-sig-a2.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+  send_!O2( O, O, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}sk(R) );
+
+
+  recv_!O3( O, O, {{prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O4( O, O, {{prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+
+
+protocol ikev1-sig-a2(I, R)
+{
+
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list, g(i), Ni, I );
+  recv_!2( R, I, (Ci,Cr), algo, Gr, Nr, R, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}sk(R) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!3( I, R, (Ci,Cr), {{prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list, Gi, Ni, I );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!2( R, I, (Ci,Cr), algo, g(r), Nr, R, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}sk(R) );
+  recv_!3( I, R, (Ci,Cr), {{prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-sig-m-perlman.spdl

@@ -0,0 +1,133 @@
+# 1 "ikev1-sig-m-perlman.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-sig-m-perlman.cpp"
+# 17 "ikev1-sig-m-perlman.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 18 "ikev1-sig-m-perlman.cpp" 2
+# 27 "ikev1-sig-m-perlman.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {R, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O2( O, O, {R, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+
+
+  recv_!O3( O, O, {I, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O4( O, O, {I, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+
+
+protocol ikev1-sig-m-perlman(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, Ci, Cr, algo );
+  send_3( I, R, Ci, Cr, g(i), Ni );
+  recv_!4( R, I, Ci, Cr, Gr, Nr, {R, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!5( I, R, Ci, Cr, {I, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, Ci, Cr, algo );
+  recv_3( I, R, Ci, Cr, Gi, Ni );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!4( R, I, Ci, Cr, g(r), Nr, {R, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  recv_!5( I, R, Ci, Cr, {I, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev1-sig-m.spdl

@@ -0,0 +1,134 @@
+# 1 "ikev1-sig-m.cpp"
+# 1 "<command-line>"
+# 1 "ikev1-sig-m.cpp"
+# 16 "ikev1-sig-m.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+
+
+
+
+
+
+
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+
+
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 17 "ikev1-sig-m.cpp" 2
+# 28 "ikev1-sig-m.cpp"
+usertype String;
+const list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {I, {prf(Ni, Nr, h(g(r),i), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!O2( O, O, {I, {prf(Ni, Nr, h(g(i),r), g(i), g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+
+  recv_!O3( O, O, {R, {prf(Ni, Nr, h(g(i),r), g(r), g(i), Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+  send_!O4( O, O, {R, {prf(Ni, Nr, h(g(r),i), g(r), g(i), Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+
+ }
+
+
+}
+
+protocol ikev1-sig-m(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, list );
+  recv_2( R, I, (Ci,Cr), algo );
+  send_3( I, R, (Ci,Cr), g(i), Ni );
+  recv_4( R, I, (Ci,Cr), Gr, Nr );
+  claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr );
+  send_!5( I, R, (Ci,Cr), {I, {prf(Ni, Nr, h(Gr,i), g(i), Gr, Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+  recv_!6( R, I, (Ci,Cr), {R, {prf(Ni, Nr, h(Gr,i), Gr, g(i), Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni, Nr, g(i), Gr, Ci, Cr );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, list );
+  send_2( R, I, (Ci,Cr), algo );
+  recv_3( I, R, (Ci,Cr), Gi, Ni );
+  send_4( R, I, (Ci,Cr), g(r), Nr );
+  recv_!5( I, R, (Ci,Cr), {I, {prf(Ni, Nr, h(Gi,r), Gi, g(r), Ci, Cr, list, I)}sk(I)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr );
+  send_!6( R, I, (Ci,Cr), {R, {prf(Ni, Nr, h(Gi,r), g(r), Gi, Cr, Ci, list, R)}sk(R)}KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni, Nr, Gi, g(r), Ci, Cr );
+
+ }
+}

gui/Protocols/IKE/ikev2-child-nopfs.spdl

@@ -0,0 +1,112 @@
+# 1 "ikev2-child-nopfs.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-child-nopfs.cpp"
+# 15 "ikev2-child-nopfs.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 138 "common.h"
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(k(I,R),Ni,Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(k(R,I),Ni,Nr) );
+
+ }
+
+
+}
+# 16 "ikev2-child-nopfs.cpp" 2
+
+
+const SA3: Nonce;
+
+
+
+
+
+
+protocol @executability(O) {
+ role O {
+  var Ni, Nr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {SA3, Ni}k(I,R) );
+  send_!O2( O, O, {SA3, Ni}k(R,I) );
+
+
+  recv_!O3( O, O, {SA3, Nr}k(R,I) );
+  send_!O4( O, O, {SA3, Nr}k(I,R) );
+
+ }
+}
+
+
+protocol ikev2-child-nopfs(I, R)
+{
+
+ role I {
+  fresh Ni: Nonce;
+  var Nr: Nonce;
+
+
+  claim( I, Running, R,Ni );
+  send_!1( I, R, {SA3, Ni}k(I,R) );
+  recv_!2( R, I, {SA3, Nr}k(I,R) );
+
+
+  claim( I, SKR, KDF(k(I,R),Ni,Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,Ni,Nr );
+
+ }
+
+ role R {
+  fresh Nr: Nonce;
+  var Ni: Nonce;
+
+  recv_!1( I, R, {SA3, Ni}k(R,I) );
+  claim( R, Running, I,Ni,Nr );
+  send_!2( R, I, {SA3, Nr}k(R,I) );
+
+
+  claim( R, SKR, KDF(k(R,I),Ni,Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Ni );
+ }
+}

gui/Protocols/IKE/ikev2-child.spdl

@@ -0,0 +1,121 @@
+# 1 "ikev2-child.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-child.cpp"
+# 15 "ikev2-child.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 135 "common.h"
+  var I, R: Agent;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(k(I,R),h(g(r),i),Ni,Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(k(R,I),h(g(i),r),Ni,Nr) );
+
+ }
+
+
+}
+# 16 "ikev2-child.cpp" 2
+
+
+
+usertype SecurityAssociation;
+const SA1 ,SA2, SA3: SecurityAssociation;
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {SA3, Ni, g(i)}k(I,R) );
+  send_!O2( O, O, {SA3, Ni, g(i)}k(R,I) );
+
+
+  recv_!O3( O, O, {SA3, Nr, g(r)}k(R,I) );
+  send_!O4( O, O, {SA3, Nr, g(r)}k(I,R) );
+
+ }
+
+
+}
+
+
+
+protocol ikev2-child(I, R)
+{
+
+ role I {
+  fresh i, Ni: Nonce;
+  var Nr: Nonce;
+  var Gr: Ticket;
+
+
+  claim( I, Running, R,Ni,g(i) );
+  send_!1( I, R, {SA3, Ni, g(i)}k(I,R) );
+  recv_!2( R, I, {SA3, Nr, Gr}k(I,R) );
+
+
+  claim( I, SKR, KDF(k(I,R),h(Gr,i),Ni,Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,Ni,g(i),Nr,Gr );
+
+ }
+
+ role R {
+  fresh r, Nr: Nonce;
+  var Ni: Nonce;
+  var Gi: Ticket;
+
+  recv_!1( I, R, {SA3, Ni, Gi}k(R,I) );
+  claim( R, Running, I,Ni,Gi,Nr,g(r) );
+  send_!2( R, I, {SA3, Nr, g(r)}k(R,I) );
+
+
+  claim( R, SKR, KDF(k(R,I),h(Gi,r),Ni,Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Ni,Gi );
+ }
+}

gui/Protocols/IKE/ikev2-eap.spdl

@@ -0,0 +1,160 @@
+# 1 "ikev2-eap.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-eap.cpp"
+# 15 "ikev2-eap.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-eap.cpp" 2
+# 24 "ikev2-eap.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr, EAP, EAPOK: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E5( E, E, {EAP}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E6( E, E, {EAP}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E7( E, E, {EAPOK}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E8( E, E, {EAPOK}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E9( E, E, {{SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!EA( E, E, {{SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  send_!EB( E, E, {{SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!EC( E, E, {{SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+ }
+
+
+}
+
+
+protocol ikev2-eap(I, R)
+{
+
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var EAP, EAPOK: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  send_!3( I, R, (SPIi,SPIr), {I, R, SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  send_!5( I, R, (SPIi,SPIr), {EAP}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!6( R, I, (SPIi,SPIr), {EAPOK}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr,EAP,EAPOK );
+  send_!7( I, R, (SPIi,SPIr), {{SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!8( R, I, (SPIi,SPIr), {{SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni,g(i),Nr,Gr,TSi,TSr,EAP,EAPOK );
+
+ }
+
+ role R {
+  fresh EAP, EAPOK: Nonce;
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, R, SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  recv_!5( I, R, (SPIi,SPIr), {EAP}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!6( R, I, (SPIi,SPIr), {EAPOK}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  recv_!7( I, R, (SPIi,SPIr), {{SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr,EAP,EAPOK );
+  send_!8( R, I, (SPIi,SPIr), {{SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr,EAP,EAPOK );
+
+ }
+}

gui/Protocols/IKE/ikev2-eap2.spdl

@@ -0,0 +1,160 @@
+# 1 "ikev2-eap2.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-eap2.cpp"
+# 22 "ikev2-eap2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 23 "ikev2-eap2.cpp" 2
+# 31 "ikev2-eap2.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr, EAP, EAPOK: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E5( E, E, {EAP}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E6( E, E, {EAP}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E7( E, E, {EAPOK}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E8( E, E, {EAPOK}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E9( E, E, {{SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!EA( E, E, {{SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  send_!EB( E, E, {{SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!EC( E, E, {{SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+ }
+
+
+}
+
+
+protocol ikev2-eap2(I, R)
+{
+
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var EAP, EAPOK: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  send_!3( I, R, (SPIi,SPIr), {I, SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  send_!5( I, R, (SPIi,SPIr), {EAP}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!6( R, I, (SPIi,SPIr), {EAPOK}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr,EAP,EAPOK );
+  send_!7( I, R, (SPIi,SPIr), {{SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!8( R, I, (SPIi,SPIr), {{SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni,g(i),Nr,Gr,TSi,TSr,EAP,EAPOK );
+
+ }
+
+ role R {
+  fresh EAP, EAPOK: Nonce;
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), EAP}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  recv_!5( I, R, (SPIi,SPIr), {EAP}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!6( R, I, (SPIi,SPIr), {EAPOK}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  recv_!7( I, R, (SPIi,SPIr), {{SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I)}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr,EAP,EAPOK );
+  send_!8( R, I, (SPIi,SPIr), {{SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr,EAP,EAPOK );
+
+ }
+}

gui/Protocols/IKE/ikev2-mac.spdl

@@ -0,0 +1,133 @@
+# 1 "ikev2-mac.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-mac.cpp"
+# 15 "ikev2-mac.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-mac.cpp" 2
+# 24 "ikev2-mac.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, MAC(k(R,I), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, MAC(k(I,R), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-mac(I, R)
+{
+
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr);
+  send_!3( I, R, (SPIi,SPIr), {I, R, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni,g(i),Nr,Gr,TSi,TSr);
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, R, MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr);
+  send_!4( R, I, (SPIi,SPIr), {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr);
+ }
+}

gui/Protocols/IKE/ikev2-mac2.spdl

@@ -0,0 +1,133 @@
+# 1 "ikev2-mac2.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-mac2.cpp"
+# 15 "ikev2-mac2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-mac2.cpp" 2
+# 24 "ikev2-mac2.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, MAC(k(R,I), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, MAC(k(I,R), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-mac2(I, R)
+{
+
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr );
+  send_!3( I, R, (SPIi,SPIr), {I, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R, Ni,g(i),Nr,Gr,TSi,TSr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr );
+  send_!4( R, I, (SPIi,SPIr), {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr );
+ }
+}

gui/Protocols/IKE/ikev2-mactosig.spdl

@@ -0,0 +1,132 @@
+# 1 "ikev2-mactosig.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-mactosig.cpp"
+# 16 "ikev2-mactosig.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 17 "ikev2-mactosig.cpp" 2
+# 25 "ikev2-mactosig.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, MAC(k(R,I), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-mactosig(I, R)
+{
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr );
+
+
+  claim( I, Running, R,Ni,g(i),Nr,Gr,TSi,TSr );
+  send_!3( I, R, SPIi, SPIr, {I, R, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, SPIi, SPIr, {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,Ni,g(i),Nr,Gr,TSi,TSr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, SPIi, SPIr, SA1, g(r), Nr );
+
+
+  recv_!3( I, R, SPIi, SPIr, {I, R, MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr );
+  send_!4( R, I, SPIi, SPIr, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr );
+ }
+}

gui/Protocols/IKE/ikev2-mactosig2.spdl

@@ -0,0 +1,131 @@
+# 1 "ikev2-mactosig2.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-mactosig2.cpp"
+# 16 "ikev2-mactosig2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 17 "ikev2-mactosig2.cpp" 2
+# 25 "ikev2-mactosig2.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, MAC(k(R,I), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+protocol ikev2-mactosig2(I, R)
+{
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr );
+
+
+  claim( I, Running, R,Ni,g(i),Nr,Gr,TSi,TSr );
+  send_!3( I, R, SPIi, SPIr, {I, MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, SPIi, SPIr, {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,Ni,g(i),Nr,Gr,TSi,TSr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, SPIi, SPIr, SA1, g(r), Nr );
+
+
+  recv_!3( I, R, SPIi, SPIr, {I, MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr );
+  send_!4( R, I, SPIi, SPIr, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr );
+ }
+}

gui/Protocols/IKE/ikev2-sig-child-composed.spdl

@@ -0,0 +1,165 @@
+# 1 "ikev2-sig-child-composed.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sig-child-composed.cpp"
+# 15 "ikev2-sig-child-composed.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-sig-child-composed.cpp" 2
+# 26 "ikev2-sig-child-composed.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E5( E, E, {SA3, Mi, g(j), TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E6( E, E, {SA3, Mi, g(j), TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E7( E, E, {SA3, Mr, g(t), TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E8( E, E, {SA3, Mr, g(t), TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+ }
+
+
+}
+protocol @ora(S) {
+
+
+
+
+ role S {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+
+  recv_!S1( S, S, KDF(Ni, Nr, h(g(r),i), h(g(t),j), Mi, Mr) );
+  send_!S2( S, S, KDF(Ni, Nr, h(g(i),r), h(g(j),t), Mi, Mr) );
+ }
+
+
+
+
+}
+
+
+protocol ikev2-sig-child(I, R)
+{
+ role I {
+  fresh i, j, Ni, Mi, SPIi: Nonce;
+  var Nr, Mr, SPIr: Nonce;
+  var Gr, Gt: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  send_!3( I, R, (SPIi,SPIr), {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, Running, R,g(i),g(j),Gr );
+  send_!5( I, R, (SPIi,SPIr), {SA3, Mi, g(j), TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!6( R, I, (SPIi,SPIr), {SA3, Mr, Gt, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), h(Gt,j), Mi, Mr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),g(j),Gr,Gt );
+
+ }
+
+ role R {
+  fresh r, t, Nr, Mr, SPIr: Nonce;
+  var Ni, Mi, SPIi: Nonce;
+  var Gi, Gj: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, R, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  recv_!5( I, R, (SPIi,SPIr), {SA3, Mi, Gj, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,Gj,g(r),g(t) );
+  send_!6( R, I, (SPIi,SPIr), {SA3, Mr, g(t), TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), h(Gi,t), Mi, Mr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,Gj,g(r) );
+ }
+}

gui/Protocols/IKE/ikev2-sig-child.spdl

@@ -0,0 +1,165 @@
+# 1 "ikev2-sig-child.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sig-child.cpp"
+# 15 "ikev2-sig-child.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-sig-child.cpp" 2
+# 26 "ikev2-sig-child.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E5( E, E, {SA3, Mi, g(j), TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E6( E, E, {SA3, Mi, g(j), TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E7( E, E, {SA3, Mr, g(t), TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E8( E, E, {SA3, Mr, g(t), TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+ }
+
+
+}
+protocol @ora(S) {
+
+
+
+
+ role S {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+
+  recv_!S1( S, S, KDF(Ni, Nr, h(g(r),i), h(g(t),j), Mi, Mr) );
+  send_!S2( S, S, KDF(Ni, Nr, h(g(i),r), h(g(j),t), Mi, Mr) );
+ }
+
+
+
+
+}
+
+
+protocol ikev2-sig-child(I, R)
+{
+ role I {
+  fresh i, j, Ni, Mi, SPIi: Nonce;
+  var Nr, Mr, SPIr: Nonce;
+  var Gr, Gt: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  send_!3( I, R, (SPIi,SPIr), {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, Running, R,g(i),g(j),Gr );
+  send_!5( I, R, (SPIi,SPIr), {SA3, Mi, g(j), TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!6( R, I, (SPIi,SPIr), {SA3, Mr, Gt, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), h(Gt,j), Mi, Mr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),g(j),Gr,Gt );
+
+ }
+
+ role R {
+  fresh r, t, Nr, Mr, SPIr: Nonce;
+  var Ni, Mi, SPIi: Nonce;
+  var Gi, Gj: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, R, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  recv_!5( I, R, (SPIi,SPIr), {SA3, Mi, Gj, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,Gj,g(r),g(t) );
+  send_!6( R, I, (SPIi,SPIr), {SA3, Mr, g(t), TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), h(Gi,t), Mi, Mr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,Gj,g(r) );
+ }
+}

gui/Protocols/IKE/ikev2-sig-child2-composed.spdl

@@ -0,0 +1,165 @@
+# 1 "ikev2-sig-child2-composed.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sig-child2-composed.cpp"
+# 15 "ikev2-sig-child2-composed.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-sig-child2-composed.cpp" 2
+# 26 "ikev2-sig-child2-composed.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E5( E, E, {SA3, Mi, g(j)}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E6( E, E, {SA3, Mi, g(j)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E7( E, E, {SA3, Mr, g(t)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E8( E, E, {SA3, Mr, g(t)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+ }
+
+
+}
+protocol @ora(S) {
+
+
+
+
+ role S {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+
+  recv_!S1( S, S, KDF(Ni, Nr, h(g(r),i), h(g(t),j), Mi, Mr) );
+  send_!S2( S, S, KDF(Ni, Nr, h(g(i),r), h(g(j),t), Mi, Mr) );
+ }
+
+
+
+
+}
+
+
+protocol ikev2-sig-child2(I, R)
+{
+ role I {
+  fresh i, j, Ni, Mi, SPIi: Nonce;
+  var Nr, Mr, SPIr: Nonce;
+  var Gr, Gt: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  send_!3( I, R, (SPIi,SPIr), {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, Running, R,g(i),g(j),Gr );
+  send_!5( I, R, (SPIi,SPIr), {SA3, Mi, g(j)}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!6( R, I, (SPIi,SPIr), {SA3, Mr, Gt}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), h(Gt,j), Mi, Mr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),g(j),Gr,Gt );
+
+ }
+
+ role R {
+  fresh r, t, Nr, Mr, SPIr: Nonce;
+  var Ni, Mi, SPIi: Nonce;
+  var Gi, Gj: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  recv_!5( I, R, (SPIi,SPIr), {SA3, Mi, Gj}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,Gj,g(r),g(t) );
+  send_!6( R, I, (SPIi,SPIr), {SA3, Mr, g(t)}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), h(Gi,t), Mi, Mr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,Gj,g(r) );
+ }
+}

gui/Protocols/IKE/ikev2-sig-child2.spdl

@@ -0,0 +1,165 @@
+# 1 "ikev2-sig-child2.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sig-child2.cpp"
+# 15 "ikev2-sig-child2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-sig-child2.cpp" 2
+# 26 "ikev2-sig-child2.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+
+  recv_!E5( E, E, {SA3, Mi, g(j)}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E6( E, E, {SA3, Mi, g(j)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E7( E, E, {SA3, Mr, g(t)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E8( E, E, {SA3, Mr, g(t)}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+ }
+
+
+}
+protocol @ora(S) {
+
+
+
+
+ role S {
+  var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce;
+
+  recv_!S1( S, S, KDF(Ni, Nr, h(g(r),i), h(g(t),j), Mi, Mr) );
+  send_!S2( S, S, KDF(Ni, Nr, h(g(i),r), h(g(j),t), Mi, Mr) );
+ }
+
+
+
+
+}
+
+
+protocol ikev2-sig-child2(I, R)
+{
+ role I {
+  fresh i, j, Ni, Mi, SPIi: Nonce;
+  var Nr, Mr, SPIr: Nonce;
+  var Gr, Gt: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  send_!3( I, R, (SPIi,SPIr), {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, Running, R,g(i),g(j),Gr );
+  send_!5( I, R, (SPIi,SPIr), {SA3, Mi, g(j)}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!6( R, I, (SPIi,SPIr), {SA3, Mr, Gt}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), h(Gt,j), Mi, Mr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),g(j),Gr,Gt );
+
+ }
+
+ role R {
+  fresh r, t, Nr, Mr, SPIr: Nonce;
+  var Ni, Mi, SPIi: Nonce;
+  var Gi, Gj: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  recv_!5( I, R, (SPIi,SPIr), {SA3, Mi, Gj}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,Gj,g(r),g(t) );
+  send_!6( R, I, (SPIi,SPIr), {SA3, Mr, g(t)}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), h(Gi,t), Mi, Mr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,Gj,g(r) );
+ }
+}

gui/Protocols/IKE/ikev2-sig.spdl

@@ -0,0 +1,132 @@
+# 1 "ikev2-sig.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sig.cpp"
+# 15 "ikev2-sig.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-sig.cpp" 2
+# 24 "ikev2-sig.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-sig(I, R)
+{
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  claim( I, Running, R,g(i),Gr,Ni,Nr );
+  send_!3( I, R, (SPIi,SPIr), {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),Gr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, R, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,g(r),Ni,Nr );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,g(r),Ni,Nr );
+ }
+}

gui/Protocols/IKE/ikev2-sig2.spdl

@@ -0,0 +1,132 @@
+# 1 "ikev2-sig2.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sig2.cpp"
+# 15 "ikev2-sig2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 16 "ikev2-sig2.cpp" 2
+# 24 "ikev2-sig2.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-sig2(I, R)
+{
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, (SPIi,SPIr), SA1, Gr, Nr );
+
+
+  claim( I, Running, R,Ni,g(i),Nr,Gr,TSi,TSr );
+  send_!3( I, R, (SPIi,SPIr), {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,Ni,g(i),Nr,Gr,TSi,TSr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, (SPIi,SPIr), SA1, g(r), Nr );
+
+
+  recv_!3( I, R, (SPIi,SPIr), {I, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr );
+  send_!4( R, I, (SPIi,SPIr), {R, {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)}sk(R), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I, Ni,Gi,Nr,g(r),TSi,TSr );
+ }
+}

gui/Protocols/IKE/ikev2-sigtomac.spdl

@@ -0,0 +1,132 @@
+# 1 "ikev2-sigtomac.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sigtomac.cpp"
+# 16 "ikev2-sigtomac.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 17 "ikev2-sigtomac.cpp" 2
+# 25 "ikev2-sigtomac.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, MAC(k(I,R), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-sigtomac(I, R)
+{
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr );
+
+
+  claim( I, Running, R,g(i),Gr,Ni,Nr );
+  send_!3( I, R, SPIi, SPIr, {I, R, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, SPIi, SPIr, {R, MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),Gr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, SPIi, SPIr, SA1, g(r), Nr );
+
+
+  recv_!3( I, R, SPIi, SPIr, {I, R, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,g(r),Ni,Nr );
+  send_!4( R, I, SPIi, SPIr, {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,g(r),Ni,Nr );
+ }
+}

gui/Protocols/IKE/ikev2-sigtomac2.spdl

@@ -0,0 +1,132 @@
+# 1 "ikev2-sigtomac2.cpp"
+# 1 "<command-line>"
+# 1 "ikev2-sigtomac2.cpp"
+# 16 "ikev2-sigtomac2.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 43 "common.h"
+hashfunction MAC;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 132 "common.h"
+  var SPIi, SPIr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+ }
+
+
+}
+# 17 "ikev2-sigtomac2.cpp" 2
+# 25 "ikev2-sigtomac2.cpp"
+usertype Number, SecurityAssociation, TrafficSelector;
+const O: Number;
+const SA1 ,SA2, SA3: SecurityAssociation;
+const TSi, TSr: TrafficSelector;
+
+
+
+
+
+
+protocol @executability(E) {
+
+
+ role E {
+  var i, r, Ni, Nr, SPIi, SPIr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!E1( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+  send_!E2( E, E, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+
+
+  recv_!E3( E, E, {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(i),r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(i),r),SPIi,SPIr) );
+  send_!E4( E, E, {R, MAC(k(I,R), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(g(r),i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(g(r),i),SPIi,SPIr) );
+
+ }
+
+
+}
+
+
+protocol ikev2-sigtomac2(I, R)
+{
+ role I {
+  fresh i, Ni, SPIi: Nonce;
+  var Nr, SPIr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, SPIi, O, SA1, g(i), Ni );
+  recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr );
+
+
+  claim( I, Running, R,g(i),Gr,Ni,Nr );
+  send_!3( I, R, SPIi, SPIr, {I, {SPIi, O, SA1, g(i), Ni, Nr, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+  recv_!4( R, I, SPIi, SPIr, {R, MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(KDF(Ni,Nr,h(Gr,i),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+
+  claim( I, SKR, KDF(Ni,Nr,h(Gr,i),SPIi,SPIr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+  claim( I, Commit, R,g(i),Gr,Ni,Nr );
+
+ }
+
+ role R {
+  fresh r, Nr, SPIr: Nonce;
+  var Ni, SPIi: Nonce;
+  var Gi: Ticket;
+
+
+
+  recv_1( I, R, SPIi, O, SA1, Gi, Ni );
+  send_2( R, I, SPIi, SPIr, SA1, g(r), Nr );
+
+
+  recv_!3( I, R, SPIi, SPIr, {I, {SPIi, O, SA1, Gi, Ni, Nr, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), I)}sk(I), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+  claim( R, Running, I,Gi,g(r),Ni,Nr );
+  send_!4( R, I, SPIi, SPIr, {R, MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(KDF(Ni,Nr,h(Gi,r),SPIi,SPIr), R)), SA2, TSi, TSr}KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+
+  claim( R, SKR, KDF(Ni,Nr,h(Gi,r),SPIi,SPIr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+  claim( R, Commit, I,Gi,g(r),Ni,Nr );
+ }
+}

gui/Protocols/IKE/jfki-core.spdl

@@ -0,0 +1,88 @@
+# 1 "jfki-core.cpp"
+# 1 "<command-line>"
+# 1 "jfki-core.cpp"
+# 15 "jfki-core.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 60 "common.h"
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i), Ni, Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r), Ni, Nr) );
+
+ }
+
+
+}
+# 16 "jfki-core.cpp" 2
+
+
+
+protocol jfki-core(I, R)
+{
+ role I {
+  fresh i, Ni: Nonce;
+  var Nr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ni, I, g(i) );
+  recv_2( R, I, Nr, Ni, R, Gr, {Nr, Ni, Gr, g(i), I}sk(R) );
+  send_3( I, R, Nr, Ni, {Nr, Ni, Gr, g(i), R}sk(I) );
+
+
+  claim( I, SKR, KDF(h(Gr,i), Ni, Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr: Nonce;
+  var Ni: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ni, I, Gi );
+  send_2( R, I, Nr, Ni, R, g(r), {Nr, Ni, g(r), Gi, I}sk(R) );
+  recv_3( I, R, Nr, Ni, {Nr, Ni, g(r), Gi, R}sk(I) );
+
+
+  claim( R, SKR, KDF(h(Gi,r), Ni, Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/jfki.spdl

@@ -0,0 +1,118 @@
+# 1 "jfki.cpp"
+# 1 "<command-line>"
+# 1 "jfki.cpp"
+# 15 "jfki.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 66 "common.h"
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i), H(Ni), Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r), H(Ni), Nr) );
+
+ }
+
+
+}
+# 16 "jfki.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, SAi, SAr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {I, SAi, {H(Ni), Nr, g(i), g(r), R, SAi}sk(I)}KDF(h(g(r),i), H(Ni), Nr) );
+  send_!O2( O, O, {I, SAi, {H(Ni), Nr, g(i), g(r), R, SAi}sk(I)}KDF(h(g(i),r), H(Ni), Nr) );
+
+
+  recv_!O3( O, O, {{H(Ni), Nr, g(i), g(r), I, SAi, SAr}sk(R), SAr}KDF(h(g(i),r), H(Ni), Nr) );
+  send_!O4( O, O, {{H(Ni), Nr, g(i), g(r), I, SAi, SAr}sk(R), SAr}KDF(h(g(r),i), H(Ni), Nr) );
+
+ }
+
+
+}
+
+
+
+protocol jfki(I, R)
+{
+ role I {
+  fresh i, Ni, SAi: Nonce;
+  var Nr, SAr: Nonce;
+  var Gr, TH: Ticket;
+
+  send_1( I, R, H(Ni), g(i) );
+  recv_2( R, I, H(Ni), Nr, Gr, R, {Gr}sk(R), TH );
+  send_!3( I, R, Ni, Nr, g(i), Gr, TH, {I, SAi, {H(Ni), Nr, g(i), Gr, R, SAi}sk(I)}KDF(h(Gr,i), H(Ni), Nr) );
+  recv_!4( R, I, {{H(Ni), Nr, g(i), Gr, I, SAi, SAr}sk(R), SAr}KDF(h(Gr,i), H(Ni), Nr) );
+
+
+  claim( I, SKR, KDF(h(Gr,i), H(Ni), Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr, SAr, HKr: Nonce;
+  var Ni, SAi: Nonce;
+  var Gi, HNi: Ticket;
+
+  recv_1( I, R, HNi, Gi );
+  send_2( R, I, HNi, Nr, g(r), R, {g(r)}sk(R), H(HKr, g(r), Nr, HNi) );
+
+  recv_!3( I, R, Ni, Nr, Gi, g(r), H(HKr, g(r), Nr, H(Ni)), {I, SAi, {H(Ni), Nr, Gi, g(r), R, SAi}sk(I)}KDF(h(Gi,r), H(Ni), Nr) );
+        send_!4( R, I, {{H(Ni), Nr, Gi, g(r), I, SAi, SAr}sk(R), SAr}KDF(h(Gi,r), H(Ni), Nr) );
+
+
+  claim( R, Secret, HKr );
+  claim( R, SKR, KDF(h(Gi,r), H(Ni), Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/jfkr-core.spdl

@@ -0,0 +1,112 @@
+# 1 "jfkr-core.cpp"
+# 1 "<command-line>"
+# 1 "jfkr-core.cpp"
+# 15 "jfkr-core.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 60 "common.h"
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i), Ni, Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r), Ni, Nr) );
+
+ }
+
+
+}
+# 16 "jfkr-core.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, H(KDF(h(g(i),r), Ni, Nr), Nr, Ni, R) );
+  send_!O2( O, O, H(KDF(h(g(r),i), Ni, Nr), Nr, Ni, R) );
+
+
+  recv_!O3( O, O, H(KDF(h(g(r),i), Ni, Nr), Nr, Ni, I) );
+  send_!O4( O, O, H(KDF(h(g(i),r), Ni, Nr), Nr, Ni, I) );
+
+ }
+
+
+}
+
+
+
+protocol jfkr-core(I, R)
+{
+ role I {
+  fresh i, Ni: Nonce;
+  var Nr, Gr: Ticket;
+
+  send_1( I, R, Ni, g(i) );
+  recv_!2( R, I, Nr, Ni, R, Gr, {Nr, Ni, Gr, g(i)}sk(R), H(KDF(h(Gr,i), Ni, Nr), Nr, Ni, R) );
+  send_!3( I, R, Nr, Ni, I, {Nr, Ni, Gr, g(i)}sk(I), H(KDF(h(Gr,i), Ni, Nr), Nr, Ni, I) );
+
+
+  claim( I, SKR, KDF(h(Gr,i), Ni, Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr: Nonce;
+  var Ni, Gi: Ticket;
+
+  recv_1( I, R, Ni, Gi );
+  send_!2( R, I, Nr, Ni, R, g(r), {Nr, Ni, g(r), Gi}sk(R), H(KDF(h(Gi,r), Ni, Nr), Nr, Ni, R) );
+  recv_!3( I, R, Nr, Ni, I, {Nr, Ni, g(r), Gi}sk(I), H(KDF(h(Gi,r), Ni, Nr), Nr, Ni, I) );
+
+
+  claim( R, SKR, KDF(h(Gi,r), Ni, Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/jfkr.spdl

@@ -0,0 +1,117 @@
+# 1 "jfkr.cpp"
+# 1 "<command-line>"
+# 1 "jfkr.cpp"
+# 15 "jfkr.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 66 "common.h"
+hashfunction H;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i), H(Ni), Nr) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r), H(Ni), Nr) );
+
+ }
+
+
+}
+# 16 "jfkr.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, SAi, SAr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {I, SAi, {H(Ni), Nr, g(i), g(r)}sk(I)}KDF(h(g(r),i), H(Ni), Nr) );
+  send_!O2( O, O, {I, SAi, {H(Ni), Nr, g(i), g(r)}sk(I)}KDF(h(g(i),r), H(Ni), Nr) );
+
+
+  recv_!O3( O, O, {R, SAr, {g(r), Nr, g(i), H(Ni)}sk(R)}KDF(h(g(i),r), H(Ni), Nr) );
+  send_!O4( O, O, {R, SAr, {g(r), Nr, g(i), H(Ni)}sk(R)}KDF(h(g(r),i), H(Ni), Nr) );
+
+ }
+
+
+}
+
+
+
+protocol jfkr(I, R)
+{
+ role I {
+  fresh i, Ni, SAi: Nonce;
+  var Nr, SAr: Nonce;
+  var Gr, TH: Ticket;
+
+  send_1( I, R, H(Ni), g(i) );
+  recv_2( R, I, H(Ni), Nr, Gr, TH );
+  send_!3( I, R, Ni, Nr, g(i), Gr, TH, {I, SAi, {H(Ni), Nr, g(i), Gr}sk(I)}KDF(h(Gr,i), H(Ni), Nr) );
+  recv_!4( R, I, {R, SAr, {Gr, Nr, g(i), H(Ni)}sk(R)}KDF(h(Gr,i), H(Ni), Nr) );
+
+
+  claim( I, SKR, KDF(h(Gr,i), H(Ni), Nr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr, SAr, HKr: Nonce;
+  var Ni, SAi: Nonce;
+  var Gi, HNi: Ticket;
+
+  recv_1( I, R, HNi, Gi );
+  send_2( R, I, HNi, Nr, g(r), H(HKr, g(r), Nr, HNi) );
+  recv_!3( I, R, Ni, Nr, Gi, g(r), H(HKr, g(r), Nr, H(Ni)), {I, SAi, {H(Ni), Nr, Gi, g(r)}sk(I)}KDF(h(Gi,r), H(Ni), Nr) );
+        send_!4( R, I, {R, SAr, {g(r), Nr, Gi, H(Ni)}sk(R)}KDF(h(Gi,r), H(Ni), Nr) );
+
+
+  claim( R, Secret, HKr );
+  claim( R, SKR, KDF(h(Gi,r), H(Ni), Nr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/oakley-a.spdl

@@ -0,0 +1,91 @@
+# 1 "oakley-a.cpp"
+# 1 "<command-line>"
+# 1 "oakley-a.cpp"
+# 18 "oakley-a.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 141 "common.h"
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 19 "oakley-a.cpp" 2
+
+
+
+usertype String;
+const list, algo: String;
+
+protocol oakley-a(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, Ci, g(i), list, I, R, Ni, {I, R, Ni, g(i), list}sk(I) );
+  recv_2( R, I, Cr, Ci, Gr, algo, R, I, Nr, Ni, {R, I, Nr, Ni, g(i), Gr, algo}sk(R) );
+  send_3( I, R, Ci, Cr, g(i), algo, I, R, Ni, Nr, {I, R, Ni, Nr, g(i), Gr, algo}sk(I) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, Gi, list, I, R, Ni, {I, R, Ni, Gi, list}sk(I) );
+  send_2( R, I, Cr, Ci, g(r), algo, R, I, Nr, Ni, {R, I, Nr, Ni, Gi, g(r), algo}sk(R) );
+  recv_3( I, R, Ci, Cr, Gi, algo, I, R, Ni, Nr, {I, R, Ni, Nr, Gi, g(r), algo}sk(I) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/oakley-alt.spdl

@@ -0,0 +1,94 @@
+# 1 "oakley-alt.cpp"
+# 1 "<command-line>"
+# 1 "oakley-alt.cpp"
+# 18 "oakley-alt.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 141 "common.h"
+  var Ci, Cr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 19 "oakley-alt.cpp" 2
+
+
+
+
+usertype String;
+const list, algo: String;
+
+protocol oakley-alt(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+
+
+  send_1( I, R, Ci, g(i), list, pk(R), {I, R, Ni}pk(R) );
+  recv_2( R, I, Cr, Ci, Gr, algo, {R, I, Nr}pk(I), prf(prf(Ni,Nr), R, I, Gr, g(i), algo) );
+  send_3( I, R, Ci, Cr, prf(prf(Ni,Nr), I, R, g(i), Gr, algo) );
+
+
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Ci, Gi, list, pk(R), {I, R, Ni}pk(R) );
+  send_2( R, I, Cr, Ci, g(r), algo, {R, I, Nr}pk(I), prf(prf(Ni,Nr), R, I, g(r), Gi, algo) );
+  recv_3( I, R, Ci, Cr, prf(prf(Ni,Nr), I, R, Gi, g(r), algo) );
+
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/oakley-c.spdl

@@ -0,0 +1,140 @@
+# 1 "oakley-c.cpp"
+# 1 "<command-line>"
+# 1 "oakley-c.cpp"
+# 18 "oakley-c.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 144 "common.h"
+  var Ci, Cr: Nonce;
+
+
+
+
+
+  recv_!SWAP1( SWAP, SWAP, KDF(Ni, Nr, h(g(r),i), Ci, Cr) );
+  send_!SWAP2( SWAP, SWAP, KDF(Ni, Nr, h(g(i),r), Ci, Cr) );
+
+ }
+
+
+}
+# 19 "oakley-c.cpp" 2
+
+
+
+
+
+
+
+usertype String;
+const OK, list, algo: String;
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r, Ni, Nr, Ci, Cr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {I, R, {Ni}pk(R)}prf(h(g(r),i)) );
+  send_!O2( O, O, {I, R, {Ni}pk(R)}prf(h(g(i),r)) );
+
+
+  recv_!O3( O, O, {{Nr, Ni}pk(I), R, I, prf(prf(Ni,Nr), R, I, g(r), g(i), algo)}prf(h(g(i),r)) );
+  send_!O4( O, O, {{Nr, Ni}pk(I), R, I, prf(prf(Ni,Nr), R, I, g(r), g(i), algo)}prf(h(g(r),i)) );
+
+
+  recv_!O5( O, O, {prf(prf(Ni,Nr), I, R, g(i), g(r), algo)}prf(h(g(r),i)) );
+  send_!O6( O, O, {prf(prf(Ni,Nr), I, R, g(i), g(r), algo)}prf(h(g(i),r)) );
+
+ }
+
+
+}
+
+
+protocol oakley-c(I, R)
+{
+ role I {
+  fresh i, Ni, Ci: Nonce;
+  var Nr, Cr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, OK );
+  recv_2( R, I, Cr );
+  send_3( I, R, Ci, Cr, g(i), list );
+  recv_4( R, I, Cr, Ci, Gr, algo );
+  send_!5( I, R, Ci, Cr, g(i), {I, R, {Ni}pk(R)}prf(h(Gr,i)) );
+  recv_!6( R, I, Cr, Ci, {{Nr, Ni}pk(I), R, I, prf(prf(Ni,Nr), R, I, Gr, g(i), algo)}prf(h(Gr,i)) );
+  send_!7( I, R, Ci, Cr, {prf(prf(Ni,Nr), I, R, g(i), Gr, algo)}prf(h(Gr,i)) );
+
+
+  claim( I, SKR, prf(h(Gr,i)) );
+  claim( I, SKR, KDF(Ni, Nr, h(Gr,i), Ci, Cr) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr, Cr: Nonce;
+  var Ni, Ci: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, OK );
+  send_2( R, I, Cr );
+  recv_3( I, R, Ci, Cr, Gi, list );
+  send_4( R, I, Cr, Ci, g(r), algo );
+  recv_!5( I, R, Ci, Cr, Gi, {I, R, {Ni}pk(R)}prf(h(Gi,r)) );
+  send_!6( R, I, Cr, Ci, {{Nr, Ni}pk(I), R, I, prf(prf(Ni,Nr), R, I, g(r), Gi, algo)}prf(h(Gi,r)) );
+  recv_!7( I, R, Ci, Cr, {prf(prf(Ni,Nr), I, R, Gi, g(r), algo)}prf(h(Gi,r)) );
+
+
+  claim( R, SKR, prf(h(Gi,r)) );
+
+  claim( R, SKR, KDF(Ni, Nr, h(Gi,r), Ci, Cr) );
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/skeme-basic.spdl

@@ -0,0 +1,87 @@
+# 1 "skeme-basic.cpp"
+# 1 "<command-line>"
+# 1 "skeme-basic.cpp"
+# 21 "skeme-basic.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i)) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r)) );
+
+ }
+
+
+}
+# 22 "skeme-basic.cpp" 2
+
+
+
+
+protocol skeme-basic(I, R)
+{
+ role I {
+  fresh i, Ni: Nonce;
+  var Nr: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, {I, Ni}pk(R), g(i) );
+  recv_2( R, I, {Nr}pk(I), Gr, prf(prf(Ni,Nr), g(i), Gr, R, I) );
+  send_3( I, R, prf(prf(Ni,Nr), Gr, g(i), I, R) );
+
+
+  claim( I, SKR, KDF(h(Gr,i)) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r, Nr: Nonce;
+  var Ni: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, {I, Ni}pk(R), Gi );
+  send_2( R, I, {Nr}pk(I), g(r), prf(prf(Ni,Nr), Gi, g(r), R, I) );
+  recv_3( I, R, prf(prf(Ni,Nr), g(r), Gi, I, R) );
+
+
+  claim( R, SKR, KDF(h(Gi,r)) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/skeme-psk.spdl

@@ -0,0 +1,109 @@
+# 1 "skeme-psk.cpp"
+# 1 "<command-line>"
+# 1 "skeme-psk.cpp"
+# 20 "skeme-psk.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i)) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r)) );
+
+ }
+
+
+}
+# 21 "skeme-psk.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(k(R,I), g(i), g(r), R, I) );
+  send_!O2( O, O, prf(k(I,R), g(i), g(r), R, I) );
+
+
+  recv_!O3( O, O, prf(k(I,R), g(r), g(i), I, R) );
+  send_!O4( O, O, prf(k(R,I), g(r), g(i), I, R) );
+
+ }
+
+
+}
+
+
+protocol skeme-psk(I, R)
+{
+ role I {
+  fresh i: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, g(i) );
+  recv_!2( R, I, Gr, prf(k(I,R), g(i), Gr, R, I) );
+  send_!3( I, R, prf(k(I,R), Gr, g(i), I, R) );
+
+
+  claim( I, SKR, KDF(h(Gr,i)) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Gi );
+  send_!2( R, I, g(r), prf(k(R,I), Gi, g(r), R, I) );
+  recv_!3( I, R, prf(k(R,I), g(r), Gi, I, R) );
+
+
+  claim( R, SKR, KDF(h(Gi,r)) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/skeme-rekey.spdl

@@ -0,0 +1,111 @@
+# 1 "skeme-rekey.cpp"
+# 1 "<command-line>"
+# 1 "skeme-rekey.cpp"
+# 19 "skeme-rekey.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 97 "common.h"
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 147 "common.h"
+  var I, R: Agent;
+
+
+  recv_!SWAP1( SWAP, SWAP, KDF(k(I,R),prf(k(I,R), Ni, Nr, R, I)) );
+  send_!SWAP2( SWAP, SWAP, KDF(k(R,I),prf(k(R,I), Ni, Nr, R, I)) );
+
+ }
+
+
+}
+# 20 "skeme-rekey.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var Ni, Nr: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, prf(k(R,I), Ni, Nr, R, I) );
+  send_!O2( O, O, prf(k(I,R), Ni, Nr, R, I) );
+
+
+  recv_!O3( O, O, prf(k(I,R), Nr, Ni, I, R) );
+  send_!O4( O, O, prf(k(R,I), Nr, Ni, I, R) );
+
+ }
+
+
+}
+
+protocol skeme-rekey(I, R)
+{
+ role I {
+  fresh Ni: Nonce;
+  var Nr: Nonce;
+
+  send_1( I, R, Ni );
+  recv_!2( R, I, Nr, prf(k(I,R), Ni, Nr, R, I) );
+  send_!3( I, R, prf(k(I,R), Nr, Ni, I, R) );
+
+
+  claim( I, SKR, KDF(k(I,R),prf(k(I,R), Ni, Nr, R, I)) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh Nr: Nonce;
+  var Ni: Nonce;
+
+  recv_1( I, R, Ni );
+  send_!2( R, I, Nr, prf(k(I,R), Ni, Nr, R, I) );
+  recv_!3( I, R, prf(k(I,R), Nr, Ni, I, R) );
+
+
+  claim( R, SKR, KDF(k(R,I),prf(k(R,I), Ni, Nr, R, I)) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/sts-mac.spdl

@@ -0,0 +1,112 @@
+# 1 "sts-mac.cpp"
+# 1 "<command-line>"
+# 1 "sts-mac.cpp"
+# 16 "sts-mac.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 94 "common.h"
+hashfunction MAC;
+
+
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i)) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r)) );
+
+ }
+
+
+}
+# 17 "sts-mac.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r: Nonce;
+
+
+  recv_!O1( O, O, MAC(h(g(i),r), g(r), g(i)) );
+  send_!O2( O, O, MAC(h(g(r),i), g(r), g(i)) );
+
+
+  recv_!O3( O, O, MAC(h(g(r),i), g(i), g(r)) );
+  send_!O4( O, O, MAC(h(g(i),r), g(i), g(r)) );
+
+ }
+
+
+}
+
+
+
+protocol sts-mac(I, R)
+{
+ role I {
+  fresh i: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, g(i) );
+  recv_!2( R, I, Gr, {Gr, g(i)}sk(R), MAC(h(Gr,i), Gr, g(i)) );
+  send_!3( I, R, {g(i), Gr}sk(I), MAC(h(Gr,i), g(i), Gr) );
+
+
+  claim( I, SKR, KDF(h(Gr,i)) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Gi );
+  send_!2( R, I, Gi, {g(r), Gi}sk(R), MAC(h(Gi,r), g(r), Gi) );
+  recv_!3( I, R, {Gi, g(r)}sk(I), MAC(h(Gi,r), Gi, g(r)) );
+
+
+  claim( R, SKR, KDF(h(Gi,r)) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/sts-main.spdl

@@ -0,0 +1,114 @@
+# 1 "sts-main.cpp"
+# 1 "<command-line>"
+# 1 "sts-main.cpp"
+# 15 "sts-main.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 94 "common.h"
+hashfunction MAC;
+
+
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i)) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r)) );
+
+ }
+
+
+}
+# 16 "sts-main.cpp" 2
+
+
+
+
+
+
+
+protocol @executability(O) {
+
+
+ role O {
+  var i, r: Nonce;
+  var I, R: Agent;
+
+
+  recv_!O1( O, O, {{g(r), g(i)}sk(R)}KDF(h(g(i),r)) );
+  send_!O2( O, O, {{g(r), g(i)}sk(R)}KDF(h(g(r),i)) );
+
+
+  recv_!O3( O, O, {{g(i), g(r)}sk(I)}KDF(h(g(r),i)) );
+  send_!O4( O, O, {{g(i), g(r)}sk(I)}KDF(h(g(i),r)) );
+
+ }
+
+
+}
+
+
+
+
+protocol sts-main(I, R)
+{
+ role I {
+  fresh i: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, g(i) );
+  recv_!2( R, I, Gr, {{Gr, g(i)}sk(R)}KDF(h(Gr,i)) );
+  send_!3( I, R, {{g(i), Gr}sk(I)}KDF(h(Gr,i)) );
+
+
+  claim( I, SKR, KDF(h(Gr,i)) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Gi );
+  send_!2( R, I, g(r), {{g(r), Gi}sk(R)}KDF(h(Gi,r)) );
+  recv_!3( I, R, {{Gi, g(r)}sk(I)}KDF(h(Gi,r)) );
+
+
+  claim( R, SKR, KDF(h(Gi,r)) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}

gui/Protocols/IKE/sts-modified.spdl

@@ -0,0 +1,88 @@
+# 1 "sts-modified.cpp"
+# 1 "<command-line>"
+# 1 "sts-modified.cpp"
+# 17 "sts-modified.cpp"
+# 1 "common.h" 1
+
+
+
+
+ hashfunction prf, KDF;
+
+
+
+
+
+
+const g, h: Function;
+# 94 "common.h"
+hashfunction MAC;
+
+
+protocol @oracle (DH, SWAP) {
+
+
+
+
+
+
+
+ role DH {
+  var i, r: Nonce;
+
+  recv_!DH1( DH, DH, h(g(r),i) );
+  send_!DH2( DH, DH, h(g(i),r) );
+ }
+
+
+
+
+ role SWAP {
+  var i, r, Ni, Nr: Nonce;
+# 150 "common.h"
+  recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i)) );
+  send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r)) );
+
+ }
+
+
+}
+# 18 "sts-modified.cpp" 2
+
+
+
+
+protocol sts-modified(I, R)
+{
+ role I {
+  fresh i: Nonce;
+  var Gr: Ticket;
+
+  send_1( I, R, g(i) );
+  recv_2( R, I, Gr, {Gr, g(i), I}sk(R) );
+  send_3( I, R, {g(i), Gr, R}sk(I) );
+
+
+  claim( I, SKR, KDF(h(Gr,i)) );
+
+  claim( I, Alive );
+  claim( I, Weakagree );
+
+ }
+
+ role R {
+  fresh r: Nonce;
+  var Gi: Ticket;
+
+  recv_1( I, R, Gi );
+  send_2( R, I, g(r), {g(r), Gi, I}sk(R) );
+  recv_3( I, R, {Gi, g(r), R}sk(I) );
+
+
+  claim( R, SKR, KDF(h(Gi,r)) );
+
+  claim( R, Alive );
+  claim( R, Weakagree );
+
+ }
+}