- Added role/protocol adding constructs for the intruder with Arachne.
This commit is contained in:
parent
293c29b88e
commit
7df10cf568
@ -15,8 +15,13 @@
|
|||||||
#include "arachne.h"
|
#include "arachne.h"
|
||||||
|
|
||||||
static System sys;
|
static System sys;
|
||||||
static Protocol INTRUDER; // Pointers, to be set by the Init
|
Protocol INTRUDER; // Pointers, to be set by the Init
|
||||||
static Role I_GOAL; // Same here.
|
Role I_GOAL; // Same here.
|
||||||
|
Role I_TEE;
|
||||||
|
Role I_SPLIT;
|
||||||
|
Role I_TUPLE;
|
||||||
|
Role I_ENCRYPT;
|
||||||
|
Role I_DECRYPT;
|
||||||
|
|
||||||
#ifdef DEBUG
|
#ifdef DEBUG
|
||||||
static char *explanation; // Pointer to a string that describes what we just tried to do
|
static char *explanation; // Pointer to a string that describes what we just tried to do
|
||||||
@ -46,10 +51,35 @@ int iterate ();
|
|||||||
void
|
void
|
||||||
arachneInit (const System mysys)
|
arachneInit (const System mysys)
|
||||||
{
|
{
|
||||||
|
Roledef rd = NULL;
|
||||||
|
|
||||||
|
void add_event (int event, Term message)
|
||||||
|
{
|
||||||
|
rd = roledefAdd (rd, event, NULL, NULL, NULL, message, NULL);
|
||||||
|
}
|
||||||
|
Role add_role (const char *rolename)
|
||||||
|
{
|
||||||
|
Role r;
|
||||||
|
|
||||||
|
r = roleCreate (makeGlobalConstant (rolename));
|
||||||
|
r->roledef = rd;
|
||||||
|
rd = NULL;
|
||||||
|
r->next = INTRUDER->roles;
|
||||||
|
INTRUDER->roles = r;
|
||||||
|
compute_role_variables (sys, INTRUDER, r);
|
||||||
|
return r;
|
||||||
|
}
|
||||||
|
|
||||||
sys = mysys; // make sys available for this module as a global
|
sys = mysys; // make sys available for this module as a global
|
||||||
/*
|
/*
|
||||||
* Add intruder protocol roles
|
* Add intruder protocol roles
|
||||||
*/
|
*/
|
||||||
|
|
||||||
|
INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER "));
|
||||||
|
|
||||||
|
add_event (READ, NULL);
|
||||||
|
I_GOAL = add_role (" I_GOAL ");
|
||||||
|
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -33,6 +33,7 @@ Term levelFind (Symbol s, int i);
|
|||||||
Term symbolFind (Symbol s);
|
Term symbolFind (Symbol s);
|
||||||
Term tacTerm (Tac tc);
|
Term tacTerm (Tac tc);
|
||||||
Termlist tacTermlist (Tac tc);
|
Termlist tacTermlist (Tac tc);
|
||||||
|
Term levelDeclare (Symbol s, int isVar, int level);
|
||||||
void compute_role_variables (const System sys, Protocol p, Role r);
|
void compute_role_variables (const System sys, Protocol p, Role r);
|
||||||
|
|
||||||
#define levelDeclareVar(s) levelTacDeclaration(s,1)
|
#define levelDeclareVar(s) levelTacDeclaration(s,1)
|
||||||
@ -101,6 +102,12 @@ compilerInit (const System mysys)
|
|||||||
langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
|
langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//! Make a global constant
|
||||||
|
Term makeGlobalConstant (const char *s)
|
||||||
|
{
|
||||||
|
return levelDeclare (symbolSysConst(s), 0, 0);
|
||||||
|
}
|
||||||
|
|
||||||
//! Clean up afterwards
|
//! Clean up afterwards
|
||||||
void
|
void
|
||||||
compilerDone (void)
|
compilerDone (void)
|
||||||
|
@ -7,5 +7,7 @@ void compilerDone (void);
|
|||||||
void compile (Tac tc, int maxruns);
|
void compile (Tac tc, int maxruns);
|
||||||
void preprocess (const System sys);
|
void preprocess (const System sys);
|
||||||
Term findGlobalConstant (const char *s);
|
Term findGlobalConstant (const char *s);
|
||||||
|
Term makeGlobalConstant (const char *s);
|
||||||
|
void compute_role_variables (const System sys, Protocol p, Role r);
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
Loading…
Reference in New Issue
Block a user