Added IKE base models.
Modelers: Adrian Kyburz and Cas Cremers
This commit is contained in:
parent
5918bf1a3c
commit
34d7cba293
11
gui/Protocols/IKE/Makefile
Normal file
11
gui/Protocols/IKE/Makefile
Normal file
@ -0,0 +1,11 @@
|
||||
CPPSRC= $(wildcard *.cpp)
|
||||
DEST= $(CPPSRC:.cpp=.spdl)
|
||||
|
||||
default: $(DEST)
|
||||
|
||||
%.spdl: %.cpp
|
||||
cpp $< >$@
|
||||
|
||||
mpa: $(DEST) make-mpa.py
|
||||
./make-mpa.py
|
||||
|
157
gui/Protocols/IKE/common.h
Normal file
157
gui/Protocols/IKE/common.h
Normal file
@ -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__
|
96
gui/Protocols/IKE/ikev1-pk-a1.cpp
Normal file
96
gui/Protocols/IKE/ikev1-pk-a1.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
95
gui/Protocols/IKE/ikev1-pk-a12.cpp
Normal file
95
gui/Protocols/IKE/ikev1-pk-a12.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
97
gui/Protocols/IKE/ikev1-pk-a2.cpp
Normal file
97
gui/Protocols/IKE/ikev1-pk-a2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
95
gui/Protocols/IKE/ikev1-pk-a22.cpp
Normal file
95
gui/Protocols/IKE/ikev1-pk-a22.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
103
gui/Protocols/IKE/ikev1-pk-m.cpp
Normal file
103
gui/Protocols/IKE/ikev1-pk-m.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
102
gui/Protocols/IKE/ikev1-pk-m2.cpp
Normal file
102
gui/Protocols/IKE/ikev1-pk-m2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
97
gui/Protocols/IKE/ikev1-pk2-a.cpp
Normal file
97
gui/Protocols/IKE/ikev1-pk2-a.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
97
gui/Protocols/IKE/ikev1-pk2-a2.cpp
Normal file
97
gui/Protocols/IKE/ikev1-pk2-a2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
104
gui/Protocols/IKE/ikev1-pk2-m.cpp
Normal file
104
gui/Protocols/IKE/ikev1-pk2-m.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
106
gui/Protocols/IKE/ikev1-pk2-m2.cpp
Normal file
106
gui/Protocols/IKE/ikev1-pk2-m2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
94
gui/Protocols/IKE/ikev1-psk-a.cpp
Normal file
94
gui/Protocols/IKE/ikev1-psk-a.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
101
gui/Protocols/IKE/ikev1-psk-m-perlman.cpp
Normal file
101
gui/Protocols/IKE/ikev1-psk-m-perlman.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
100
gui/Protocols/IKE/ikev1-psk-m.cpp
Normal file
100
gui/Protocols/IKE/ikev1-psk-m.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
102
gui/Protocols/IKE/ikev1-quick-noid.cpp
Normal file
102
gui/Protocols/IKE/ikev1-quick-noid.cpp
Normal file
@ -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
|
96
gui/Protocols/IKE/ikev1-quick-nopfs.cpp
Normal file
96
gui/Protocols/IKE/ikev1-quick-nopfs.cpp
Normal file
@ -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
|
70
gui/Protocols/IKE/ikev1-quick.cpp
Normal file
70
gui/Protocols/IKE/ikev1-quick.cpp
Normal file
@ -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
|
99
gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp
Normal file
99
gui/Protocols/IKE/ikev1-sig-a-perlman1.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
99
gui/Protocols/IKE/ikev1-sig-a-perlman2.cpp
Normal file
99
gui/Protocols/IKE/ikev1-sig-a-perlman2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
98
gui/Protocols/IKE/ikev1-sig-a1.cpp
Normal file
98
gui/Protocols/IKE/ikev1-sig-a1.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
99
gui/Protocols/IKE/ikev1-sig-a2.cpp
Normal file
99
gui/Protocols/IKE/ikev1-sig-a2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
100
gui/Protocols/IKE/ikev1-sig-m-perlman.cpp
Normal file
100
gui/Protocols/IKE/ikev1-sig-m-perlman.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
102
gui/Protocols/IKE/ikev1-sig-m.cpp
Normal file
102
gui/Protocols/IKE/ikev1-sig-m.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
78
gui/Protocols/IKE/ikev2-child-nopfs.cpp
Normal file
78
gui/Protocols/IKE/ikev2-child-nopfs.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
87
gui/Protocols/IKE/ikev2-child.cpp
Normal file
87
gui/Protocols/IKE/ikev2-child.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
131
gui/Protocols/IKE/ikev2-eap.cpp
Normal file
131
gui/Protocols/IKE/ikev2-eap.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
138
gui/Protocols/IKE/ikev2-eap2.cpp
Normal file
138
gui/Protocols/IKE/ikev2-eap2.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
104
gui/Protocols/IKE/ikev2-mac.cpp
Normal file
104
gui/Protocols/IKE/ikev2-mac.cpp
Normal file
@ -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);
|
||||
}
|
||||
}
|
104
gui/Protocols/IKE/ikev2-mac2.cpp
Normal file
104
gui/Protocols/IKE/ikev2-mac2.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
104
gui/Protocols/IKE/ikev2-mactosig.cpp
Normal file
104
gui/Protocols/IKE/ikev2-mactosig.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
103
gui/Protocols/IKE/ikev2-mactosig2.cpp
Normal file
103
gui/Protocols/IKE/ikev2-mactosig2.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
138
gui/Protocols/IKE/ikev2-sig-child-composed.cpp
Normal file
138
gui/Protocols/IKE/ikev2-sig-child-composed.cpp
Normal file
@ -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) );
|
||||
}
|
||||
}
|
138
gui/Protocols/IKE/ikev2-sig-child.cpp
Normal file
138
gui/Protocols/IKE/ikev2-sig-child.cpp
Normal file
@ -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) );
|
||||
}
|
||||
}
|
138
gui/Protocols/IKE/ikev2-sig-child2-composed.cpp
Normal file
138
gui/Protocols/IKE/ikev2-sig-child2-composed.cpp
Normal file
@ -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) );
|
||||
}
|
||||
}
|
138
gui/Protocols/IKE/ikev2-sig-child2.cpp
Normal file
138
gui/Protocols/IKE/ikev2-sig-child2.cpp
Normal file
@ -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) );
|
||||
}
|
||||
}
|
103
gui/Protocols/IKE/ikev2-sig.cpp
Normal file
103
gui/Protocols/IKE/ikev2-sig.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
103
gui/Protocols/IKE/ikev2-sig2.cpp
Normal file
103
gui/Protocols/IKE/ikev2-sig2.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
104
gui/Protocols/IKE/ikev2-sigtomac.cpp
Normal file
104
gui/Protocols/IKE/ikev2-sigtomac.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
104
gui/Protocols/IKE/ikev2-sigtomac2.cpp
Normal file
104
gui/Protocols/IKE/ikev2-sigtomac2.cpp
Normal file
@ -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 );
|
||||
}
|
||||
}
|
54
gui/Protocols/IKE/jfki-core.cpp
Normal file
54
gui/Protocols/IKE/jfki-core.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
84
gui/Protocols/IKE/jfki.cpp
Normal file
84
gui/Protocols/IKE/jfki.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
78
gui/Protocols/IKE/jfkr-core.cpp
Normal file
78
gui/Protocols/IKE/jfkr-core.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
83
gui/Protocols/IKE/jfkr.cpp
Normal file
83
gui/Protocols/IKE/jfkr.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
63
gui/Protocols/IKE/make-mpa.py
Executable file
63
gui/Protocols/IKE/make-mpa.py
Executable file
@ -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()
|
||||
|
||||
|
6
gui/Protocols/IKE/mpa/README.txt
Normal file
6
gui/Protocols/IKE/mpa/README.txt
Normal file
@ -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.
|
60
gui/Protocols/IKE/oakley-a.cpp
Normal file
60
gui/Protocols/IKE/oakley-a.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
63
gui/Protocols/IKE/oakley-alt.cpp
Normal file
63
gui/Protocols/IKE/oakley-alt.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
105
gui/Protocols/IKE/oakley-c.cpp
Normal file
105
gui/Protocols/IKE/oakley-c.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
21
gui/Protocols/IKE/pp.sh
Executable file
21
gui/Protocols/IKE/pp.sh
Executable file
@ -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
|
800
gui/Protocols/IKE/scanner.py
Executable file
800
gui/Protocols/IKE/scanner.py
Executable file
@ -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)
|
||||
|
||||
|
||||
|
||||
|
||||
|
61
gui/Protocols/IKE/skeme-basic.cpp
Normal file
61
gui/Protocols/IKE/skeme-basic.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
82
gui/Protocols/IKE/skeme-psk.cpp
Normal file
82
gui/Protocols/IKE/skeme-psk.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
80
gui/Protocols/IKE/skeme-rekey.cpp
Normal file
80
gui/Protocols/IKE/skeme-rekey.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
78
gui/Protocols/IKE/sts-mac.cpp
Normal file
78
gui/Protocols/IKE/sts-mac.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
79
gui/Protocols/IKE/sts-main.cpp
Normal file
79
gui/Protocols/IKE/sts-main.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
55
gui/Protocols/IKE/sts-modified.cpp
Normal file
55
gui/Protocols/IKE/sts-modified.cpp
Normal file
@ -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 );
|
||||
|
||||
}
|
||||
}
|
149
gui/Protocols/IKE/verify.sh
Executable file
149
gui/Protocols/IKE/verify.sh
Executable file
@ -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
|
20
gui/Protocols/IKE/verify_all.sh
Executable file
20
gui/Protocols/IKE/verify_all.sh
Executable file
@ -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
|
Loading…
Reference in New Issue
Block a user