From 03f49d3b29ebb8f63e52b2b7c503362fee3d9235 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 15 Nov 2012 11:48:46 +0100 Subject: [PATCH] Added IKE .spdl files (auto-generated from the .cpp files) for reference. --- gui/Protocols/IKE/ikev1-pk-a1.spdl | 129 ++++++++++++++ gui/Protocols/IKE/ikev1-pk-a12.spdl | 128 ++++++++++++++ gui/Protocols/IKE/ikev1-pk-a2.spdl | 129 ++++++++++++++ gui/Protocols/IKE/ikev1-pk-a22.spdl | 128 ++++++++++++++ gui/Protocols/IKE/ikev1-pk-m.spdl | 136 +++++++++++++++ gui/Protocols/IKE/ikev1-pk-m2.spdl | 135 ++++++++++++++ gui/Protocols/IKE/ikev1-pk2-a.spdl | 129 ++++++++++++++ gui/Protocols/IKE/ikev1-pk2-a2.spdl | 128 ++++++++++++++ gui/Protocols/IKE/ikev1-pk2-m.spdl | 136 +++++++++++++++ gui/Protocols/IKE/ikev1-pk2-m2.spdl | 136 +++++++++++++++ gui/Protocols/IKE/ikev1-psk-a.spdl | 125 +++++++++++++ gui/Protocols/IKE/ikev1-psk-m-perlman.spdl | 131 ++++++++++++++ gui/Protocols/IKE/ikev1-psk-m.spdl | 130 ++++++++++++++ gui/Protocols/IKE/ikev1-quick-noid.spdl | 124 +++++++++++++ gui/Protocols/IKE/ikev1-quick-nopfs.spdl | 118 +++++++++++++ gui/Protocols/IKE/ikev1-quick.spdl | 91 ++++++++++ gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl | 130 ++++++++++++++ gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl | 130 ++++++++++++++ gui/Protocols/IKE/ikev1-sig-a1.spdl | 130 ++++++++++++++ gui/Protocols/IKE/ikev1-sig-a2.spdl | 130 ++++++++++++++ gui/Protocols/IKE/ikev1-sig-m-perlman.spdl | 133 ++++++++++++++ gui/Protocols/IKE/ikev1-sig-m.spdl | 134 ++++++++++++++ gui/Protocols/IKE/ikev2-child-nopfs.spdl | 112 ++++++++++++ gui/Protocols/IKE/ikev2-child.spdl | 121 +++++++++++++ gui/Protocols/IKE/ikev2-eap.spdl | 160 +++++++++++++++++ gui/Protocols/IKE/ikev2-eap2.spdl | 160 +++++++++++++++++ gui/Protocols/IKE/ikev2-mac.spdl | 133 ++++++++++++++ gui/Protocols/IKE/ikev2-mac2.spdl | 133 ++++++++++++++ gui/Protocols/IKE/ikev2-mactosig.spdl | 132 ++++++++++++++ gui/Protocols/IKE/ikev2-mactosig2.spdl | 131 ++++++++++++++ .../IKE/ikev2-sig-child-composed.spdl | 165 ++++++++++++++++++ gui/Protocols/IKE/ikev2-sig-child.spdl | 165 ++++++++++++++++++ .../IKE/ikev2-sig-child2-composed.spdl | 165 ++++++++++++++++++ gui/Protocols/IKE/ikev2-sig-child2.spdl | 165 ++++++++++++++++++ gui/Protocols/IKE/ikev2-sig.spdl | 132 ++++++++++++++ gui/Protocols/IKE/ikev2-sig2.spdl | 132 ++++++++++++++ gui/Protocols/IKE/ikev2-sigtomac.spdl | 132 ++++++++++++++ gui/Protocols/IKE/ikev2-sigtomac2.spdl | 132 ++++++++++++++ gui/Protocols/IKE/jfki-core.spdl | 88 ++++++++++ gui/Protocols/IKE/jfki.spdl | 118 +++++++++++++ gui/Protocols/IKE/jfkr-core.spdl | 112 ++++++++++++ gui/Protocols/IKE/jfkr.spdl | 117 +++++++++++++ gui/Protocols/IKE/oakley-a.spdl | 91 ++++++++++ gui/Protocols/IKE/oakley-alt.spdl | 94 ++++++++++ gui/Protocols/IKE/oakley-c.spdl | 140 +++++++++++++++ gui/Protocols/IKE/skeme-basic.spdl | 87 +++++++++ gui/Protocols/IKE/skeme-psk.spdl | 109 ++++++++++++ gui/Protocols/IKE/skeme-rekey.spdl | 111 ++++++++++++ gui/Protocols/IKE/sts-mac.spdl | 112 ++++++++++++ gui/Protocols/IKE/sts-main.spdl | 114 ++++++++++++ gui/Protocols/IKE/sts-modified.spdl | 88 ++++++++++ 51 files changed, 6471 insertions(+) create mode 100644 gui/Protocols/IKE/ikev1-pk-a1.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk-a12.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk-a2.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk-a22.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk-m.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk-m2.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk2-a.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk2-a2.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk2-m.spdl create mode 100644 gui/Protocols/IKE/ikev1-pk2-m2.spdl create mode 100644 gui/Protocols/IKE/ikev1-psk-a.spdl create mode 100644 gui/Protocols/IKE/ikev1-psk-m-perlman.spdl create mode 100644 gui/Protocols/IKE/ikev1-psk-m.spdl create mode 100644 gui/Protocols/IKE/ikev1-quick-noid.spdl create mode 100644 gui/Protocols/IKE/ikev1-quick-nopfs.spdl create mode 100644 gui/Protocols/IKE/ikev1-quick.spdl create mode 100644 gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl create mode 100644 gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl create mode 100644 gui/Protocols/IKE/ikev1-sig-a1.spdl create mode 100644 gui/Protocols/IKE/ikev1-sig-a2.spdl create mode 100644 gui/Protocols/IKE/ikev1-sig-m-perlman.spdl create mode 100644 gui/Protocols/IKE/ikev1-sig-m.spdl create mode 100644 gui/Protocols/IKE/ikev2-child-nopfs.spdl create mode 100644 gui/Protocols/IKE/ikev2-child.spdl create mode 100644 gui/Protocols/IKE/ikev2-eap.spdl create mode 100644 gui/Protocols/IKE/ikev2-eap2.spdl create mode 100644 gui/Protocols/IKE/ikev2-mac.spdl create mode 100644 gui/Protocols/IKE/ikev2-mac2.spdl create mode 100644 gui/Protocols/IKE/ikev2-mactosig.spdl create mode 100644 gui/Protocols/IKE/ikev2-mactosig2.spdl create mode 100644 gui/Protocols/IKE/ikev2-sig-child-composed.spdl create mode 100644 gui/Protocols/IKE/ikev2-sig-child.spdl create mode 100644 gui/Protocols/IKE/ikev2-sig-child2-composed.spdl create mode 100644 gui/Protocols/IKE/ikev2-sig-child2.spdl create mode 100644 gui/Protocols/IKE/ikev2-sig.spdl create mode 100644 gui/Protocols/IKE/ikev2-sig2.spdl create mode 100644 gui/Protocols/IKE/ikev2-sigtomac.spdl create mode 100644 gui/Protocols/IKE/ikev2-sigtomac2.spdl create mode 100644 gui/Protocols/IKE/jfki-core.spdl create mode 100644 gui/Protocols/IKE/jfki.spdl create mode 100644 gui/Protocols/IKE/jfkr-core.spdl create mode 100644 gui/Protocols/IKE/jfkr.spdl create mode 100644 gui/Protocols/IKE/oakley-a.spdl create mode 100644 gui/Protocols/IKE/oakley-alt.spdl create mode 100644 gui/Protocols/IKE/oakley-c.spdl create mode 100644 gui/Protocols/IKE/skeme-basic.spdl create mode 100644 gui/Protocols/IKE/skeme-psk.spdl create mode 100644 gui/Protocols/IKE/skeme-rekey.spdl create mode 100644 gui/Protocols/IKE/sts-mac.spdl create mode 100644 gui/Protocols/IKE/sts-main.spdl create mode 100644 gui/Protocols/IKE/sts-modified.spdl diff --git a/gui/Protocols/IKE/ikev1-pk-a1.spdl b/gui/Protocols/IKE/ikev1-pk-a1.spdl new file mode 100644 index 0000000..7439f2f --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a1.spdl @@ -0,0 +1,129 @@ +# 1 "ikev1-pk-a1.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk-a12.spdl b/gui/Protocols/IKE/ikev1-pk-a12.spdl new file mode 100644 index 0000000..f55e2c2 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a12.spdl @@ -0,0 +1,128 @@ +# 1 "ikev1-pk-a12.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk-a2.spdl b/gui/Protocols/IKE/ikev1-pk-a2.spdl new file mode 100644 index 0000000..c81760a --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a2.spdl @@ -0,0 +1,129 @@ +# 1 "ikev1-pk-a2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk-a22.spdl b/gui/Protocols/IKE/ikev1-pk-a22.spdl new file mode 100644 index 0000000..b8e6853 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a22.spdl @@ -0,0 +1,128 @@ +# 1 "ikev1-pk-a22.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk-m.spdl b/gui/Protocols/IKE/ikev1-pk-m.spdl new file mode 100644 index 0000000..c121d25 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-m.spdl @@ -0,0 +1,136 @@ +# 1 "ikev1-pk-m.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk-m2.spdl b/gui/Protocols/IKE/ikev1-pk-m2.spdl new file mode 100644 index 0000000..f21988b --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-m2.spdl @@ -0,0 +1,135 @@ +# 1 "ikev1-pk-m2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk2-a.spdl b/gui/Protocols/IKE/ikev1-pk2-a.spdl new file mode 100644 index 0000000..2836575 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-a.spdl @@ -0,0 +1,129 @@ +# 1 "ikev1-pk2-a.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk2-a2.spdl b/gui/Protocols/IKE/ikev1-pk2-a2.spdl new file mode 100644 index 0000000..f916068 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-a2.spdl @@ -0,0 +1,128 @@ +# 1 "ikev1-pk2-a2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk2-m.spdl b/gui/Protocols/IKE/ikev1-pk2-m.spdl new file mode 100644 index 0000000..84f0459 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-m.spdl @@ -0,0 +1,136 @@ +# 1 "ikev1-pk2-m.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-pk2-m2.spdl b/gui/Protocols/IKE/ikev1-pk2-m2.spdl new file mode 100644 index 0000000..d87dbb1 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-m2.spdl @@ -0,0 +1,136 @@ +# 1 "ikev1-pk2-m2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-psk-a.spdl b/gui/Protocols/IKE/ikev1-psk-a.spdl new file mode 100644 index 0000000..3a66a36 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-psk-a.spdl @@ -0,0 +1,125 @@ +# 1 "ikev1-psk-a.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-psk-m-perlman.spdl b/gui/Protocols/IKE/ikev1-psk-m-perlman.spdl new file mode 100644 index 0000000..68c9213 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-psk-m-perlman.spdl @@ -0,0 +1,131 @@ +# 1 "ikev1-psk-m-perlman.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-psk-m.spdl b/gui/Protocols/IKE/ikev1-psk-m.spdl new file mode 100644 index 0000000..b98435f --- /dev/null +++ b/gui/Protocols/IKE/ikev1-psk-m.spdl @@ -0,0 +1,130 @@ +# 1 "ikev1-psk-m.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-quick-noid.spdl b/gui/Protocols/IKE/ikev1-quick-noid.spdl new file mode 100644 index 0000000..96246de --- /dev/null +++ b/gui/Protocols/IKE/ikev1-quick-noid.spdl @@ -0,0 +1,124 @@ +# 1 "ikev1-quick-noid.cpp" +# 1 "" +# 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) ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-quick-nopfs.spdl b/gui/Protocols/IKE/ikev1-quick-nopfs.spdl new file mode 100644 index 0000000..8f7d3a2 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-quick-nopfs.spdl @@ -0,0 +1,118 @@ +# 1 "ikev1-quick-nopfs.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-quick.spdl b/gui/Protocols/IKE/ikev1-quick.spdl new file mode 100644 index 0000000..5ace037 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-quick.spdl @@ -0,0 +1,91 @@ +# 1 "ikev1-quick.cpp" +# 1 "" +# 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) ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl b/gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl new file mode 100644 index 0000000..ff8babf --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl @@ -0,0 +1,130 @@ +# 1 "ikev1-sig-a-perlman1.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl b/gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl new file mode 100644 index 0000000..cb520cc --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl @@ -0,0 +1,130 @@ +# 1 "ikev1-sig-a-perlman2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-sig-a1.spdl b/gui/Protocols/IKE/ikev1-sig-a1.spdl new file mode 100644 index 0000000..936776e --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a1.spdl @@ -0,0 +1,130 @@ +# 1 "ikev1-sig-a1.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-sig-a2.spdl b/gui/Protocols/IKE/ikev1-sig-a2.spdl new file mode 100644 index 0000000..ea26372 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a2.spdl @@ -0,0 +1,130 @@ +# 1 "ikev1-sig-a2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-sig-m-perlman.spdl b/gui/Protocols/IKE/ikev1-sig-m-perlman.spdl new file mode 100644 index 0000000..e97ba4c --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-m-perlman.spdl @@ -0,0 +1,133 @@ +# 1 "ikev1-sig-m-perlman.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev1-sig-m.spdl b/gui/Protocols/IKE/ikev1-sig-m.spdl new file mode 100644 index 0000000..121f5d1 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-m.spdl @@ -0,0 +1,134 @@ +# 1 "ikev1-sig-m.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev2-child-nopfs.spdl b/gui/Protocols/IKE/ikev2-child-nopfs.spdl new file mode 100644 index 0000000..342bed2 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-child-nopfs.spdl @@ -0,0 +1,112 @@ +# 1 "ikev2-child-nopfs.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-child.spdl b/gui/Protocols/IKE/ikev2-child.spdl new file mode 100644 index 0000000..8b3d408 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-child.spdl @@ -0,0 +1,121 @@ +# 1 "ikev2-child.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-eap.spdl b/gui/Protocols/IKE/ikev2-eap.spdl new file mode 100644 index 0000000..d2c3932 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-eap.spdl @@ -0,0 +1,160 @@ +# 1 "ikev2-eap.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev2-eap2.spdl b/gui/Protocols/IKE/ikev2-eap2.spdl new file mode 100644 index 0000000..b1bfcbd --- /dev/null +++ b/gui/Protocols/IKE/ikev2-eap2.spdl @@ -0,0 +1,160 @@ +# 1 "ikev2-eap2.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/ikev2-mac.spdl b/gui/Protocols/IKE/ikev2-mac.spdl new file mode 100644 index 0000000..264d16a --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mac.spdl @@ -0,0 +1,133 @@ +# 1 "ikev2-mac.cpp" +# 1 "" +# 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); + } +} diff --git a/gui/Protocols/IKE/ikev2-mac2.spdl b/gui/Protocols/IKE/ikev2-mac2.spdl new file mode 100644 index 0000000..5d3acc3 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mac2.spdl @@ -0,0 +1,133 @@ +# 1 "ikev2-mac2.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-mactosig.spdl b/gui/Protocols/IKE/ikev2-mactosig.spdl new file mode 100644 index 0000000..895724f --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mactosig.spdl @@ -0,0 +1,132 @@ +# 1 "ikev2-mactosig.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-mactosig2.spdl b/gui/Protocols/IKE/ikev2-mactosig2.spdl new file mode 100644 index 0000000..c434d7e --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mactosig2.spdl @@ -0,0 +1,131 @@ +# 1 "ikev2-mactosig2.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child-composed.spdl b/gui/Protocols/IKE/ikev2-sig-child-composed.spdl new file mode 100644 index 0000000..b3c4630 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child-composed.spdl @@ -0,0 +1,165 @@ +# 1 "ikev2-sig-child-composed.cpp" +# 1 "" +# 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) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child.spdl b/gui/Protocols/IKE/ikev2-sig-child.spdl new file mode 100644 index 0000000..54b7342 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child.spdl @@ -0,0 +1,165 @@ +# 1 "ikev2-sig-child.cpp" +# 1 "" +# 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) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child2-composed.spdl b/gui/Protocols/IKE/ikev2-sig-child2-composed.spdl new file mode 100644 index 0000000..d87dfb6 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child2-composed.spdl @@ -0,0 +1,165 @@ +# 1 "ikev2-sig-child2-composed.cpp" +# 1 "" +# 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) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child2.spdl b/gui/Protocols/IKE/ikev2-sig-child2.spdl new file mode 100644 index 0000000..3694664 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child2.spdl @@ -0,0 +1,165 @@ +# 1 "ikev2-sig-child2.cpp" +# 1 "" +# 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) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig.spdl b/gui/Protocols/IKE/ikev2-sig.spdl new file mode 100644 index 0000000..261d732 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig.spdl @@ -0,0 +1,132 @@ +# 1 "ikev2-sig.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig2.spdl b/gui/Protocols/IKE/ikev2-sig2.spdl new file mode 100644 index 0000000..309c9c5 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig2.spdl @@ -0,0 +1,132 @@ +# 1 "ikev2-sig2.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sigtomac.spdl b/gui/Protocols/IKE/ikev2-sigtomac.spdl new file mode 100644 index 0000000..eea159b --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sigtomac.spdl @@ -0,0 +1,132 @@ +# 1 "ikev2-sigtomac.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sigtomac2.spdl b/gui/Protocols/IKE/ikev2-sigtomac2.spdl new file mode 100644 index 0000000..79ef0f4 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sigtomac2.spdl @@ -0,0 +1,132 @@ +# 1 "ikev2-sigtomac2.cpp" +# 1 "" +# 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 ); + } +} diff --git a/gui/Protocols/IKE/jfki-core.spdl b/gui/Protocols/IKE/jfki-core.spdl new file mode 100644 index 0000000..599786c --- /dev/null +++ b/gui/Protocols/IKE/jfki-core.spdl @@ -0,0 +1,88 @@ +# 1 "jfki-core.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/jfki.spdl b/gui/Protocols/IKE/jfki.spdl new file mode 100644 index 0000000..02c916f --- /dev/null +++ b/gui/Protocols/IKE/jfki.spdl @@ -0,0 +1,118 @@ +# 1 "jfki.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/jfkr-core.spdl b/gui/Protocols/IKE/jfkr-core.spdl new file mode 100644 index 0000000..9668081 --- /dev/null +++ b/gui/Protocols/IKE/jfkr-core.spdl @@ -0,0 +1,112 @@ +# 1 "jfkr-core.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/jfkr.spdl b/gui/Protocols/IKE/jfkr.spdl new file mode 100644 index 0000000..0a3fc64 --- /dev/null +++ b/gui/Protocols/IKE/jfkr.spdl @@ -0,0 +1,117 @@ +# 1 "jfkr.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/oakley-a.spdl b/gui/Protocols/IKE/oakley-a.spdl new file mode 100644 index 0000000..597f7c2 --- /dev/null +++ b/gui/Protocols/IKE/oakley-a.spdl @@ -0,0 +1,91 @@ +# 1 "oakley-a.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/oakley-alt.spdl b/gui/Protocols/IKE/oakley-alt.spdl new file mode 100644 index 0000000..8fe6c65 --- /dev/null +++ b/gui/Protocols/IKE/oakley-alt.spdl @@ -0,0 +1,94 @@ +# 1 "oakley-alt.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/oakley-c.spdl b/gui/Protocols/IKE/oakley-c.spdl new file mode 100644 index 0000000..fba780d --- /dev/null +++ b/gui/Protocols/IKE/oakley-c.spdl @@ -0,0 +1,140 @@ +# 1 "oakley-c.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/skeme-basic.spdl b/gui/Protocols/IKE/skeme-basic.spdl new file mode 100644 index 0000000..8ff3ecd --- /dev/null +++ b/gui/Protocols/IKE/skeme-basic.spdl @@ -0,0 +1,87 @@ +# 1 "skeme-basic.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/skeme-psk.spdl b/gui/Protocols/IKE/skeme-psk.spdl new file mode 100644 index 0000000..70d33bc --- /dev/null +++ b/gui/Protocols/IKE/skeme-psk.spdl @@ -0,0 +1,109 @@ +# 1 "skeme-psk.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/skeme-rekey.spdl b/gui/Protocols/IKE/skeme-rekey.spdl new file mode 100644 index 0000000..dcc709c --- /dev/null +++ b/gui/Protocols/IKE/skeme-rekey.spdl @@ -0,0 +1,111 @@ +# 1 "skeme-rekey.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/sts-mac.spdl b/gui/Protocols/IKE/sts-mac.spdl new file mode 100644 index 0000000..fdc1a11 --- /dev/null +++ b/gui/Protocols/IKE/sts-mac.spdl @@ -0,0 +1,112 @@ +# 1 "sts-mac.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/sts-main.spdl b/gui/Protocols/IKE/sts-main.spdl new file mode 100644 index 0000000..17951b1 --- /dev/null +++ b/gui/Protocols/IKE/sts-main.spdl @@ -0,0 +1,114 @@ +# 1 "sts-main.cpp" +# 1 "" +# 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 ); + + } +} diff --git a/gui/Protocols/IKE/sts-modified.spdl b/gui/Protocols/IKE/sts-modified.spdl new file mode 100644 index 0000000..f9cafa1 --- /dev/null +++ b/gui/Protocols/IKE/sts-modified.spdl @@ -0,0 +1,88 @@ +# 1 "sts-modified.cpp" +# 1 "" +# 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 ); + + } +}