From 7df10cf56821ee8defb1632c52b0e46ed6e24d7f Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 12 Aug 2004 11:55:03 +0000 Subject: [PATCH] - Added role/protocol adding constructs for the intruder with Arachne. --- src/arachne.c | 34 ++++++++++++++++++++++++++++++++-- src/compiler.c | 7 +++++++ src/compiler.h | 2 ++ 3 files changed, 41 insertions(+), 2 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index d395837..a6cf96c 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -15,8 +15,13 @@ #include "arachne.h" static System sys; -static Protocol INTRUDER; // Pointers, to be set by the Init -static Role I_GOAL; // Same here. +Protocol INTRUDER; // Pointers, to be set by the Init +Role I_GOAL; // Same here. +Role I_TEE; +Role I_SPLIT; +Role I_TUPLE; +Role I_ENCRYPT; +Role I_DECRYPT; #ifdef DEBUG static char *explanation; // Pointer to a string that describes what we just tried to do @@ -46,10 +51,35 @@ int iterate (); void 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 /* * Add intruder protocol roles */ + + INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER ")); + + add_event (READ, NULL); + I_GOAL = add_role (" I_GOAL "); + return; } diff --git a/src/compiler.c b/src/compiler.c index 3f5fcee..d44e28d 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -33,6 +33,7 @@ Term levelFind (Symbol s, int i); Term symbolFind (Symbol s); Term tacTerm (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); #define levelDeclareVar(s) levelTacDeclaration(s,1) @@ -101,6 +102,12 @@ compilerInit (const System mysys) langcons (CLAIM_Niagree, "Niagree", TERM_Claim); } +//! Make a global constant +Term makeGlobalConstant (const char *s) +{ + return levelDeclare (symbolSysConst(s), 0, 0); +} + //! Clean up afterwards void compilerDone (void) diff --git a/src/compiler.h b/src/compiler.h index 62e85a1..14eb820 100644 --- a/src/compiler.h +++ b/src/compiler.h @@ -7,5 +7,7 @@ void compilerDone (void); void compile (Tac tc, int maxruns); void preprocess (const System sys); Term findGlobalConstant (const char *s); +Term makeGlobalConstant (const char *s); +void compute_role_variables (const System sys, Protocol p, Role r); #endif