From df1a56c7804c98850e9dce6eaafeb3777c524734 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 27 Jul 2006 11:55:24 +0000 Subject: [PATCH] - Iteration seems to work nicely, thank you. --- src/compiler.c | 30 ++++----- src/intruderknowledge.c | 140 ++++++++++++++++++++++++++++++++++++++++ src/intruderknowledge.h | 8 +++ src/system.c | 1 + src/system.h | 1 + 5 files changed, 163 insertions(+), 17 deletions(-) create mode 100644 src/intruderknowledge.c create mode 100644 src/intruderknowledge.h diff --git a/src/compiler.c b/src/compiler.c index 79f4950..9df1e55 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -15,6 +15,7 @@ #include "warshall.h" #include "hidelevel.h" #include "debug.h" +#include "intruderknowledge.h" /* Simple sys pointer as a global. Yields cleaner code although it's against programming standards. @@ -323,6 +324,7 @@ levelTacDeclaration (Tac tc, int isVar) Tac tscan; Termlist typetl = NULL; Term t; + int isAgent; // tscan contains the type list (as is const x,z: Term or var y: Term,Ding) tscan = tc->t2.tac; @@ -353,6 +355,9 @@ levelTacDeclaration (Tac tc, int isVar) typetl = termlistAdd (typetl, t); tscan = tscan->next; } + /* check whether the type list contains the agent type */ + isAgent = inTermlist (typetl, TERM_Agent); + /* parse all constants and vars, because a single declaration can contain multiple ones */ tscan = tc->t1.tac; while (tscan != NULL) @@ -379,6 +384,10 @@ levelTacDeclaration (Tac tc, int isVar) else if (level == 0) { sys->globalconstants = termlistAdd (sys->globalconstants, t); + if (isAgent) + { + sys->agentnames = termlistAdd (sys->agentnames, t); + } } tscan = tscan->next; } @@ -1813,21 +1822,8 @@ preprocess (const System sys) * compute hidelevels */ hidelevelCompute (sys); - - if (switches.check) - { - /* - * display initial role knowledge - */ - - int showRK (Protocol p, Role r) - { - eprintf ("Role "); - termPrint (r->nameterm); - eprintf (" knows "); - termlistPrint (r->knows); - eprintf ("\n"); - } - iterateRoles (sys, showRK); - } + /* + * Initial knowledge + */ + initialIntruderKnowledge (sys); } diff --git a/src/intruderknowledge.c b/src/intruderknowledge.c new file mode 100644 index 0000000..c5b2cd9 --- /dev/null +++ b/src/intruderknowledge.c @@ -0,0 +1,140 @@ +/** + * Initial intruder knowledge computation. + */ + +#include "intruderknowledge.h" + +//! Add a (copy of) a term to the intruder knowledge +void +addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist) +{ + Term t2; + + t2 = termLocal (t, fromlist, tolist); + eprintf ("[ Adding "); + termPrint (t2); + eprintf (" to the initial intruder knowledge]\n"); +} + +//! Unfold the term for all possible options +void +addEnumTerm (const System sys, Term t, Term actor, Termlist todo, + Termlist fromlist, Termlist tolist) +{ + if (todo == NULL) + { + addSTerm (sys, t, fromlist, tolist); + } + else + { + if (termSubTerm (t, todo->term)) + { + // Occurs, we have to iterate + fromlist = termlistPrepend (fromlist, todo->term); + + void iterateThis (Term to) + { + tolist = termlistPrepend (tolist, to); + + addEnumTerm (sys, t, actor, todo->next, fromlist, tolist); + + tolist = termlistDelTerm (tolist); + } + + if (isTermEqual (todo->term, actor)) + { + // Untrusted agents only + Termlist tl; + + for (tl = sys->untrusted; tl != NULL; tl = tl->next) + { + iterateThis (tl->term); + } + } + else + { + // any agents + Termlist tl; + + for (tl = sys->agentnames; tl != NULL; tl = tl->next) + { + iterateThis (tl->term); + } + } + fromlist = termlistDelTerm (fromlist); + } + else + { + // Simply proceed to next + addEnumTerm (sys, t, actor, todo->next, fromlist, tolist); + } + } +} + +//! Does t contain any of sublist? +int +anySubTerm (Term t, Termlist sublist) +{ + while (sublist != NULL) + { + if (termSubTerm (t, sublist->term)) + { + return true; + } + sublist = sublist->next; + } + return false; +} + +void +initialIntruderKnowledge (const System sys) +{ + eprintf ("Computing initial intruder knowledge.\n\n"); + eprintf ("Agent names : "); + termlistPrint (sys->agentnames); + eprintf ("\n"); + eprintf ("Untrusted agents : "); + termlistPrint (sys->untrusted); + eprintf ("\n"); + + /* + * display initial role knowledge + */ + int deriveFromRole (Protocol p, Role r) + { + void addListKnowledge (Termlist tl, Term actor) + { + void addTermKnowledge (Term t) + { + if (anySubTerm (t, p->rolenames)) + { + // Has rolename subterms. We have to enumerate those. + addEnumTerm (sys, t, actor, p->rolenames, NULL, NULL); + } + else + { + // No actor subterm. Simply add. + addSTerm (sys, t, NULL, NULL); + } + } + + while (tl != NULL) + { + addTermKnowledge (tl->term); + tl = tl->next; + } + } + + + eprintf ("Role "); + termPrint (r->nameterm); + eprintf (" knows "); + termlistPrint (r->knows); + eprintf ("\n"); + + addListKnowledge (r->knows, r->nameterm); + return true; + } + + iterateRoles (sys, deriveFromRole); +} diff --git a/src/intruderknowledge.h b/src/intruderknowledge.h new file mode 100644 index 0000000..ad3d284 --- /dev/null +++ b/src/intruderknowledge.h @@ -0,0 +1,8 @@ +#ifndef INTRUDERKNOWLEDGE +#define INTRUDERKNOWLEDGE + +#include "system.h" + +void initialIntruderKnowledge (const System sys); + +#endif diff --git a/src/system.c b/src/system.c index 32a1c44..f8e6156 100644 --- a/src/system.c +++ b/src/system.c @@ -59,6 +59,7 @@ systemInit () sys->protocols = NULL; sys->locals = NULL; sys->variables = NULL; + sys->agentnames = NULL; sys->untrusted = NULL; sys->globalconstants = NULL; sys->hidden = NULL; diff --git a/src/system.h b/src/system.h index 53d9652..94c36db 100644 --- a/src/system.h +++ b/src/system.h @@ -128,6 +128,7 @@ struct system Protocol protocols; //!< List of protocols in the system Termlist locals; //!< List of local terms Termlist variables; //!< List of all variables + Termlist agentnames; //!< List of all agent names (trusted and untrusted) Termlist untrusted; //!< List of untrusted agent names Termlist globalconstants; //!< List of global constants Hiddenterm hidden; //!< List of hiddenterm constructs for Hidelevel lemma