From 34d7cba29390ec7640e5d2ade45a603dbb4274b9 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 15 Nov 2012 11:48:14 +0100 Subject: [PATCH] Added IKE base models. Modelers: Adrian Kyburz and Cas Cremers --- gui/Protocols/IKE/Makefile | 11 + gui/Protocols/IKE/common.h | 157 ++++ gui/Protocols/IKE/ikev1-pk-a1.cpp | 96 +++ gui/Protocols/IKE/ikev1-pk-a12.cpp | 95 +++ gui/Protocols/IKE/ikev1-pk-a2.cpp | 97 +++ gui/Protocols/IKE/ikev1-pk-a22.cpp | 95 +++ gui/Protocols/IKE/ikev1-pk-m.cpp | 103 +++ gui/Protocols/IKE/ikev1-pk-m2.cpp | 102 +++ gui/Protocols/IKE/ikev1-pk2-a.cpp | 97 +++ gui/Protocols/IKE/ikev1-pk2-a2.cpp | 97 +++ gui/Protocols/IKE/ikev1-pk2-m.cpp | 104 +++ gui/Protocols/IKE/ikev1-pk2-m2.cpp | 106 +++ gui/Protocols/IKE/ikev1-psk-a.cpp | 94 ++ gui/Protocols/IKE/ikev1-psk-m-perlman.cpp | 101 +++ gui/Protocols/IKE/ikev1-psk-m.cpp | 100 +++ gui/Protocols/IKE/ikev1-quick-noid.cpp | 102 +++ gui/Protocols/IKE/ikev1-quick-nopfs.cpp | 96 +++ gui/Protocols/IKE/ikev1-quick.cpp | 70 ++ gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp | 99 +++ gui/Protocols/IKE/ikev1-sig-a-perlman2.cpp | 99 +++ gui/Protocols/IKE/ikev1-sig-a1.cpp | 98 +++ gui/Protocols/IKE/ikev1-sig-a2.cpp | 99 +++ gui/Protocols/IKE/ikev1-sig-m-perlman.cpp | 100 +++ gui/Protocols/IKE/ikev1-sig-m.cpp | 102 +++ gui/Protocols/IKE/ikev2-child-nopfs.cpp | 78 ++ gui/Protocols/IKE/ikev2-child.cpp | 87 ++ gui/Protocols/IKE/ikev2-eap.cpp | 131 +++ gui/Protocols/IKE/ikev2-eap2.cpp | 138 +++ gui/Protocols/IKE/ikev2-mac.cpp | 104 +++ gui/Protocols/IKE/ikev2-mac2.cpp | 104 +++ gui/Protocols/IKE/ikev2-mactosig.cpp | 104 +++ gui/Protocols/IKE/ikev2-mactosig2.cpp | 103 +++ .../IKE/ikev2-sig-child-composed.cpp | 138 +++ gui/Protocols/IKE/ikev2-sig-child.cpp | 138 +++ .../IKE/ikev2-sig-child2-composed.cpp | 138 +++ gui/Protocols/IKE/ikev2-sig-child2.cpp | 138 +++ gui/Protocols/IKE/ikev2-sig.cpp | 103 +++ gui/Protocols/IKE/ikev2-sig2.cpp | 103 +++ gui/Protocols/IKE/ikev2-sigtomac.cpp | 104 +++ gui/Protocols/IKE/ikev2-sigtomac2.cpp | 104 +++ gui/Protocols/IKE/jfki-core.cpp | 54 ++ gui/Protocols/IKE/jfki.cpp | 84 ++ gui/Protocols/IKE/jfkr-core.cpp | 78 ++ gui/Protocols/IKE/jfkr.cpp | 83 ++ gui/Protocols/IKE/make-mpa.py | 63 ++ gui/Protocols/IKE/mpa/README.txt | 6 + gui/Protocols/IKE/oakley-a.cpp | 60 ++ gui/Protocols/IKE/oakley-alt.cpp | 63 ++ gui/Protocols/IKE/oakley-c.cpp | 105 +++ gui/Protocols/IKE/pp.sh | 21 + gui/Protocols/IKE/scanner.py | 800 ++++++++++++++++++ gui/Protocols/IKE/skeme-basic.cpp | 61 ++ gui/Protocols/IKE/skeme-psk.cpp | 82 ++ gui/Protocols/IKE/skeme-rekey.cpp | 80 ++ gui/Protocols/IKE/sts-mac.cpp | 78 ++ gui/Protocols/IKE/sts-main.cpp | 79 ++ gui/Protocols/IKE/sts-modified.cpp | 55 ++ gui/Protocols/IKE/verify.sh | 149 ++++ gui/Protocols/IKE/verify_all.sh | 20 + 59 files changed, 6156 insertions(+) create mode 100644 gui/Protocols/IKE/Makefile create mode 100644 gui/Protocols/IKE/common.h create mode 100644 gui/Protocols/IKE/ikev1-pk-a1.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk-a12.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk-a2.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk-a22.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk-m.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk-m2.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk2-a.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk2-a2.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk2-m.cpp create mode 100644 gui/Protocols/IKE/ikev1-pk2-m2.cpp create mode 100644 gui/Protocols/IKE/ikev1-psk-a.cpp create mode 100644 gui/Protocols/IKE/ikev1-psk-m-perlman.cpp create mode 100644 gui/Protocols/IKE/ikev1-psk-m.cpp create mode 100644 gui/Protocols/IKE/ikev1-quick-noid.cpp create mode 100644 gui/Protocols/IKE/ikev1-quick-nopfs.cpp create mode 100644 gui/Protocols/IKE/ikev1-quick.cpp create mode 100644 gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp create mode 100644 gui/Protocols/IKE/ikev1-sig-a-perlman2.cpp create mode 100644 gui/Protocols/IKE/ikev1-sig-a1.cpp create mode 100644 gui/Protocols/IKE/ikev1-sig-a2.cpp create mode 100644 gui/Protocols/IKE/ikev1-sig-m-perlman.cpp create mode 100644 gui/Protocols/IKE/ikev1-sig-m.cpp create mode 100644 gui/Protocols/IKE/ikev2-child-nopfs.cpp create mode 100644 gui/Protocols/IKE/ikev2-child.cpp create mode 100644 gui/Protocols/IKE/ikev2-eap.cpp create mode 100644 gui/Protocols/IKE/ikev2-eap2.cpp create mode 100644 gui/Protocols/IKE/ikev2-mac.cpp create mode 100644 gui/Protocols/IKE/ikev2-mac2.cpp create mode 100644 gui/Protocols/IKE/ikev2-mactosig.cpp create mode 100644 gui/Protocols/IKE/ikev2-mactosig2.cpp create mode 100644 gui/Protocols/IKE/ikev2-sig-child-composed.cpp create mode 100644 gui/Protocols/IKE/ikev2-sig-child.cpp create mode 100644 gui/Protocols/IKE/ikev2-sig-child2-composed.cpp create mode 100644 gui/Protocols/IKE/ikev2-sig-child2.cpp create mode 100644 gui/Protocols/IKE/ikev2-sig.cpp create mode 100644 gui/Protocols/IKE/ikev2-sig2.cpp create mode 100644 gui/Protocols/IKE/ikev2-sigtomac.cpp create mode 100644 gui/Protocols/IKE/ikev2-sigtomac2.cpp create mode 100644 gui/Protocols/IKE/jfki-core.cpp create mode 100644 gui/Protocols/IKE/jfki.cpp create mode 100644 gui/Protocols/IKE/jfkr-core.cpp create mode 100644 gui/Protocols/IKE/jfkr.cpp create mode 100755 gui/Protocols/IKE/make-mpa.py create mode 100644 gui/Protocols/IKE/mpa/README.txt create mode 100644 gui/Protocols/IKE/oakley-a.cpp create mode 100644 gui/Protocols/IKE/oakley-alt.cpp create mode 100644 gui/Protocols/IKE/oakley-c.cpp create mode 100755 gui/Protocols/IKE/pp.sh create mode 100755 gui/Protocols/IKE/scanner.py create mode 100644 gui/Protocols/IKE/skeme-basic.cpp create mode 100644 gui/Protocols/IKE/skeme-psk.cpp create mode 100644 gui/Protocols/IKE/skeme-rekey.cpp create mode 100644 gui/Protocols/IKE/sts-mac.cpp create mode 100644 gui/Protocols/IKE/sts-main.cpp create mode 100644 gui/Protocols/IKE/sts-modified.cpp create mode 100755 gui/Protocols/IKE/verify.sh create mode 100755 gui/Protocols/IKE/verify_all.sh diff --git a/gui/Protocols/IKE/Makefile b/gui/Protocols/IKE/Makefile new file mode 100644 index 0000000..7234a64 --- /dev/null +++ b/gui/Protocols/IKE/Makefile @@ -0,0 +1,11 @@ +CPPSRC= $(wildcard *.cpp) +DEST= $(CPPSRC:.cpp=.spdl) + +default: $(DEST) + +%.spdl: %.cpp + cpp $< >$@ + +mpa: $(DEST) make-mpa.py + ./make-mpa.py + diff --git a/gui/Protocols/IKE/common.h b/gui/Protocols/IKE/common.h new file mode 100644 index 0000000..6dcb5d2 --- /dev/null +++ b/gui/Protocols/IKE/common.h @@ -0,0 +1,157 @@ +/**************************************************************************** + * THIS FILE CONTAINS DEFINITIONS OF COMMON MACROS AND TYPES * + ****************************************************************************/ + + hashfunction prf, KDF; + +/********************************** + * DIFFIE-HELLMAN ABSTRACTIONS * + * Zi = Gr^i = g^(ri) + * Zr = Gi^r = g^(ir) + **********************************/ +const g, h: Function; +#define Zi h(Gr,i) +#define Zr h(Gi,r) + +/********************************** + * PROTOCOL DEPENDENT DEFINITIONS * + **********************************/ +#ifdef __IKEV1__ +hashfunction H; +#define SKi KDF(Ni, Nr, Zi, Ci, Cr) +#define SKr KDF(Ni, Nr, Zr, Ci, Cr) +#endif + +#ifdef __IKEV1_PSK__ +#define SKi prf(k(I,R), Ni, Nr, Zi, Ci, Cr) +#define SKr prf(k(R,I), Ni, Nr, Zr, Ci, Cr) +#endif + +#ifdef __IKEV1_QUICK__ +/* k(.,.) equals Kd from the spec */ +#define SKi KDF(k(I,R),Zi,Ni,Nr) +#define SKr KDF(k(R,I),Zr,Ni,Nr) +#endif + +#ifdef __IKEV1_QUICK_NOPFS__ +/* k(.,.) equals Kd from the spec */ +#define SKi KDF(k(I,R),Ni,Nr) +#define SKr KDF(k(R,I),Ni,Nr) +#endif + +#ifdef __IKEV2__ +hashfunction MAC; +#define HDR (SPIi,SPIr) +#define SKi KDF(Ni,Nr,Zi,SPIi,SPIr) +#define SKr KDF(Ni,Nr,Zr,SPIi,SPIr) +#endif + +#ifdef __IKEV2_CHILD__ +#define SKi KDF(k(I,R),Zi,Ni,Nr) +#define SKr KDF(k(R,I),Zr,Ni,Nr) +#endif + +#ifdef __IKEV2_CHILD_NOPFS__ +#define SKi KDF(k(I,R),Ni,Nr) +#define SKr KDF(k(R,I),Ni,Nr) +#endif + +#ifdef __JFK_CORE__ +hashfunction H; +#define SKi KDF(Zi, Ni, Nr) +#define SKr KDF(Zr, Ni, Nr) +#endif + +#ifdef __JFK__ +hashfunction H; +#define SKi KDF(Zi, H(Ni), Nr) +#define SKr KDF(Zr, H(Ni), Nr) +#endif + +#ifdef __OAKLEY__ +#define SKi KDF(Ni, Nr, Zi, Ci, Cr) +#define SKr KDF(Ni, Nr, Zr, Ci, Cr) +#endif + +#ifdef __OAKLEY_CONSERVATIVE__ +#define SKi KDF(Ni, Nr, Zi, Ci, Cr) +#define SKr KDF(Ni, Nr, Zr, Ci, Cr) +#endif + +#ifdef __SKEME__ +#define SKi KDF(Zi) +#define SKr KDF(Zr) +#endif + +#ifdef __SKEME_REKEY__ +#define SKi KDF(k(I,R),prf(k(I,R), Ni, Nr, R, I)) +#define SKr KDF(k(R,I),prf(k(R,I), Ni, Nr, R, I)) +#endif + +#ifdef __STS__ +#define SKi KDF(Zi) +#define SKr KDF(Zr) +hashfunction MAC; +#endif + +protocol @oracle (DH, SWAP) { +#define Gi g(i) +#define Gr g(r) + + /* Diffie-Hellman oracle: If the adversary is in possession of g^xy, he + * can obtain g^yx. + * @obsolete The adversary does not need DH as long as SWAP exists + */ + role DH { + var i, r: Nonce; + + recv_!DH1( DH, DH, Zi ); + send_!DH2( DH, DH, Zr ); + } + + /* Session key swap oracle: If the adversary is in possession of eg the + * initiators session key, he can obtain the responders session key. + */ + role SWAP { + var i, r, Ni, Nr: Nonce; + +#ifdef __IKEV1__ + var Ci, Cr: Nonce; +#endif +#ifdef __IKEV1_PSK__ + var Ci, Cr: Nonce; + var I, R: Agent; +#endif +#ifdef __IKEV1_QUICK__ + var I, R: Agent; +#endif +#ifdef __IKEV1_QUICK_NOPFS__ + var I, R: Agent; +#endif +#ifdef __IKEV2__ + var SPIi, SPIr: Nonce; +#endif +#ifdef __IKEV2_CHILD__ + var I, R: Agent; +#endif +#ifdef __IKEV2_CHILD_NOPFS__ + var I, R: Agent; +#endif +#ifdef __OAKLEY__ + var Ci, Cr: Nonce; +#endif +#ifdef __OAKLEY_CONSERVATIVE__ + var Ci, Cr: Nonce; +#endif +#ifdef __SKEME_REKEY__ + var I, R: Agent; +#endif + + recv_!SWAP1( SWAP, SWAP, SKi ); + send_!SWAP2( SWAP, SWAP, SKr ); + + } +#undef Gi +#undef Gr +} +#define __ORACLE__ \ No newline at end of file diff --git a/gui/Protocols/IKE/ikev1-pk-a1.cpp b/gui/Protocols/IKE/ikev1-pk-a1.cpp new file mode 100644 index 0000000..86947a8 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a1.cpp @@ -0,0 +1,96 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Public key authentication (aggressive mode), + * last message not encrypted + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define HASH1 H(CERT(R)) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, HASH_Ii ); + send_!O4( O, O, HASH_Ir ); + + } +#undef Gi +#undef Gr +} + + +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), HASH_Ri ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!3( I, R, Ci, Cr, HASH_Ii ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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), HASH_Rr ); + recv_!3( I, R, Ci, Cr, HASH_Ir ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk-a12.cpp new file mode 100644 index 0000000..435479a --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a12.cpp @@ -0,0 +1,95 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Public key authentication (aggressive mode), + * last message encrypted + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define HASH1 H(CERT(R)) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, {HASH_Ii}SKi ); + send_!O4( O, O, {HASH_Ir}SKr ); + + } +#undef Gi +#undef Gr +} + +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), HASH_Ri ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!3( I, R, Ci, Cr, {HASH_Ii}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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), HASH_Rr ); + recv_!3( I, R, Ci, Cr, {HASH_Ir}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk-a2.cpp new file mode 100644 index 0000000..b149cfe --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a2.cpp @@ -0,0 +1,97 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Public key authentication (aggressive mode), + * last message not encrypted, nonce and id encrypted + * together + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define HASH1 H(CERT(R)) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, HASH_Ii ); + send_!O4( O, O, HASH_Ir ); + + } +#undef Gi +#undef Gr +} + + +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), HASH_Ri ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!3( I, R, Ci, Cr, HASH_Ii ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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), HASH_Rr ); + recv_!3( I, R, Ci, Cr, HASH_Ir ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk-a22.cpp new file mode 100644 index 0000000..a71e20a --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-a22.cpp @@ -0,0 +1,95 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Public key authentication (aggressive mode), + * last message encrypted, nonce and id encrypted together + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define HASH1 H(CERT(R)) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, {HASH_Ii}SKi ); + send_!O4( O, O, {HASH_Ir}SKr ); + + } +#undef Gi +#undef Gr +} + +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), HASH_Ri ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!3( I, R, Ci, Cr, {HASH_Ii}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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), HASH_Rr ); + recv_!3( I, R, Ci, Cr, {HASH_Ir}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk-m.cpp new file mode 100644 index 0000000..1b27c5f --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-m.cpp @@ -0,0 +1,103 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Public key authentication (main mode) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define HASH1 H({R, pk(R)}sk(s)) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {HASH_Ii}SKi ); + send_!O2( O, O, {HASH_Ir}SKr ); + + // msg 6 + recv_!O3( O, O, {HASH_Rr}SKr ); + send_!O4( O, O, {HASH_Ri}SKi ); + + } +#undef Gi +#undef Gr +} + + +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, {HASH_Ii}SKi ); + recv_!6( R, I, Ci, Cr, {HASH_Ri}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, {HASH_Ir}SKr ); + claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr ); + send_!6( R, I, Ci, Cr, {HASH_Rr}SKr ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk-m2.cpp new file mode 100644 index 0000000..fc08ea0 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk-m2.cpp @@ -0,0 +1,102 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Public key authentication (main mode), + * Nonce and id encrypted together + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {HASH_Ii}SKi ); + send_!O2( O, O, {HASH_Ir}SKr ); + + // msg 6 + recv_!O3( O, O, {HASH_Rr}SKr ); + send_!O4( O, O, {HASH_Ri}SKi ); + + } +#undef Gi +#undef Gr +} + +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, {HASH_Ii}SKi ); + recv_!6( R, I, Ci, Cr, {HASH_Ri}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, {HASH_Ir}SKr ); + claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr ); + send_!6( R, I, Ci, Cr, {HASH_Rr}SKr ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk2-a.cpp new file mode 100644 index 0000000..9549e44 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-a.cpp @@ -0,0 +1,97 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Revised public key authentication (aggressive mode) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define Nei prf(Ni, Ci) +#define Ner prf(Nr, Cr) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, HASH_Ir ); + send_!O4( O, O, HASH_Ii ); + + } +#undef Gi +#undef Gr +} + + +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)}Nei, {I}Nei ); + recv_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {Gr}Ner, {R}Ner, HASH_Ri ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!3( I, R, Ci, Cr, HASH_Ii ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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}Nei, {I}Nei ); + claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr ); + send_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {g(r)}Ner, {R}Ner, HASH_Rr ); + recv_!3( I, R, Ci, Cr, HASH_Ir ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk2-a2.cpp new file mode 100644 index 0000000..a8536fb --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-a2.cpp @@ -0,0 +1,97 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Revised public key authentication (aggressive mode), + * Diffie-Hellman token encrypted together with identity + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define Nei prf(Ni, Ci) +#define Ner prf(Nr, Cr) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, HASH_Ir ); + send_!O4( O, O, HASH_Ii ); + + } +#undef Gi +#undef Gr +} + +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}Nei ); + recv_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {Gr,R}Ner, HASH_Ri ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!3( I, R, Ci, Cr, HASH_Ii ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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}Nei ); + claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr ); + send_!2( R, I, Ci, Cr, algo, {Nr}pk(I), {g(r),R}Ner, HASH_Rr ); + recv_!3( I, R, Ci, Cr, HASH_Ir ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk2-m.cpp new file mode 100644 index 0000000..42f2d9d --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-m.cpp @@ -0,0 +1,104 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Revised public key authentication (main mode) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define Nei prf(Ni, Ci) +#define Ner prf(Nr, Cr) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {HASH_Ii}SKi ); + send_!O2( O, O, {HASH_Ir}SKr ); + + // msg 6 + recv_!O3( O, O, {HASH_Rr}SKr ); + send_!O4( O, O, {HASH_Ri}SKi ); + + } +#undef Gi +#undef Gr +} + + +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)}Nei, {I}Nei ); + recv_4( R, I, Ci, Cr, {Nr}pk(I), {Gr}Ner, {R}Ner ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!5( I, R, Ci, Cr, {HASH_Ii}SKi ); + recv_!6( R, I, Ci, Cr, {HASH_Ri}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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}Nei, {I}Nei ); + send_4( R, I, Ci, Cr, {Nr}pk(I), {g(r)}Ner, {R}Ner ); + recv_!5( I, R, Ci, Cr, {HASH_Ir}SKr ); + claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr ); + send_!6( R, I, Ci, Cr, {HASH_Rr}SKr ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-pk2-m2.cpp new file mode 100644 index 0000000..653a839 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-pk2-m2.cpp @@ -0,0 +1,106 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Revised public key authentication (aggressive mode), + * Diffie-Hellman token encrypted together with identity + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(H(Ni,Nr),Ci,Cr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) +#define HASH1 H({R, pk(R)}sk(s)) +#define Nei prf(Ni, Ci) +#define Ner prf(Nr, Cr) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {HASH_Ii}SKi ); + send_!O2( O, O, {HASH_Ir}SKr ); + + // msg 6 + recv_!O3( O, O, {HASH_Rr}SKr ); + send_!O4( O, O, {HASH_Ri}SKi ); + + } +#undef Gi +#undef Gr +} + + +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}Nei ); + recv_4( R, I, Ci, Cr, {Nr}pk(I), {Gr,R}Ner ); + claim( I, Running, R, g(i),Gr,Ci,Cr,Ni,Nr ); + send_!5( I, R, Ci, Cr, {HASH_Ii}SKi ); + recv_!6( R, I, Ci, Cr, {HASH_Ri}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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}Nei ); + send_4( R, I, Ci, Cr, {Nr}pk(I), {g(r),R}Ner ); + recv_!5( I, R, Ci, Cr, {HASH_Ir}SKr ); + claim( R, Running, I, Gi,g(r),Ci,Cr,Ni,Nr ); + send_!6( R, I, Ci, Cr, {HASH_Rr}SKr ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-psk-a.cpp new file mode 100644 index 0000000..bdd5b4c --- /dev/null +++ b/gui/Protocols/IKE/ikev1-psk-a.cpp @@ -0,0 +1,94 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Pre-shared key authentication (aggressive mode) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1_PSK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HASH_Ii prf(k(I,R), Ni, Nr, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(k(R,I), Ni, Nr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(k(I,R), Ni, Nr, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(k(R,I), Ni, Nr, g(r), Gi, Cr, Ci, list, R) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, HASH_Rr ); + send_!O2( O, O, HASH_Ri ); + + // msg 3 + recv_!O3( O, O, HASH_Ii ); + send_!O4( O, O, HASH_Ir ); + + } +#undef Gi +#undef Gr +} + + +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, HASH_Ri ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!3( I, R, Ci, Cr, HASH_Ii ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HASH_Rr ); + recv_!3( I, R, Ci, Cr, HASH_Ir ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-psk-m-perlman.cpp new file mode 100644 index 0000000..01640ad --- /dev/null +++ b/gui/Protocols/IKE/ikev1-psk-m-perlman.cpp @@ -0,0 +1,101 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Pre-shared key authentication (main mode) incorporating + * a fix by Perlman et. al. + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1_PSK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HASH_Ii prf(k(I,R), Ni, Nr, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(k(R,I), Ni, Nr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(k(I,R), Ni, Nr, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(k(R,I), Ni, Nr, g(r), Gi, Cr, Ci, list, R) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {I, HASH_Ii}Zi ); + send_!O2( O, O, {I, HASH_Ir}Zr ); + + // msg 6 + recv_!O3( O, O, {R, HASH_Rr}Zr ); + send_!O4( O, O, {R, HASH_Ri}Zi ); + + } +#undef Gi +#undef Gr +} + + +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, HASH_Ii}Zi ); + recv_!6( R, I, Ci, Cr, {R, HASH_Ri}Zi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HASH_Ir}Zr ); + claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr ); + send_!6( R, I, Ci, Cr, {R, HASH_Rr}Zr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-psk-m.cpp new file mode 100644 index 0000000..f203018 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-psk-m.cpp @@ -0,0 +1,100 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Pre-shared key authentication (main mode) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1_PSK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYID prf(k(I,R),Ni,Nr) +#define HASH_Ii prf(k(I,R), Ni, Nr, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(k(R,I), Ni, Nr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(k(I,R), Ni, Nr, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(k(R,I), Ni, Nr, g(r), Gi, Cr, Ci, list, R) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {I, HASH_Ii}SKi ); + send_!O2( O, O, {I, HASH_Ir}SKr ); + + // msg 6 + recv_!O3( O, O, {R, HASH_Rr}SKr ); + send_!O4( O, O, {R, HASH_Ri}SKi ); + + } +#undef Gi +#undef Gr +} + +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, HASH_Ii}SKi ); + recv_!6( R, I, Ci, Cr, {R, HASH_Ri}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HASH_Ir}SKr ); + claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr ); + send_!6( R, I, Ci, Cr, {R, HASH_Rr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-quick-noid.cpp new file mode 100644 index 0000000..f6f5712 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-quick-noid.cpp @@ -0,0 +1,102 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Quick mode (pfs), without optional identities + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1_QUICK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/* k(I,R)=k(R,I) equal Ka from the spec */ +#define HASH1i prf(k(I,R), mid, list, Ni, g(i)) +#define HASH1r prf(k(R,I), mid, list, Ni, Gi) +#define HASH2i prf(k(I,R), mid, Ni, algo, Nr, Gr) +#define HASH2r prf(k(R,I), mid, Ni, algo, Nr, g(r)) +#define HASH3i prf(k(I,R), mid, Ni, Nr) +#define HASH3r prf(k(R,I), mid, Ni, Nr) + +usertype String; +const list, algo: String; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling k(I,R) = k(R,I). + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var mid, i, r, Ni, Nr: Nonce; + var I, R: Agent; + + // msg 1 + recv_!O1( O, O, {HASH1i, list, Ni, g(i)}k(I,R) ); + send_!O2( O, O, {HASH1r, list, Ni, Gi}k(R,I) ); + + // msg 2 + recv_!O3( O, O, {HASH2r, algo, Nr, g(r)}k(R,I) ); + send_!O4( O, O, {HASH2i, algo, Nr, Gr}k(I,R) ); + + // msg 3 + recv_!O5( O, O, {HASH3i}k(I,R) ); + send_!O6( O, O, {HASH3r}k(R,I) ); + + } +#undef Gi +#undef Gr +} + + +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, {HASH1i, list, Ni, g(i)}k(I,R) ); + recv_!2( R, I, mid, {HASH2i, algo, Nr, Gr}k(I,R) ); + claim( I, Running, R, Ni, Nr, g(i), Gr ); + send_!3( I, R, mid, {HASH3i}k(I,R) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, {HASH1r, list, Ni, Gi}k(R,I) ); + claim( R, Running, I, Ni, Nr, Gi, g(r) ); + send_!2( R, I, mid, {HASH2r, algo, Nr, g(r)}k(R,I) ); + recv_!3( I, R, mid, {HASH3r}k(R,I) ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I, Ni, Nr, Gi, g(r) ); + + } +} +// TODO: Incorporate into various phase 1 protocols (see spec for adaptions) +// NOTE: If incorporated in phase 1, make sure to model with and without optional identities in msg 2 & 3 diff --git a/gui/Protocols/IKE/ikev1-quick-nopfs.cpp b/gui/Protocols/IKE/ikev1-quick-nopfs.cpp new file mode 100644 index 0000000..38a1fc4 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-quick-nopfs.cpp @@ -0,0 +1,96 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Quick mode (no pfs), without optional identities + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1_QUICK_NOPFS__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/* k(I,R)=k(R,I) equal Ka from the spec */ +#define HASH1i prf(k(I,R), mid, list, Ni) +#define HASH1r prf(k(R,I), mid, list, Ni) +#define HASH2i prf(k(I,R), mid, Ni, algo, Nr) +#define HASH2r prf(k(R,I), mid, Ni, algo, Nr) +#define HASH3i prf(k(I,R), mid, Ni, Nr) +#define HASH3r prf(k(R,I), mid, Ni, Nr) + +usertype String; +const list, algo: String; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling k(I,R) = k(R,I). + */ +protocol @executability(O) { + role O { + var mid, Ni, Nr: Nonce; + var I, R: Agent; + + // msg 1 + recv_!O1( O, O, {HASH1i, list, Ni}k(I,R) ); + send_!O2( O, O, {HASH1r, list, Ni}k(R,I) ); + + // msg 2 + recv_!O3( O, O, {HASH2r, algo, Nr}k(R,I) ); + send_!O4( O, O, {HASH2i, algo, Nr}k(I,R) ); + + // msg 3 + recv_!O5( O, O, {HASH3i}k(I,R) ); + send_!O6( O, O, {HASH3r}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, {HASH1i, list, Ni}k(I,R) ); + recv_!2( R, I, mid, {HASH2i, algo, Nr}k(I,R) ); + claim( I, Running, R, Ni, Nr ); + send_!3( I, R, mid, {HASH3i}k(I,R) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, {HASH1r, list, Ni}k(R,I) ); + claim( R, Running, I, Ni, Nr ); + send_!2( R, I, mid, {HASH2r, algo, Nr}k(R,I) ); + recv_!3( I, R, mid, {HASH3r}k(R,I) ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I, Ni, Nr ); + + } +} +// TODO: Incorporate into various phase 1 protocols (see spec for adaptions) +// NOTE: If incorporated in phase 1, make sure to model with and without optional identities in msg 2 & 3 diff --git a/gui/Protocols/IKE/ikev1-quick.cpp b/gui/Protocols/IKE/ikev1-quick.cpp new file mode 100644 index 0000000..60e9fcc --- /dev/null +++ b/gui/Protocols/IKE/ikev1-quick.cpp @@ -0,0 +1,70 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Quick mode (pfs), optional identities included + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1_QUICK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/* k(I,R) equals Ka from the spec */ +#define HASH1i prf(k(I,R), mid, list, Ni, g(i), I, R) +#define HASH1r prf(k(R,I), mid, list, Ni, Gi, I, R) +#define HASH2i prf(k(I,R), mid, Ni, algo, Nr, Gr, I, R) +#define HASH2r prf(k(R,I), mid, Ni, algo, Nr, g(r), I, R) +#define HASH3i prf(k(I,R), mid, Ni, Nr) +#define HASH3r prf(k(R,I), mid, Ni, Nr) + + +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, {HASH1i, list, Ni, g(i), I, R}k(I,R) ); + recv_!2( R, I, mid, {HASH2i, algo, Nr, Gr, I, R}k(I,R) ); + claim( I, Running, R, Ni, Nr, g(i), Gr ); + send_!3( I, R, mid, {HASH3i}k(I,R) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, {HASH1r, list, Ni, Gi, I, R}k(I,R) ); + claim( R, Running, I, Ni, Nr, Gi, g(r) ); + send_!2( R, I, mid, {HASH2r, algo, Nr, g(r), I, R}k(I,R) ); + recv_!3( I, R, mid, {HASH3r}k(I,R) ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I, Ni, Nr, Gi, g(r) ); + + } +} +// TODO: Incorporate into various phase 1 protocols (see spec for adaptions) +// NOTE: If incorporated in phase 1, make sure to model with and without optional identities in msg 2 & 3 diff --git a/gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp b/gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp new file mode 100644 index 0000000..ddebfcb --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp @@ -0,0 +1,99 @@ +/*********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Digital signature authentication (aggressive mode) with + * a modification suggested by Perlman et al. (last msg not + * encrypted) + ***********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HDR (Ci,Cr) +#define SKEYIDi prf(Ni,Nr,Zi) +#define SKEYIDr prf(Ni,Nr,Zr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, {R}SKr, {HASH_Rr}sk(R) ); + send_!O2( O, O, {R}SKi, {HASH_Ri}sk(R) ); + + // msg 3 + recv_!O3( O, O, {I}SKi, {HASH_Ii}sk(I) ); + send_!O4( O, O, {I}SKr, {HASH_Ir}sk(I) ); + + } +#undef Gi +#undef Gr +} + + +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, HDR, algo, Gr, Nr, {R}SKi, {HASH_Ri}sk(R) ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!3( I, R, HDR, {I}SKi, {HASH_Ii}sk(I) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HDR, algo, g(r), Nr, R, {R}SKr, {HASH_Rr}sk(R) ); + recv_!3( I, R, HDR, {I}SKr, {HASH_Ir}sk(I) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-sig-a-perlman2.cpp new file mode 100644 index 0000000..e39a7b9 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a-perlman2.cpp @@ -0,0 +1,99 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Digital signature authentication (aggressive mode) with + * a modification suggested by Perlman et al. (last msg + * encrypted) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HDR (Ci,Cr) +#define SKEYIDi prf(Ni,Nr,Zi) +#define SKEYIDr prf(Ni,Nr,Zr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, {R}SKr, {HASH_Rr}sk(R) ); + send_!O2( O, O, {R}SKi, {HASH_Ri}sk(R) ); + + // msg 3 + recv_!O3( O, O, {I, {HASH_Ii}sk(I)}SKi ); + send_!O4( O, O, {I, {HASH_Ir}sk(I)}SKr ); + + } +#undef Gi +#undef Gr +} + + +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, HDR, algo, Gr, Nr, {R}SKi, {HASH_Ri}sk(R) ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!3( I, R, HDR, {I, {HASH_Ii}sk(I)}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HDR, algo, g(r), Nr, R, {R}SKr, {HASH_Rr}sk(R) ); + recv_!3( I, R, HDR, {I, {HASH_Ir}sk(I)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-sig-a1.cpp new file mode 100644 index 0000000..418492e --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a1.cpp @@ -0,0 +1,98 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Digital signature authentication (aggressive mode) + * where the last message is not encrypted + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HDR (Ci,Cr) +#define SKEYIDi prf(Ni,Nr,Zi) +#define SKEYIDr prf(Ni,Nr,Zr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, {HASH_Rr}sk(R) ); + send_!O2( O, O, {HASH_Ri}sk(R) ); + + // msg 3 + recv_!O3( O, O, {HASH_Ii}sk(I) ); + send_!O4( O, O, {HASH_Ir}sk(I) ); + + } +#undef Gi +#undef Gr +} + + +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, HDR, algo, Gr, Nr, R, {HASH_Ri}sk(R) ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!3( I, R, HDR, {HASH_Ii}sk(I) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HDR, algo, g(r), Nr, R, {HASH_Rr}sk(R) ); + recv_!3( I, R, HDR, {HASH_Ir}sk(I) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-sig-a2.cpp new file mode 100644 index 0000000..1c81dab --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-a2.cpp @@ -0,0 +1,99 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Digital signature authentication (aggressive mode) + * where thelast message is encrypted with the session key + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HDR (Ci,Cr) +#define SKEYIDi prf(Ni,Nr,Zi) +#define SKEYIDr prf(Ni,Nr,Zr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, {HASH_Rr}sk(R) ); + send_!O2( O, O, {HASH_Ri}sk(R) ); + + // msg 3 + recv_!O3( O, O, {{HASH_Ii}sk(I)}SKi ); + send_!O4( O, O, {{HASH_Ir}sk(I)}SKr ); + + } +#undef Gi +#undef Gr +} + + +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, HDR, algo, Gr, Nr, R, {HASH_Ri}sk(R) ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!3( I, R, HDR, {{HASH_Ii}sk(I)}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HDR, algo, g(r), Nr, R, {HASH_Rr}sk(R) ); + recv_!3( I, R, HDR, {{HASH_Ir}sk(I)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-sig-m-perlman.cpp new file mode 100644 index 0000000..4129ae2 --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-m-perlman.cpp @@ -0,0 +1,100 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Digital signature authentication (aggressive mode) with + * a modification suggested by Perlman et al. + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define SKEYIDi prf(Ni,Nr,Zi) +#define SKEYIDr prf(Ni,Nr,Zr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 4 + recv_!O1( O, O, {R, {HASH_Rr}sk(R)}SKr ); + send_!O2( O, O, {R, {HASH_Ri}sk(R)}SKi ); + + // msg 5 + recv_!O3( O, O, {I, {HASH_Ii}sk(I)}SKi ); + send_!O4( O, O, {I, {HASH_Ir}sk(I)}SKr ); + + } +#undef Gi +#undef Gr +} + + +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, {HASH_Ri}sk(R)}SKi ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!5( I, R, Ci, Cr, {I, {HASH_Ii}sk(I)}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, {HASH_Rr}sk(R)}SKr ); + recv_!5( I, R, Ci, Cr, {I, {HASH_Ir}sk(I)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev1-sig-m.cpp new file mode 100644 index 0000000..f24b78f --- /dev/null +++ b/gui/Protocols/IKE/ikev1-sig-m.cpp @@ -0,0 +1,102 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv1) + * @reference RFC 2409, + * Boyd C. and Mathuria A., Protocols for Authentication + * and Key Agreement + * @variant Digital signature authentication (aggressive mode) + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV1__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define HDR (Ci,Cr) +#define SKEYIDi prf(Ni,Nr,Zi) +#define SKEYIDr prf(Ni,Nr,Zr) +#define HASH_Ii prf(Ni, Nr, Zi, g(i), Gr, Ci, Cr, list, I) +#define HASH_Ir prf(Ni, Nr, Zr, Gi, g(r), Ci, Cr, list, I) +#define HASH_Ri prf(Ni, Nr, Zi, Gr, g(i), Cr, Ci, list, R) +#define HASH_Rr prf(Ni, Nr, Zr, g(r), Gi, Cr, Ci, list, R) + + +usertype String; +const list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {I, {HASH_Ii}sk(I)}SKi ); + send_!O2( O, O, {I, {HASH_Ir}sk(I)}SKr ); + + // msg 6 + recv_!O3( O, O, {R, {HASH_Rr}sk(R)}SKr ); + send_!O4( O, O, {R, {HASH_Ri}sk(R)}SKi ); + + } +#undef Gi +#undef Gr +} + +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, HDR, algo ); + send_3( I, R, HDR, g(i), Ni ); + recv_4( R, I, HDR, Gr, Nr ); + claim( I, Running, R, Ni, Nr, g(i), Gr, Ci, Cr ); + send_!5( I, R, HDR, {I, {HASH_Ii}sk(I)}SKi ); + recv_!6( R, I, HDR, {R, {HASH_Ri}sk(R)}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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, HDR, algo ); + recv_3( I, R, HDR, Gi, Ni ); + send_4( R, I, HDR, g(r), Nr ); + recv_!5( I, R, HDR, {I, {HASH_Ir}sk(I)}SKr ); + claim( R, Running, I, Ni, Nr, Gi, g(r), Ci, Cr ); + send_!6( R, I, HDR, {R, {HASH_Rr}sk(R)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-child-nopfs.cpp new file mode 100644 index 0000000..9607308 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-child-nopfs.cpp @@ -0,0 +1,78 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol IKE Create Child SA + * @reference RFC 4306 + * @variant No perfect forward secrecy support + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2_CHILD_NOPFS__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +const SA3: Nonce; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling k(I,R) = k(R,I). + */ +protocol @executability(O) { + role O { + var Ni, Nr: Nonce; + var I, R: Agent; + + // msg 1 + recv_!O1( O, O, {SA3, Ni}k(I,R) ); + send_!O2( O, O, {SA3, Ni}k(R,I) ); + + // msg 2 + 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; + + /* IKE_SA_INIT */ + claim( I, Running, R,Ni ); + send_!1( I, R, {SA3, Ni}k(I,R) ); + recv_!2( R, I, {SA3, Nr}k(I,R) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Ni ); + } +} diff --git a/gui/Protocols/IKE/ikev2-child.cpp b/gui/Protocols/IKE/ikev2-child.cpp new file mode 100644 index 0000000..2378231 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-child.cpp @@ -0,0 +1,87 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol IKE Create Child SA + * @reference RFC 4306 + * @variant Supports perfect forward secrecy + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2_CHILD__ +#ifndef __ORACLE__ +#include "common.h" +#endif + + +usertype SecurityAssociation; +const SA1 ,SA2, SA3: SecurityAssociation; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling k(I,R) = k(R,I). + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr: Nonce; + var I, R: Agent; + + // msg 1 + recv_!O1( O, O, {SA3, Ni, g(i)}k(I,R) ); + send_!O2( O, O, {SA3, Ni, g(i)}k(R,I) ); + + // msg 2 + recv_!O3( O, O, {SA3, Nr, Gr}k(R,I) ); + send_!O4( O, O, {SA3, Nr, Gr}k(I,R) ); + + } +#undef Gi +#undef Gr +} + +// Note: SPIs not modeled as they would lead to trivial attacks where the adversary +// tampers with the SPIs (they are not subsequently authenticated) +protocol ikev2-child(I, R) +{ + + role I { + fresh i, Ni: Nonce; + var Nr: Nonce; + var Gr: Ticket; + + /* IKE_SA_INIT */ + 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) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Ni,Gi ); + } +} diff --git a/gui/Protocols/IKE/ikev2-eap.cpp b/gui/Protocols/IKE/ikev2-eap.cpp new file mode 100644 index 0000000..7d8310b --- /dev/null +++ b/gui/Protocols/IKE/ikev2-eap.cpp @@ -0,0 +1,131 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol IKE EAP + * @reference RFC 4306 + * @variant Includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr, EAP, EAPOK: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, EAP}SKr ); + send_!E4( E, E, {R, AUTHri, EAP}SKi ); + + // msg 5 + recv_!E5( E, E, {EAP}SKi ); + send_!E6( E, E, {EAP}SKr ); + + // msg 6 + recv_!E7( E, E, {EAPOK}SKr ); + send_!E8( E, E, {EAPOK}SKi ); + + // msg 7 + recv_!E9( E, E, {AUTHii}SKi ); + send_!EA( E, E, {AUTHir}SKr ); + + // msg 8 + send_!EB( E, E, {AUTHrr, SA2, TSi, TSr}SKr ); + send_!EC( E, E, {AUTHri, SA2, TSi, TSr}SKi ); + } +#undef Gi +#undef Gr +} + + +protocol ikev2-eap(I, R) +{ + + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var EAP, EAPOK: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + send_!3( I, R, HDR, {I, R, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, EAP}SKi ); + send_!5( I, R, HDR, {EAP}SKi ); + recv_!6( R, I, HDR, {EAPOK}SKi ); + claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr,EAP,EAPOK ); + send_!7( I, R, HDR, {AUTHii}SKi ); + recv_!8( R, I, HDR, {AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, R, SA2, TSi, TSr}SKr ); + send_!4( R, I, HDR, {R, AUTHrr, EAP}SKr ); + recv_!5( I, R, HDR, {EAP}SKr ); + send_!6( R, I, HDR, {EAPOK}SKr ); + recv_!7( I, R, HDR, {AUTHir}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr,EAP,EAPOK ); + send_!8( R, I, HDR, {AUTHrr, SA2, TSi, TSr}SKr ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-eap2.cpp new file mode 100644 index 0000000..c56855a --- /dev/null +++ b/gui/Protocols/IKE/ikev2-eap2.cpp @@ -0,0 +1,138 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol IKE EAP + * @reference RFC 4306 + * @variant Excludes optional payloads + **********************************************************************/ + +/** + * Modeling notes: + * - It's not clear what to put in the EAP payloads; we now model them + * as nonces, but maybe it is better to view them as a function of the + * actor. + */ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr, EAP, EAPOK: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, EAP}SKr ); + send_!E4( E, E, {R, AUTHri, EAP}SKi ); + + // msg 5 + recv_!E5( E, E, {EAP}SKi ); + send_!E6( E, E, {EAP}SKr ); + + // msg 6 + recv_!E7( E, E, {EAPOK}SKr ); + send_!E8( E, E, {EAPOK}SKi ); + + // msg 7 + recv_!E9( E, E, {AUTHii}SKi ); + send_!EA( E, E, {AUTHir}SKr ); + + // msg 8 + send_!EB( E, E, {AUTHrr, SA2, TSi, TSr}SKr ); + send_!EC( E, E, {AUTHri, SA2, TSi, TSr}SKi ); + } +#undef Gi +#undef Gr +} + + +protocol ikev2-eap2(I, R) +{ + + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var EAP, EAPOK: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + send_!3( I, R, HDR, {I, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, EAP}SKi ); + send_!5( I, R, HDR, {EAP}SKi ); + recv_!6( R, I, HDR, {EAPOK}SKi ); + claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr,EAP,EAPOK ); + send_!7( I, R, HDR, {AUTHii}SKi ); + recv_!8( R, I, HDR, {AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, SA2, TSi, TSr}SKr ); + send_!4( R, I, HDR, {R, AUTHrr, EAP}SKr ); + recv_!5( I, R, HDR, {EAP}SKr ); + send_!6( R, I, HDR, {EAPOK}SKr ); + recv_!7( I, R, HDR, {AUTHir}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr,EAP,EAPOK ); + send_!8( R, I, HDR, {AUTHrr, SA2, TSi, TSr}SKr ); + + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-mac.cpp new file mode 100644 index 0000000..832afae --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mac.cpp @@ -0,0 +1,104 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol MAC authenticated IKEv2 + * @reference RFC 4306 + * @variant Includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)) +#define AUTHir MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)) +#define AUTHri MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)) +#define AUTHrr MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-mac(I, R) +{ + + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr); + send_!3( I, R, HDR, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-mac2.cpp new file mode 100644 index 0000000..cb09faa --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mac2.cpp @@ -0,0 +1,104 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol MAC authenticated IKEv2 + * @reference RFC 4306 + * @variant Excludes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)) +#define AUTHir MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)) +#define AUTHri MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)) +#define AUTHrr MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-mac2(I, R) +{ + + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R, Ni,g(i),Nr,Gr,TSi,TSr ); + send_!3( I, R, HDR, {I, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-mactosig.cpp new file mode 100644 index 0000000..519f93a --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mactosig.cpp @@ -0,0 +1,104 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Initiator authenticates itself using message + * authentication codes while responder uses digital + * signatures. Includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)) +#define AUTHir MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-mactosig(I, R) +{ + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R,Ni,g(i),Nr,Gr,TSi,TSr ); + send_!3( I, R, SPIi, SPIr, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, SPIi, SPIr, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, SPIi, SPIr, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, SPIi, SPIr, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr ); + send_!4( R, I, SPIi, SPIr, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-mactosig2.cpp new file mode 100644 index 0000000..73b20f5 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-mactosig2.cpp @@ -0,0 +1,103 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Initiator authenticates itself using message + * authentication codes while responder uses digital + * signatures. Excludes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii MAC(k(I,R), SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)) +#define AUTHir MAC(k(R,I), SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + +protocol ikev2-mactosig2(I, R) +{ + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R,Ni,g(i),Nr,Gr,TSi,TSr ); + send_!3( I, R, SPIi, SPIr, {I, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, SPIi, SPIr, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, SPIi, SPIr, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, SPIi, SPIr, {I, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr ); + send_!4( R, I, SPIi, SPIr, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-sig-child-composed.cpp new file mode 100644 index 0000000..62ddf6f --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child-composed.cpp @@ -0,0 +1,138 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Combination of signature authenticated IKEv2 and + * CREATE_CHILD_SA, includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) +#define KEYMATi KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) +#define KEYMATr KDF(Ni, Nr, Zr, h(Gi,t), Mi, Mr) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + // msg 5 + recv_!E5( E, E, {SA3, Mi, g(j), TSi, TSr}SKi ); + send_!E6( E, E, {SA3, Mi, g(j), TSi, TSr}SKr ); + + // msg 6 + recv_!E7( E, E, {SA3, Mr, g(t), TSi, TSr}SKr ); + send_!E8( E, E, {SA3, Mr, g(t), TSi, TSr}SKr ); + } +#undef Gi +#undef Gr +} +protocol @ora(S) { +#define Gi g(i) +#define Gj g(j) +#define Gr g(r) +#define Gt g(t) + role S { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + + recv_!S1( S, S, KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) ); + send_!S2( S, S, KDF(Ni, Nr, Zr, h(Gj,t), Mi, Mr) ); + } +#undef Gi +#undef Gj +#undef Gr +#undef Gt +} + + +protocol ikev2-sig-child(I, R) +{ + role I { + fresh i, j, Ni, Mi, SPIi: Nonce; + var Nr, Mr, SPIr: Nonce; + var Gr, Gt: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + send_!3( I, R, HDR, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* CREATE_CHILD_SA */ + claim( I, Running, R,g(i),g(j),Gr ); + send_!5( I, R, HDR, {SA3, Mi, g(j), TSi, TSr}SKi ); + recv_!6( R, I, HDR, {SA3, Mr, Gt, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + claim( I, SKR, KEYMATi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* CREATE_CHILD_SA */ + recv_!5( I, R, HDR, {SA3, Mi, Gj, TSi, TSr}SKr ); + claim( R, Running, I,Gi,Gj,g(r),g(t) ); + send_!6( R, I, HDR, {SA3, Mr, g(t), TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + claim( R, SKR, KEYMATr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,Gj,g(r) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child.cpp b/gui/Protocols/IKE/ikev2-sig-child.cpp new file mode 100644 index 0000000..62ddf6f --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child.cpp @@ -0,0 +1,138 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Combination of signature authenticated IKEv2 and + * CREATE_CHILD_SA, includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) +#define KEYMATi KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) +#define KEYMATr KDF(Ni, Nr, Zr, h(Gi,t), Mi, Mr) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + // msg 5 + recv_!E5( E, E, {SA3, Mi, g(j), TSi, TSr}SKi ); + send_!E6( E, E, {SA3, Mi, g(j), TSi, TSr}SKr ); + + // msg 6 + recv_!E7( E, E, {SA3, Mr, g(t), TSi, TSr}SKr ); + send_!E8( E, E, {SA3, Mr, g(t), TSi, TSr}SKr ); + } +#undef Gi +#undef Gr +} +protocol @ora(S) { +#define Gi g(i) +#define Gj g(j) +#define Gr g(r) +#define Gt g(t) + role S { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + + recv_!S1( S, S, KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) ); + send_!S2( S, S, KDF(Ni, Nr, Zr, h(Gj,t), Mi, Mr) ); + } +#undef Gi +#undef Gj +#undef Gr +#undef Gt +} + + +protocol ikev2-sig-child(I, R) +{ + role I { + fresh i, j, Ni, Mi, SPIi: Nonce; + var Nr, Mr, SPIr: Nonce; + var Gr, Gt: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + send_!3( I, R, HDR, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* CREATE_CHILD_SA */ + claim( I, Running, R,g(i),g(j),Gr ); + send_!5( I, R, HDR, {SA3, Mi, g(j), TSi, TSr}SKi ); + recv_!6( R, I, HDR, {SA3, Mr, Gt, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + claim( I, SKR, KEYMATi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* CREATE_CHILD_SA */ + recv_!5( I, R, HDR, {SA3, Mi, Gj, TSi, TSr}SKr ); + claim( R, Running, I,Gi,Gj,g(r),g(t) ); + send_!6( R, I, HDR, {SA3, Mr, g(t), TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + claim( R, SKR, KEYMATr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,Gj,g(r) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child2-composed.cpp b/gui/Protocols/IKE/ikev2-sig-child2-composed.cpp new file mode 100644 index 0000000..621e7f6 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child2-composed.cpp @@ -0,0 +1,138 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Combination of signature authenticated IKEv2 and + * CREATE_CHILD_SA, excludes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) +#define KEYMATi KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) +#define KEYMATr KDF(Ni, Nr, Zr, h(Gi,t), Mi, Mr) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + // msg 5 + recv_!E5( E, E, {SA3, Mi, g(j)}SKi ); + send_!E6( E, E, {SA3, Mi, g(j)}SKr ); + + // msg 6 + recv_!E7( E, E, {SA3, Mr, g(t)}SKr ); + send_!E8( E, E, {SA3, Mr, g(t)}SKr ); + } +#undef Gi +#undef Gr +} +protocol @ora(S) { +#define Gi g(i) +#define Gj g(j) +#define Gr g(r) +#define Gt g(t) + role S { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + + recv_!S1( S, S, KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) ); + send_!S2( S, S, KDF(Ni, Nr, Zr, h(Gj,t), Mi, Mr) ); + } +#undef Gi +#undef Gj +#undef Gr +#undef Gt +} + + +protocol ikev2-sig-child2(I, R) +{ + role I { + fresh i, j, Ni, Mi, SPIi: Nonce; + var Nr, Mr, SPIr: Nonce; + var Gr, Gt: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + send_!3( I, R, HDR, {I, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* CREATE_CHILD_SA */ + claim( I, Running, R,g(i),g(j),Gr ); + send_!5( I, R, HDR, {SA3, Mi, g(j)}SKi ); + recv_!6( R, I, HDR, {SA3, Mr, Gt}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + claim( I, SKR, KEYMATi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, AUTHir, SA2, TSi, TSr}SKr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* CREATE_CHILD_SA */ + recv_!5( I, R, HDR, {SA3, Mi, Gj}SKr ); + claim( R, Running, I,Gi,Gj,g(r),g(t) ); + send_!6( R, I, HDR, {SA3, Mr, g(t)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + claim( R, SKR, KEYMATr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,Gj,g(r) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig-child2.cpp b/gui/Protocols/IKE/ikev2-sig-child2.cpp new file mode 100644 index 0000000..621e7f6 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig-child2.cpp @@ -0,0 +1,138 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Combination of signature authenticated IKEv2 and + * CREATE_CHILD_SA, excludes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) +#define KEYMATi KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) +#define KEYMATr KDF(Ni, Nr, Zr, h(Gi,t), Mi, Mr) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + // msg 5 + recv_!E5( E, E, {SA3, Mi, g(j)}SKi ); + send_!E6( E, E, {SA3, Mi, g(j)}SKr ); + + // msg 6 + recv_!E7( E, E, {SA3, Mr, g(t)}SKr ); + send_!E8( E, E, {SA3, Mr, g(t)}SKr ); + } +#undef Gi +#undef Gr +} +protocol @ora(S) { +#define Gi g(i) +#define Gj g(j) +#define Gr g(r) +#define Gt g(t) + role S { + var i, j, r, t, Mi, Ni, Mr, Nr, SPIi, SPIr: Nonce; + + recv_!S1( S, S, KDF(Ni, Nr, Zi, h(Gt,j), Mi, Mr) ); + send_!S2( S, S, KDF(Ni, Nr, Zr, h(Gj,t), Mi, Mr) ); + } +#undef Gi +#undef Gj +#undef Gr +#undef Gt +} + + +protocol ikev2-sig-child2(I, R) +{ + role I { + fresh i, j, Ni, Mi, SPIi: Nonce; + var Nr, Mr, SPIr: Nonce; + var Gr, Gt: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + send_!3( I, R, HDR, {I, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* CREATE_CHILD_SA */ + claim( I, Running, R,g(i),g(j),Gr ); + send_!5( I, R, HDR, {SA3, Mi, g(j)}SKi ); + recv_!6( R, I, HDR, {SA3, Mr, Gt}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + claim( I, SKR, KEYMATi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, AUTHir, SA2, TSi, TSr}SKr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* CREATE_CHILD_SA */ + recv_!5( I, R, HDR, {SA3, Mi, Gj}SKr ); + claim( R, Running, I,Gi,Gj,g(r),g(t) ); + send_!6( R, I, HDR, {SA3, Mr, g(t)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + claim( R, SKR, KEYMATr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,Gj,g(r) ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig.cpp b/gui/Protocols/IKE/ikev2-sig.cpp new file mode 100644 index 0000000..68e7326 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig.cpp @@ -0,0 +1,103 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol Signature authenticated IKEv2 + * @reference RFC 4306 + * @variant Includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-sig(I, R) +{ + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R,g(i),Gr,Ni,Nr ); + send_!3( I, R, HDR, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I,Gi,g(r),Ni,Nr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,g(r),Ni,Nr ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sig2.cpp b/gui/Protocols/IKE/ikev2-sig2.cpp new file mode 100644 index 0000000..e2e02b7 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sig2.cpp @@ -0,0 +1,103 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @subprotocol Signature authenticated IKEv2 + * @reference RFC 4306 + * @variant Excludes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri {SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)}sk(R) +#define AUTHrr {SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)}sk(R) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-sig2(I, R) +{ + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, HDR, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R,Ni,g(i),Nr,Gr,TSi,TSr ); + send_!3( I, R, HDR, {I, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, HDR, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, HDR, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, HDR, {I, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I, Ni,Gi,Nr,g(r),TSi,TSr ); + send_!4( R, I, HDR, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + 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.cpp b/gui/Protocols/IKE/ikev2-sigtomac.cpp new file mode 100644 index 0000000..dc7a059 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sigtomac.cpp @@ -0,0 +1,104 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Initiator authenticates itself using digital signatures + * while responder uses message authentication codes. + * Includes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)) +#define AUTHrr MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-sigtomac(I, R) +{ + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R,g(i),Gr,Ni,Nr ); + send_!3( I, R, SPIi, SPIr, {I, R, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, SPIi, SPIr, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, SPIi, SPIr, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, SPIi, SPIr, {I, R, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I,Gi,g(r),Ni,Nr ); + send_!4( R, I, SPIi, SPIr, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,g(r),Ni,Nr ); + } +} diff --git a/gui/Protocols/IKE/ikev2-sigtomac2.cpp b/gui/Protocols/IKE/ikev2-sigtomac2.cpp new file mode 100644 index 0000000..bccbab3 --- /dev/null +++ b/gui/Protocols/IKE/ikev2-sigtomac2.cpp @@ -0,0 +1,104 @@ +/********************************************************************** + * @protocol Internet Key Exchange Protocol (IKEv2) + * @reference RFC 4306 + * @variant Initiator authenticates itself using digital signatures + * while responder uses message authentication codes. + * Excludes optional payloads + **********************************************************************/ + +/** + * MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + */ + +#define __IKEV2__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define AUTHii {SPIi, O, SA1, g(i), Ni, Nr, prf(SKi, I)}sk(I) +#define AUTHir {SPIi, O, SA1, Gi, Ni, Nr, prf(SKr, I)}sk(I) +#define AUTHri MAC(k(I,R), SPIi, SPIr, SA1, Gr, Nr, Ni, prf(SKi, R)) +#define AUTHrr MAC(k(R,I), SPIi, SPIr, SA1, g(r), Nr, Ni, prf(SKr, R)) + + +usertype Number, SecurityAssociation, TrafficSelector; +const O: Number; +const SA1 ,SA2, SA3: SecurityAssociation; +const TSi, TSr: TrafficSelector; + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(E) { +#define Gi g(i) +#define Gr g(r) + role E { + var i, r, Ni, Nr, SPIi, SPIr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!E1( E, E, {I, AUTHii, SA2, TSi, TSr}SKi ); + send_!E2( E, E, {I, AUTHir, SA2, TSi, TSr}SKr ); + + // msg 4 + recv_!E3( E, E, {R, AUTHrr, SA2, TSi, TSr}SKr ); + send_!E4( E, E, {R, AUTHri, SA2, TSi, TSr}SKi ); + + } +#undef Gi +#undef Gr +} + + +protocol ikev2-sigtomac2(I, R) +{ + role I { + fresh i, Ni, SPIi: Nonce; + var Nr, SPIr: Nonce; + var Gr: Ticket; + + + /* IKE_SA_INIT */ + send_1( I, R, SPIi, O, SA1, g(i), Ni ); + recv_2( R, I, SPIi, SPIr, SA1, Gr, Nr ); + + /* IKE_AUTH */ + claim( I, Running, R,g(i),Gr,Ni,Nr ); + send_!3( I, R, SPIi, SPIr, {I, AUTHii, SA2, TSi, TSr}SKi ); + recv_!4( R, I, SPIi, SPIr, {R, AUTHri, SA2, TSi, TSr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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; + + + /* IKE_SA_INIT */ + recv_1( I, R, SPIi, O, SA1, Gi, Ni ); + send_2( R, I, SPIi, SPIr, SA1, g(r), Nr ); + + /* IKE_AUTH */ + recv_!3( I, R, SPIi, SPIr, {I, AUTHir, SA2, TSi, TSr}SKr ); + claim( R, Running, I,Gi,g(r),Ni,Nr ); + send_!4( R, I, SPIi, SPIr, {R, AUTHrr, SA2, TSi, TSr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + claim( R, Commit, I,Gi,g(r),Ni,Nr ); + } +} diff --git a/gui/Protocols/IKE/jfki-core.cpp b/gui/Protocols/IKE/jfki-core.cpp new file mode 100644 index 0000000..d6c2abf --- /dev/null +++ b/gui/Protocols/IKE/jfki-core.cpp @@ -0,0 +1,54 @@ +/** HEADDOC + * @protocol Just Fast Keying + * @reference Aiello et al., Just Fast Keying: Key Agreement In A Hostile + * Internet + * @description + * @variant Core cryptographic protocol of JFKi +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __JFK_CORE__ +#ifndef __ORACLE__ +#include "common.h" +#endif + + +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) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/jfki.cpp b/gui/Protocols/IKE/jfki.cpp new file mode 100644 index 0000000..5b000f9 --- /dev/null +++ b/gui/Protocols/IKE/jfki.cpp @@ -0,0 +1,84 @@ +/** HEADDOC + * @protocol Just Fast Keying + * @reference Aiello et al., Just Fast Keying: Key Agreement In A Hostile + * Internet + * @description + * @variant Initiatior is identity protected +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __JFK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, SAi, SAr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!O1( O, O, {I, SAi, {H(Ni), Nr, g(i), Gr, R, SAi}sk(I)}SKi ); + send_!O2( O, O, {I, SAi, {H(Ni), Nr, g(i), Gr, R, SAi}sk(I)}SKr ); + + // msg 4 + recv_!O3( O, O, {{H(Ni), Nr, g(i), Gr, I, SAi, SAr}sk(R), SAr}SKr ); + send_!O4( O, O, {{H(Ni), Nr, g(i), Gr, I, SAi, SAr}sk(R), SAr}SKi ); + + } +#undef Gi +#undef Gr +} + + +// Abstractions: no grpinfo, no MAC(ENC(M)), no ID_R', no IPi +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)}SKi ); + recv_!4( R, I, {{H(Ni), Nr, g(i), Gr, I, SAi, SAr}sk(R), SAr}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + // Note: if R can receive H(HKr, g(r), Nr, H(Ni)) then HNi=H(Ni) + 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)}SKr ); + send_!4( R, I, {{H(Ni), Nr, Gi, g(r), I, SAi, SAr}sk(R), SAr}SKr ); + + /* SECURITY CLAIMS */ + claim( R, Secret, HKr ); + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/jfkr-core.cpp b/gui/Protocols/IKE/jfkr-core.cpp new file mode 100644 index 0000000..500a8bb --- /dev/null +++ b/gui/Protocols/IKE/jfkr-core.cpp @@ -0,0 +1,78 @@ +/** HEADDOC + * @protocol Just Fast Keying + * @reference Aiello et al., Just Fast Keying: Key Agreement In A Hostile + * Internet + * @description + * @variant Core cryptographic protocol of JFKr +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __JFK_CORE__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!O1( O, O, H(SKr, Nr, Ni, R) ); + send_!O2( O, O, H(SKi, Nr, Ni, R) ); + + // msg 4 + recv_!O3( O, O, H(SKi, Nr, Ni, I) ); + send_!O4( O, O, H(SKr, Nr, Ni, I) ); + + } +#undef Gi +#undef Gr +} + + +// Abstractions: same key for ENC, MAC +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(SKi, Nr, Ni, R) ); + send_!3( I, R, Nr, Ni, I, {Nr, Ni, Gr, g(i)}sk(I), H(SKi, Nr, Ni, I) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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(SKr, Nr, Ni, R) ); + recv_!3( I, R, Nr, Ni, I, {Nr, Ni, g(r), Gi}sk(I), H(SKr, Nr, Ni, I) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/jfkr.cpp b/gui/Protocols/IKE/jfkr.cpp new file mode 100644 index 0000000..fbe85d3 --- /dev/null +++ b/gui/Protocols/IKE/jfkr.cpp @@ -0,0 +1,83 @@ +/** HEADDOC + * @protocol Just Fast Keying + * @reference Aiello et al., Just Fast Keying: Key Agreement In A Hostile + * Internet + * @description + * @variant Responder is identity protected +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __JFK__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, SAi, SAr: Nonce; + var I, R: Agent; + + // msg 3 + recv_!O1( O, O, {I, SAi, {H(Ni), Nr, g(i), Gr}sk(I)}SKi ); + send_!O2( O, O, {I, SAi, {H(Ni), Nr, g(i), Gr}sk(I)}SKr ); + + // msg 4 + recv_!O3( O, O, {R, SAr, {Gr, Nr, g(i), H(Ni)}sk(R)}SKr ); + send_!O4( O, O, {R, SAr, {Gr, Nr, g(i), H(Ni)}sk(R)}SKi ); + + } +#undef Gi +#undef Gr +} + + +// Abstractions: no grpinfo, no MAC(ENC(M)), no ID_R', no IPi +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)}SKi ); + recv_!4( R, I, {R, SAr, {Gr, Nr, g(i), H(Ni)}sk(R)}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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)}SKr ); + send_!4( R, I, {R, SAr, {g(r), Nr, Gi, H(Ni)}sk(R)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, Secret, HKr ); + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/make-mpa.py b/gui/Protocols/IKE/make-mpa.py new file mode 100755 index 0000000..c75984d --- /dev/null +++ b/gui/Protocols/IKE/make-mpa.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python + +import os + +def getProtocolFiles(path=".",extension=""): + allfiles = os.listdir(path) + spfl = [] + for fn in allfiles: + if fn.endswith(extension): + spfl.append(fn) + return spfl + +def scanThis(fn,f,rewritelist,cnt): + + s = "" + mapping = [] + for lhs in rewritelist: + rhs = "%s%i" % (lhs,cnt) + mapping.append((lhs,rhs)) + + fp = open(fn,"r") + for rl in fp.xreadlines(): + l = rl + if f != None: + l = f(l) + for (lhs,rhs) in mapping: + l = l.replace(lhs,rhs) + s = s + l + fp.close() + return s + +def convertEm(f=None,path=".",rewritelist=[],newdir=".",oldext="",newext=None): + fl = getProtocolFiles(path=path,extension=oldext) + cnt = 1 + for fn in fl: + ffn = os.path.join(path,fn) + print "Processing",ffn + s = scanThis(ffn,f,rewritelist,cnt) + if newext == None: + fn2 = fn + else: + fn2 = fn.replace(oldext,newext) + ffn2 = os.path.join(newdir,fn2) + fp = open(ffn2,"w") + fp.write(s) + fp.close() + print "Produced",ffn2 + cnt = cnt+1 + +def preprocess(s): + s = s.replace("@oracle","@OracleA") + s = s.replace("@ora ", "@OracleB ") + s = s.replace("@ora(", "@OracleB(") + return s + +def main(): + convertEm(f=preprocess,rewritelist=["@OracleA","@executability","@OracleB"],path=".",newdir="mpa",oldext=".spdl") + print "Done." + +if __name__ == '__main__': + main() + + diff --git a/gui/Protocols/IKE/mpa/README.txt b/gui/Protocols/IKE/mpa/README.txt new file mode 100644 index 0000000..91e5266 --- /dev/null +++ b/gui/Protocols/IKE/mpa/README.txt @@ -0,0 +1,6 @@ +This directory is filled by the script + +`../make-mpa.py` + +It takes the `.spdl` files from the `..` directory and prepares them for +multi-protocol analysis. diff --git a/gui/Protocols/IKE/oakley-a.cpp b/gui/Protocols/IKE/oakley-a.cpp new file mode 100644 index 0000000..84db6b0 --- /dev/null +++ b/gui/Protocols/IKE/oakley-a.cpp @@ -0,0 +1,60 @@ +/** + * @protocol OAKLEY + * @reference RFC 2412, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description OAKLEY is related to STS and allows for shared key + * determination via authenticated Diffie-Hellman exchanges and + * provides perfect forward secrecy for the shared key. + * @variant Aggressive mode +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __OAKLEY__ +#ifndef __ORACLE__ +#include "common.h" +#endif + + +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) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/oakley-alt.cpp b/gui/Protocols/IKE/oakley-alt.cpp new file mode 100644 index 0000000..5c4654f --- /dev/null +++ b/gui/Protocols/IKE/oakley-alt.cpp @@ -0,0 +1,63 @@ +/** HEADDOC + * @protocol OAKLEY + * @reference RFC 2412, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description OAKLEY is related to STS and allows for shared key + * determination via authenticated Diffie-Hellman exchanges and + * provides perfect forward secrecy for the shared key. + * @variant Alternative variant to prevent user identity disclosure +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __OAKLEY__ +#ifndef __ORACLE__ +#include "common.h" +#endif +#define AK prf(Ni,Nr) + + +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; + + // NOTE: pk(R) is sent in plain so that the recipient knows which decryption key to use + // In the specification, there is a distinction between the R in pk(R) and the encrypted R + 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(AK, R, I, Gr, g(i), algo) ); + send_3( I, R, Ci, Cr, prf(AK, I, R, g(i), Gr, algo) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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(AK, R, I, g(r), Gi, algo) ); + recv_3( I, R, Ci, Cr, prf(AK, I, R, Gi, g(r), algo) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/oakley-c.cpp b/gui/Protocols/IKE/oakley-c.cpp new file mode 100644 index 0000000..32e6a80 --- /dev/null +++ b/gui/Protocols/IKE/oakley-c.cpp @@ -0,0 +1,105 @@ +/** HEADDOC + * @protocol OAKLEY + * @reference RFC 2412, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description OAKLEY is related to STS and allows for shared key + * determination via authenticated Diffie-Hellman exchanges and + * provides perfect forward secrecy for the shared key. + * @variant Conservative mode with identity hiding +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __OAKLEY_CONSERVATIVE__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +#define Kpi prf(Zi) +#define Kpr prf(Zr) +#define Kir prf(Ni,Nr) + + +usertype String; +const OK, list, algo: String; + + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r, Ni, Nr, Ci, Cr: Nonce; + var I, R: Agent; + + // msg 5 + recv_!O1( O, O, {I, R, {Ni}pk(R)}Kpi ); + send_!O2( O, O, {I, R, {Ni}pk(R)}Kpr ); + + // msg 6 + recv_!O3( O, O, {{Nr, Ni}pk(I), R, I, prf(Kir, R, I, Gr, g(i), algo)}Kpr ); + send_!O4( O, O, {{Nr, Ni}pk(I), R, I, prf(Kir, R, I, Gr, g(i), algo)}Kpi ); + + // msg 7 + recv_!O5( O, O, {prf(Kir, I, R, g(i), Gr, algo)}Kpi ); + send_!O6( O, O, {prf(Kir, I, R, g(i), Gr, algo)}Kpr ); + + } +#undef Gi +#undef Gr +} + + +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)}Kpi ); + recv_!6( R, I, Cr, Ci, {{Nr, Ni}pk(I), R, I, prf(Kir, R, I, Gr, g(i), algo)}Kpi ); + send_!7( I, R, Ci, Cr, {prf(Kir, I, R, g(i), Gr, algo)}Kpi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, Kpi ); + claim( I, SKR, SKi ); + + 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)}Kpr ); + send_!6( R, I, Cr, Ci, {{Nr, Ni}pk(I), R, I, prf(Kir, R, I, g(r), Gi, algo)}Kpr ); + recv_!7( I, R, Ci, Cr, {prf(Kir, I, R, Gi, g(r), algo)}Kpr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, Kpr ); + + claim( R, SKR, SKr ); + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/pp.sh b/gui/Protocols/IKE/pp.sh new file mode 100755 index 0000000..1ee7b6e --- /dev/null +++ b/gui/Protocols/IKE/pp.sh @@ -0,0 +1,21 @@ +#!/bin/sh + +FILES="$*" +EXT="pp" +#OUT=. +OUT=pp-results + +if [ -n "$FILES" ]; then + for file in $FILES; + do + if [ "$file" = "*.$EXT.*" ]; then + echo "skipping $file" + else + echo "preprocessing $file" + cpp $file | sed -e '/^(\#.*)*$/d' > $OUT/${file%%.*}.$EXT.spdl + fi + done +else + printf "Usage: %s: file...\n" $(basename $0) >&2 + exit 1 +fi diff --git a/gui/Protocols/IKE/scanner.py b/gui/Protocols/IKE/scanner.py new file mode 100755 index 0000000..bc529ac --- /dev/null +++ b/gui/Protocols/IKE/scanner.py @@ -0,0 +1,800 @@ +#!/usr/bin/env python + +import sys + +ALLPROTS = set() +ALLCLAIMS = set() # prot x role x claim +PREFIX = None # Required prefix +FFUNC = (lambda p: True) # Filter function + +def reset(): + + global ALLPROTS + global ALLCLAIMS + global PREFIX + global FFUNC + + ALLPROTS = set() + ALLCLAIMS = set() + PREFIX = None + FFUNC = (lambda p: True) + +def skipLine(l): + if len(l) == 0: + return True + + skippable = ["%","\\begin","\\end","Protocol"] + for skstr in skippable: + if l.startswith(skstr): + return True + + return False + +def stripRowEnd(l): + # Assume ends with \\, split by dtl + endstr = "\\\\" + if not l.endswith(endstr): + print "Error: some line does not end with \\\\" + print ">>%s<<" % (l) + sys.exit(-1) + + return l[:-len(endstr)] + +def splitStrip(l,sp): + + dtl = l.split(sp) + for i in range(0,len(dtl)): + dtl[i] = dtl[i].strip() + return dtl + +def roleClaim(dtl): + rcdt = dtl.split() + assert(rcdt[0].endswith(":")) + role = rcdt[0][:-1] + claim = rcdt[1] + return (role,claim[:20]) + +def scanAttackFile(fn): + + global ALLPROTS + + fp = open("gen-%s-mpaattacks.tex" % (fn),"r") + attackmap = {} + prot = None + role = None + claim = None + for rawline in fp.xreadlines(): + + l = rawline.strip() + + if skipLine(l): + continue + + l = stripRowEnd(l) + + dtl = splitStrip(l,"&") + + # New protocol + if len(dtl[0]) > 0: + prot = dtl[0] + + # New role + if len(dtl[1]) > 0: + (role,claim) = roleClaim(dtl[1]) + + # Claims list + # Assume starts with '[' and ends with ']' + assert(dtl[2].startswith("[")) + assert(dtl[2].endswith("]")) + attl = ((dtl[2])[1:-1]).split(",") + for i in range(0,len(attl)): + x = attl[i].strip() + assert(x.startswith("'")) + assert(x.endswith("'")) + attl[i] = x[1:-1] + + ak = (prot,role,claim) + if ak not in attackmap.keys(): + attackmap[ak] = set() + attackmap[ak].add(tuple(attl)) + + # Add to allprots set + ALLPROTS.add(prot) + for p in attl: + ALLPROTS.add(prot) + + fp.close() + + return attackmap + + +def shorten(prot): + """ + Shorten protocol name + """ + cutting = ["isoiec-","9798-"] + for ct in cutting: + if prot.startswith(ct): + prot = prot[len(ct):] + return prot.replace("-udkey","-ud") + + +def prettyclaim(cl): + """ + Rewrite if needed + """ + return cl.replace("Commit","Agreement") + + +def mpaTable(attackmap): + """ + construct table for MPA attacks + """ + counter = 1 + s = "" + + s += "\\begin{longtable}{|l|lll|l|}\n" + s += "\\hline\n" + for kk in sorted(ALLCLAIMS): + if kk not in attackmap.keys(): + continue + (prot,role,claim) = kk + + ats = str(attackmap[kk]) + sl = "%i & %s & %s & %s & %s \\\\ \n" % (counter,prot,role,claim,ats) + + s += sl + counter = counter + 1 + + s += "\\hline\n" + s += "\\end{longtable}\n" + + return s + + +def rotated(headl): + """ + Add rotated headers + """ + for i in range(0,len(headl)): + headl[i] = "\\begin{sideways} %s \\end{sideways}\n" % (headl[i]) + return " & ".join(headl) + + +def baseprot(prot): + return shorten(prot)[:5] + + +def mpaTable2(attackmap,tabtype="tabular",options=""): + """ + construct table for MPA attacks + + Second attempt + """ + + # To find the number of columns, we first need to find all protocols involved in two-protocol attacks + involved = set() + for kk in attackmap.keys(): + for atl in attackmap[kk]: + # convert tuple back to list + att = list(atl) + if len(att) == 1: + # This attack involves one *additional* protocol, so is a two-protocol attack + involved.add(att[0]) + colheads = sorted(involved) + attcols = "" + last = None + for hd in colheads: + prm = baseprot(hd) + if last == prm: + attcols += "@{\hspace{2mm}}c" + else: + last = prm + attcols += "|c" + + + #attcols = "c" * len(involved) + + counter = 1 + s = "" + + #s += "\\clearpage \n" + + s += "\\begin{%s}%s{|l|ll|%s|}\n" % (tabtype,options,attcols) + s += "\\hline\n" + s += rotated(["No","Prot","Claim"]) + for hd in colheads: + s += "& \\begin{sideways}%s\\end{sideways} " % (shorten(hd)) + s += "\\\\ \n" + + s += "\\hline\n" + last = None + for kk in sorted(ALLCLAIMS): + if kk not in attackmap.keys(): + continue + (prot,role,claim) = kk + + prm = baseprot(prot) + if last != prm: + last = prm + s += "\\hline\n" + + sl = "" + sl += "%i & %s & %s %s " % (counter,shorten(prot),role,claim) + for ch in colheads: + se = tuple([ch]) + if se in attackmap[kk]: + sl += "& $\\bullet$ " + else: + sl += "& $\\circ$ " + + sl += "\\\\ \n" + + s += sl + counter = counter + 1 + + s += "\\hline\n" + s += "\\end{%s}\n" % (tabtype) + + return s + + +def mpaTable3(attackmaps,tabtype="tabular",options=""): + """ + construct table for MPA attacks + + attmaps = sequence of (attackmap, symbol) + + Symbol of the first matching is displayed + + Second attempt + """ + + global FFUNC + # To find the number of columns, we first need to find all protocols involved in two-protocol attacks + # Also populate "allkeys" + involved = set() + allkeys = set() + for (attackmap,symbs) in attackmaps: + for kk in attackmap.keys(): + allkeys.add(kk) + for atl in attackmap[kk]: + # convert tuple back to list + att = list(atl) + if len(att) == 1: + # This attack involves one *additional* protocol, so is a two-protocol attack + if FFUNC: + if not FFUNC(att[0]): + continue + + involved.add(att[0]) + + colheads = sorted(involved) + attcols = "" + last = None + for hd in colheads: + prm = baseprot(hd) + if last == prm: + attcols += "@{\hspace{2mm}}c" + else: + last = prm + attcols += "|c" + + + #attcols = "c" * len(involved) + + counter = 1 + s = "" + + #s += "\\clearpage \n" + + s += "\\begin{%s}%s{|l|ll|%s|}\n" % (tabtype,options,attcols) + s += "\\hline\n" + s += rotated(["No","Prot","Claim"]) + for hd in colheads: + s += "& \\begin{sideways}%s\\end{sideways} " % (shorten(hd)) + s += "\\\\ \n" + + s += "\\hline\n" + last = None + for kk in sorted(ALLCLAIMS): + if kk not in attackmap.keys(): + continue + (prot,role,claim) = kk + + prm = baseprot(prot) + if last != prm: + last = prm + s += "\\hline\n" + + sl = "" + sl += "%i & %s & %s %s " % (counter,shorten(prot),role,prettyclaim(claim)) + for ch in colheads: + se = tuple([ch]) + sl += "& " + for (attackmap,symb) in attackmaps: + if kk in attackmap.keys(): + if se in attackmap[kk]: + sl += symb + break + + sl += "\\\\ \n" + + s += sl + counter = counter + 1 + + s += "\\hline\n" + s += "\\end{%s}\n" % (tabtype) + + return s + + +def scanClaimList(fn): + """ + Simply gather claims + """ + + global ALLPROTS + global ALLCLAIMS + global FFUNC + + fp = open("gen-%s-claims.txt" % (fn),"r") + + claimmap = {} + for rawline in fp.xreadlines(): + + l = rawline.strip() + + if skipLine(l): + continue + + dtl = splitStrip(l,"; ") + + filename = dtl[0] + prot = dtl[1] + if FFUNC: + if not FFUNC(prot): + continue + + label = dtl[2] + (role,claim) = roleClaim(dtl[3]) + + ALLCLAIMS.add((prot,role,claim)) + ALLPROTS.add(prot) + + fp.close() + + return claimmap + +def scanClaimFile(fn): + """ + Construct claimmap + + prot -> roles -> claims + """ + + global ALLPROTS + global ALLCLAIMS + global FFUNC + + fp = open("gen-%s-correctclaims.tex" % (fn),"r") + + claimmap = {} + for rawline in fp.xreadlines(): + + l = rawline.strip() + + if skipLine(l): + continue + + l = stripRowEnd(l) + + dtl = splitStrip(l,"&") + + prot = dtl[0] + if FFUNC: + if not FFUNC(prot): + continue + + if prot not in claimmap.keys(): + claimmap[prot] = {} + + cll = splitStrip(dtl[1],";") + + for dt in cll: + (role,claim) = roleClaim(dt) + + if role not in claimmap[prot].keys(): + claimmap[prot][role] = set() + + claimmap[prot][role].add(claim) + + ALLCLAIMS.add((prot,role,claim)) + + ALLPROTS.add(prot) + + fp.close() + + return claimmap + +def getRoleClaims(rcmap): + + rc = set() + for role in rcmap.keys(): + for claim in rcmap[role]: + rc.add((role,claim)) + + return rc + +def typeScanMatrix(cml,onlyChanged = False): + + global ALLPROTS + + """ + Scan for the influence of typing. + + Input: + + [(txt1,cm1),(txt2,cm2),...] + + """ + s = "" + + s += "\\begin{longtable}{|l|lll|%s|}\n" % ("c" * len(cml)) + s += "\\hline\n" + + s += "No & Prot & Role & Claim " + for (txt,cm) in cml: + s += "& %s " % (txt) + s += "\\\\\n" + s += "\\hline\n" + + goodverdict = "$\\circ$" + badverdict = "$\\bullet$" + + counter = 1 + for (prot,role,claim) in sorted(ALLCLAIMS): + # Header + sl = "%i & %s & %s & %s " % (counter,prot,role,claim) + alltrue = True + for (txt,cm) in cml: + verdict = badverdict + if prot in cm.keys(): + if role in cm[prot].keys(): + if claim in cm[prot][role]: + verdict = goodverdict + if verdict == badverdict: + alltrue = False + + sl += "& %s " % (verdict) + sl += "\\\\\n" + + if alltrue == True: + if onlyChanged == True: + continue + + s += sl + counter = counter + 1 + + s += "\\hline\n" + s += "\\end{longtable}\n" + return s + +def typeScanMatrix2(cml,onlyChanged = False,additive = False): + + global ALLPROTS + + """ + Scan for the influence of typing. + + Input: + + [(txt1,cm1),(txt2,cm2),...] + + """ + s = "" + + s += "\\begin{longtable}{|l|lll||c|}\n" + s += "\\hline\n" + + s += "No & Prot & Claim & Attacks" + s += "\\\\\n" + s += "\\hline\n" + s += "\\hline\n" + + goodverdict = "$\\circ$" + badverdict = "$\\bullet$" + + last = None + counter = 1 + for (prot,role,claim) in sorted(ALLCLAIMS): + if baseprot(prot) != last: + last = baseprot(prot) + s += "\\hline\n" + + # Header + sl = "%i & %s & %s %s " % (counter,prot,role,prettyclaim(claim)) + alltrue = True + res = "" + for (txt,cm) in cml: + verdict = badverdict + if prot in cm.keys(): + if role in cm[prot].keys(): + if claim in cm[prot][role]: + verdict = goodverdict + if verdict == badverdict: + alltrue = False + if additive: + res += txt + else: + res = txt + + sl += "& %s " % (res) + sl += "\\\\\n" + + if alltrue == True: + if onlyChanged == True: + continue + + s += sl + counter = counter + 1 + + s += "\\hline\n" + s += "\\end{longtable}\n" + return s + +def typeScanMatrix3(hd1,hd2,cml,f,onlyChanged = False,tabletype="longtable"): + + global ALLPROTS + + """ + Scan for the influence of typing. + + Input: + + f is given as input a sequence of Bool (attack = False) of length len(cml), should return string. + + """ + s = "" + + s += "\\begin{%s}{|l|ll||%s|}\n" % (tabletype,hd1) + s += "\\hline\n" + + s += rotated(["No","Protocol","Claim"]) + " & " + rotated(hd2) + s += "\\\\\n" + s += "\\hline\n" + s += "\\hline\n" + + goodverdict = "$\\circ$" + badverdict = "$\\bullet$" + + last = None + counter = 1 + for (prot,role,claim) in sorted(ALLCLAIMS): + if baseprot(prot) != last: + last = baseprot(prot) + s += "\\hline\n" + + # Header + sl = "%i & %s & %s %s " % (counter,prot,role,prettyclaim(claim)) + alltrue = True + res = "" + resl = [] + for cm in cml: + verdict = badverdict + if prot in cm.keys(): + if role in cm[prot].keys(): + if claim in cm[prot][role]: + verdict = goodverdict + if verdict == badverdict: + alltrue = False + resl.append(False) + else: + resl.append(True) + + sl += "& %s " % (f(resl)) + sl += "\\\\\n" + + if alltrue == True: + if onlyChanged == True: + continue + + s += sl + counter = counter + 1 + + s += "\\hline\n" + s += "\\end{%s}\n" % (tabletype) + return s + +def docWrapper(s,title=None,author=None): + + pref = "" + pref += "\\documentclass{article}\n" + pref += "\\usepackage{a4}\n" + pref += "\\usepackage{geometry}\n" + pref += "\\usepackage{longtable}\n" + pref += "\\usepackage{rotating}\n" + pref += "\\begin{document}\n" + if title or author: + if title: + pref += "\\title{%s}\n" % (title) + if author: + pref += "\\author{%s}\n" % (author) + pref += "\\maketitle\n" + post = "" + post += "\\end{document}\n" + + return pref + s + post + +def secWrapper(s,title,level=0): + """ + level : + + 0 section + 1 subsection + 2 subsub... + """ + pref = "\\" + "sub" * level + "section{" + title + "}\n\n" + post = "\n" + return pref + s + post + + +def sizeWrapper(s, width="!", height="!"): + + if (width != "!") or (height != "!"): + s = "\\resizebox{%s}{%s}{ \n%s}\n" % (width,height,s) + return s + + +def fileWrite(fn,s): + + fp = open("%s.tex" % (fn), "w") + fp.write(s) + fp.close() + + +def docWrite(fn,tex,author=None,title=None): + + fileWrite(fn, docWrapper(tex,author=author,title=title)) + + +def docMake(fn,tex,author=None,title=None): + + import commands + + docWrite(fn,tex,author,title) + cmd = "pdflatex %s" % (fn) + commands.getoutput(cmd) + +def f1(resl): + txtl = [] + for t in resl: + if t == True: + txtl.append(" ") + else: + txtl.append("$\\bullet$") + return " & ".join(txtl) + +def pb(tl,width): + nl = [] + for t in tl: + nl.append("\\parbox{%s}{%s}" % (width,t)) + return nl + +def makeReport(fn,includefiles=False): + scanClaimList(fn + "-aa-t") + + cISOaat = scanClaimFile(fn + "-aa-t") + cISOaab = scanClaimFile(fn + "-aa-b") + cISOaau = scanClaimFile(fn + "-aa-u") + cISOiut = scanClaimFile(fn + "-iu-t") + cISOiub = scanClaimFile(fn + "-iu-b") + cISOiuu = scanClaimFile(fn + "-iu-u") + cISOext = scanClaimFile(fn + "-ex-t") + cISOexb = scanClaimFile(fn + "-ex-b") + cISOexu = scanClaimFile(fn + "-ex-u") + + tex = "" + #tex += secWrapper(typeScanMatrix([("typed",cISOaat),("basic",cISOaab),("untyped",cISOaau)],onlyChanged = False),title="Normal mode (Alice-Alice communication allowed)") + #tex += secWrapper(typeScanMatrix([("typed",cISOiut),("basic",cISOiub),("untyped",cISOiuu)],onlyChanged = True),title="Disallow Alice-Alice initiators") + #tex += secWrapper(typeScanMatrix([("typed",cISOext),("basic",cISOexb),("untyped",cISOexu)],onlyChanged = True),title="Disallow Alice-Alice communications") + + orders = [cISOaab, + cISOaat, + cISOiub, + cISOiut] + + sectex = typeScanMatrix3("c|c|c|c",pb(["No type checks\\\\Alice-talks-to-Alice initators","Type checks\\\\Alice-talks-to-Alice initators","No type checks\\\\No Alice-talks-to-Alice initators","Type checks\\\\No Alice-talks-to-Alice initators"],"49mm"), orders,f1,onlyChanged = True) + + mpatex = sizeWrapper(mpaTable3([ + (scanAttackFile(fn + "-ex-t"),"$\\bullet$"), + (scanAttackFile(fn + "-aa-b"),"$\\circ$") + ]),width="\\textwidth") + + if includefiles == True: + fileWrite("../gen-att-" + fn,sectex) + fileWrite("../gen-mpa-" + fn,mpatex) + + tex += secWrapper(sectex,title="Attacks found") + tex += secWrapper(mpatex,title="MPA attacks") + docMake(fn,tex,author="Cas Cremers",title="test report %s" % (fn)) + + +def filterPrefix(prot): + """ + Returns true iff the protocol name is okay to be considered + """ + if PREFIX: + if not prot.startswith(PREFIX): + return False + return True + +def filterPrefixBD(prot): + """ + Returns true iff the protocol name is okay to be considered + """ + if PREFIX: + if not prot.startswith(PREFIX): + return False + if prot.endswith("-ud"): + return False + if prot.endswith("-udkey"): + return False + return True + + +def filterCombo(prot): + """ + Returns true iff the protocol name is okay to be considered + """ + if prot.find("-sig-child") >= 0: + return False + + return True + + +def filterISOsymmBD(prot): + """ + Returns true iff the protocol name is okay to be considered + """ + if prot.endswith("-ud"): + return False + if prot.endswith("-udkey"): + return False + + if prot.startswith("isoiec-9798-2"): + return True + if prot.startswith("isoiec-9798-4"): + return True + + return False + + + +if __name__ == "__main__": + + #reset() + #PREFIX = "isoiec-9798-2" + #makeReport(PREFIX) + + includefiles = True + + reset() + FFUNC = filterCombo + PREFIX = "ike1" + makeReport(PREFIX,includefiles=includefiles) + + reset() + FFUNC = filterCombo + PREFIX = "ike2" + makeReport(PREFIX,includefiles=includefiles) + + reset() + FFUNC = filterCombo + PREFIX = "ike0" + makeReport(PREFIX,includefiles=includefiles) + + + + + diff --git a/gui/Protocols/IKE/skeme-basic.cpp b/gui/Protocols/IKE/skeme-basic.cpp new file mode 100644 index 0000000..d9f58ab --- /dev/null +++ b/gui/Protocols/IKE/skeme-basic.cpp @@ -0,0 +1,61 @@ +/** HEADDOC + * @protocol SKEME + * @reference Krawczyk, H., SKEME: A Versatile Secure Key Exchange Mechanism + * for Internet, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description SKEME is a set of protocols suitable for negotiation of + * services in a general networked environment. The main + * characteristics are forward secrecy, privacy and anonymity, + * and DoS protection. + * @variant Basic mode +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther + * Note: May use the same oracles as sts +**/ +#define __SKEME__ +#ifndef __ORACLE__ +#include "common.h" +#endif +#define Kir prf(Ni,Nr) + + +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(Kir, g(i), Gr, R, I) ); + send_3( I, R, prf(Kir, Gr, g(i), I, R) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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(Kir, Gi, g(r), R, I) ); + recv_3( I, R, prf(Kir, g(r), Gi, I, R) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/skeme-psk.cpp b/gui/Protocols/IKE/skeme-psk.cpp new file mode 100644 index 0000000..355edc2 --- /dev/null +++ b/gui/Protocols/IKE/skeme-psk.cpp @@ -0,0 +1,82 @@ +/** HEADDOC + * @protocol SKEME + * @reference Krawczyk, H., SKEME: A Versatile Secure Key Exchange Mechanism + * for Internet, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description SKEME is a set of protocols suitable for negotiation of + * services in a general networked environment. The main + * characteristics are forward secrecy, privacy and anonymity, + * and DoS protection. + * @variant Basic mode with pre-shared keys and correct application of DH +**/ + + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __SKEME__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling k(I,R) = k(R,I). + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, prf(k(R,I), Gi, g(r), R, I) ); + send_!O2( O, O, prf(k(I,R), Gi, g(r), R, I) ); + + // msg 3 + recv_!O3( O, O, prf(k(I,R), Gr, g(i), I, R) ); + send_!O4( O, O, prf(k(R,I), Gr, g(i), I, R) ); + + } +#undef Gi +#undef Gr +} + + +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) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/skeme-rekey.cpp b/gui/Protocols/IKE/skeme-rekey.cpp new file mode 100644 index 0000000..a1915a2 --- /dev/null +++ b/gui/Protocols/IKE/skeme-rekey.cpp @@ -0,0 +1,80 @@ +/** HEADDOC + * @protocol SKEME + * @reference Krawczyk, H., SKEME: A Versatile Secure Key Exchange Mechanism + * for Internet, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description SKEME is a set of protocols suitable for negotiation of + * services in a general networked environment. The main + * characteristics are forward secrecy, privacy and anonymity, + * and DoS protection. + * @variant Fast rekeying protocol +**/ + +/** MACRO DEFINITIONS + * Needs preprocessing by cpp before fed to scyther +**/ +#define __SKEME_REKEY__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling k(I,R) = k(R,I). + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var Ni, Nr: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, prf(k(R,I), Ni, Nr, R, I) ); + send_!O2( O, O, prf(k(I,R), Ni, Nr, R, I) ); + + // msg 3 + recv_!O3( O, O, prf(k(I,R), Nr, Ni, I, R) ); + send_!O4( O, O, prf(k(R,I), Nr, Ni, I, R) ); + + } +#undef Gi +#undef Gr +} + +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) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/sts-mac.cpp b/gui/Protocols/IKE/sts-mac.cpp new file mode 100644 index 0000000..9faaf4f --- /dev/null +++ b/gui/Protocols/IKE/sts-mac.cpp @@ -0,0 +1,78 @@ +/** HEADDOC + * @protocol Station-to-Station Protocol (STS) + * @reference Diffie W., van Oorschot P. C., and Wiener M. J., + * Authentication and authenticated key exchange, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description STS adds a diGital signaure to the exchanged messages to + * provide authentication for the Diffie-Hellman protocol. In + * addition, the shared secret is used to provide further + * assurances. + * @variant Variant using MACs +**/ + +#define __STS__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r: Nonce; + + // msg 2 + recv_!O1( O, O, MAC(Zr, g(r), Gi) ); + send_!O2( O, O, MAC(Zi, g(r), Gi) ); + + // msg 3 + recv_!O3( O, O, MAC(Zi, Gi, g(r)) ); + send_!O4( O, O, MAC(Zr, Gi, g(r)) ); + + } +#undef Gi +#undef Gr +} + +// It is not specified how the session key is derived from the ephemeral DH +// secret Z; we use KDF(Z). +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(Zi, Gr, g(i)) ); + send_!3( I, R, {g(i), Gr}sk(I), MAC(Zi, g(i), Gr) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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(Zr, g(r), Gi) ); + recv_!3( I, R, {Gi, g(r)}sk(I), MAC(Zr, Gi, g(r)) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/sts-main.cpp b/gui/Protocols/IKE/sts-main.cpp new file mode 100644 index 0000000..b95d306 --- /dev/null +++ b/gui/Protocols/IKE/sts-main.cpp @@ -0,0 +1,79 @@ +/** HEADDOC + * @protocol Station-to-Station Protocol (STS) + * @reference Diffie W., van Oorschot P. C., and Wiener M. J., + * Authentication and authenticated key exchange, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description STS adds a digital signaure to the exchanged messages to + * provide authentication for the Diffie-Hellman protocol. In + * addition, the shared secret is used to provide further + * assurances. +**/ + +#define __STS__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +/** + * This role serves as an "oracle" to ensure the executability of the + * protocol by taking care of the problems that arise from our way of + * modelling Diffie-Hellman keys. + */ +protocol @executability(O) { +#define Gi g(i) +#define Gr g(r) + role O { + var i, r: Nonce; + var I, R: Agent; + + // msg 2 + recv_!O1( O, O, {{g(r), Gi}sk(R)}SKr ); + send_!O2( O, O, {{g(r), Gi}sk(R)}SKi ); + + // msg 3 + recv_!O3( O, O, {{g(i), Gr}sk(I)}SKi ); + send_!O4( O, O, {{g(i), Gr}sk(I)}SKr ); + + } +#undef Gi +#undef Gr +} + + +// It is not specified how the session key is derived from the ephemeral DH +// secret Z; we use KDF(Z). +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)}SKi ); + send_!3( I, R, {{g(i), Gr}sk(I)}SKi ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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)}SKr ); + recv_!3( I, R, {{Gi, g(r)}sk(I)}SKr ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/sts-modified.cpp b/gui/Protocols/IKE/sts-modified.cpp new file mode 100644 index 0000000..458a042 --- /dev/null +++ b/gui/Protocols/IKE/sts-modified.cpp @@ -0,0 +1,55 @@ +/** HEADDOC + * @protocol Station-to-Station Protocol (STS) + * @reference Diffie W., van Oorschot P. C., and Wiener M. J., + * Authentication and authenticated key exchange, + * Boyd C. and Mathuria A., Protocols for Authentication and + * Key Agreement + * @description STS adds a diGital signaure to the exchanged messages to + * provide authentication for the Diffie-Hellman protocol. In + * addition, the shared secret is used to provide further + * assurances. + * @variant Variant proposed by Boyd et al to prevent unknown key-share + * attacks. +**/ + +#define __STS__ +#ifndef __ORACLE__ +#include "common.h" +#endif + +// It is not specified how the session key is derived from the ephemeral DH +// secret Z; we use KDF(Z). +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) ); + + /* SECURITY CLAIMS */ + claim( I, SKR, SKi ); + + 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) ); + + /* SECURITY CLAIMS */ + claim( R, SKR, SKr ); + + claim( R, Alive ); + claim( R, Weakagree ); + + } +} \ No newline at end of file diff --git a/gui/Protocols/IKE/verify.sh b/gui/Protocols/IKE/verify.sh new file mode 100755 index 0000000..44f2b61 --- /dev/null +++ b/gui/Protocols/IKE/verify.sh @@ -0,0 +1,149 @@ +############################################################################# +# +# NAME +# verify - batch protocol verifier script for scyther +# +# SYNOPSIS +# ./verify.sh [option]... [file]... +# +# DESCRIPTION +# Verify protocol specifications using scyther. +# +# OPTIONS +# +# -d Debug mode [false] +# -e Execution environment [cluster] +# -h Help +# -i Skip attack patterns of the form Alice talking to Alice +# -l lower bound of claims to check [1] +# -m Adversary-compromise model [ext] +# -o Output directory (attack graphs) [./graphs/] +# -r number of runs [6] +# -t timeout in s +# -u upper bound of claims to check [1] +# +# EXAMPLE +# ./verify.sh -m br -o . *.spdl +# +############################################################################# + + +#!/bin/bash + +# Default values +CLAIM[0]=1 +CLAIM[1]=1 +DEBUG=false +ENV='cluster' +FILES="*.spdl" +INITUNIQUE= +MODEL='ext' +OUTDIR='./graphs' +RUNS='-r 6' +SCYTHER='../scyther/Scyther/scyther-linux' +TIMEOUT= + +# Adversary-compromise models +# EXT +MODELS[0]= +# INT +MODELS[1]='--LKRothers 1' +# CA +MODELS[2]='--LKRactor 1' +# AF +MODELS[3]='--LKRafter 1' +# AFC +MODELS[4]='--LKRaftercorrect 1' +# BR +MODELS[5]='--LKRothers 1 --SKR 1 --SKRinfer' # (inferred session keys) +MODELS[6]='--LKRothers 1 --SKR 1' +# CKw +MODELS[7]='--LKRothers 1 --LKRactor 1 --LKRaftercorrect 1 --SKR 1 --SKRinfer --SSR 1' +MODELS[8]='--LKRothers 1 --LKRactor 1 --LKRaftercorrect 1 --SKR 1 --SSR 1' +# CK +MODELS[9]='--LKRothers 1 --LKRafter 1 --LKRaftercorrect 1 --SKR 1 --SKRinfer --SSR 1' +MODELS[10]='--LKRothers 1 --LKRafter 1 --LKRaftercorrect 1 --SKR 1 --SSR 1' +# eCK-1 +MODELS[11]='--LKRothers 1 --SKR 1 --SKRinfer --RNR 1' +MODELS[12]='--LKRothers 1 --SKR 1 --RNR 1' +# eCK-2 +MODELS[13]='--LKRothers 1 --LKRactor 1 --LKRaftercorrect 1 --SKR 1 --SKRinfer' +MODELS[14]='--LKRothers 1 --LKRactor 1 --LKRaftercorrect 1 --SKR 1' + + +# Parse command line arguments +while getopts “de:hil:m:o:r:t:u:” FLAG; +do + case $FLAG in + d) DEBUG=true;; + e) ENV=$OPTARG;; + i) INITUNIQUE='--init-unique';; + l) CLAIM[0]=$OPTARG;; + m) MODEL=$OPTARG;; + o) OUTDIR=$OPTARG;; + r) RUNS="-r $OPTARG";; + t) TIMEOUT="-T $OPTARG";; + u) CLAIM[1]=$OPTARG;; + h|?) + printf "Usage: %s: [-l num][-u num][-d][-e [cluster|remote|local]][-h][-m model][-o value][-r num][-t sec]file[...]\n" $(basename $0) >&2 + exit 1;; + esac +done +shift $(($OPTIND - 1)) + +# Remaining arguments treated as specification files +if [ -n "$*" ]; then + FILES="$*" + # mkdir -p "$OUTDIR$TSTAMP" +fi + + +# Parse model identifiers +mflags= +case $MODEL in + int) mflags=${MODELS[1]};; + ca) mflags=${MODELS[2]};; + af) mflags=${MODELS[3]};; + afc) mflags=${MODELS[4]};; + bri) mflags=${MODELS[5]};; + br) mflags=${MODELS[6]};; + ckwi) mflags=${MODELS[7]};; + ckw) mflags=${MODELS[8]};; + cki) mflags=${MODELS[9]};; + ck) mflags=${MODELS[10]};; + eck1i) mflags=${MODELS[11]};; + eck1) mflags=${MODELS[12]};; + eck2i) mflags=${MODELS[13]};; + eck2) mflags=${MODELS[14]};; +esac + + +# Verify +for file in $FILES; +do + EXT=`echo "$file" | sed 's/^.*\.//'` + if [ "$EXT" == 'spdl' ]; then + # Extract protocol name + tmp=`basename $file .spdl` + p=`basename $tmp .pp` + + # Execute scyther for selected models and claim + for (( c=${CLAIM[0]}; c<=${CLAIM[1]}; c++ )); + do + init="$SCYTHER $TIMEOUT --force-regular $INITUNIQUE $RUNS $mflags $file -d -o $OUTDIR/${p}_adv-${MODEL}_I$c.dot --filter=$p,I$c" + resp="$SCYTHER $TIMEOUT --force-regular $INITUNIQUE $RUNS $mflags $file -d -o $OUTDIR/${p}_adv-${MODEL}_R$c.dot --filter=$p,R$c" + if $DEBUG; then + echo $init + echo $resp + elif [ $ENV = "cluster" ]; then + bsub -W 08:00 -R "rusage[mem=4096]" $init + bsub -W 08:00 -R "rusage[mem=4096]" $resp + else # $ENV = local + time $init + time $resp + fi + done + else + printf "WARNING: %s could not be processed." $file + fi +done diff --git a/gui/Protocols/IKE/verify_all.sh b/gui/Protocols/IKE/verify_all.sh new file mode 100755 index 0000000..0cad2f6 --- /dev/null +++ b/gui/Protocols/IKE/verify_all.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +if [ -n "$*" ]; then + FILES="$*" + ./verify.sh -i -r 4 -l 1 -u 3 -e remote $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m int $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m ca $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m afc $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m af $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m br $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m bri $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m ckw $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m ckwi $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m ck $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m cki $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m eck1 $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m eck1i $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m eck2 $FILES + ./verify.sh -i -r 4 -l 1 -u 3 -e remote -m eck2i $FILES +fi