From 8b51593cf5f3a2eea9c9ffe11dc10cc4d9a4888b Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 12 May 2005 14:52:50 +0000 Subject: [PATCH] - Each attack now includes * Initial knowledge * Role definitions for protocols involved --- src/term.h | 3 + src/xmlout.c | 242 +++++++++++++++++++++++++++++++++++---------------- 2 files changed, 169 insertions(+), 76 deletions(-) diff --git a/src/term.h b/src/term.h index e4f9fc8..d065946 100644 --- a/src/term.h +++ b/src/term.h @@ -3,6 +3,9 @@ #include "symbol.h" +#define false 0 +#define true 1 + // type <= LEAF means it's a leaf, nkay? enum termtypes { GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE }; diff --git a/src/xmlout.c b/src/xmlout.c index 3fd8294..11aa88a 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -176,6 +176,23 @@ xmlTermPrint (const Term term) printf (""); } +//! Print a termlist in XML form +void +xmlTermlistPrint (Termlist tl) +{ + xmlPrint (""); + xmlindent++; + while (tl != NULL) + { + xmlIndentPrint (); + xmlTermPrint (tl->term); + printf ("\n"); + tl = tl->next; + } + xmlindent--; + xmlPrint (""); +} + //! Print a term for an element void xmlOutTerm (const char *tag, const Term term) @@ -220,91 +237,37 @@ roleTermPrint (const Term t) } } -//! Global system info -/** - * To be used by concrete trace as well as semitrace output - */ +//! Show initial knowledge void -xmlOutSysInfo (const System sys) +xmlInitialKnowledge (const System sys) { - xmlPrint (""); + Termlist knowlist; + + xmlPrint (""); xmlindent++; - - { - Protocol p; - - p = sys->protocols; - while (p != NULL) - { - xmlOutTerm ("protocol", p->nameterm); - p = p->next; - } - } - - xmlOutInteger ("match", sys->match); - + knowlist = knowledgeSet (sys->know); + xmlTermlistPrint (knowlist); + termlistDelete (knowlist); xmlindent--; - xmlPrint (""); + xmlPrint (""); } -//! Nicely format the role and agents we think we're talking to. -void -xmlAgentsOfRunPrint (const System sys, const int run) +//! Determine whether a protocol is involved in the current semitrace. +int +isProtocolInvolved (const System sys, const Protocol p) { - Termlist roles; + int run; - xmlPrint (""); - xmlindent++; - - roles = sys->runs[run].protocol->rolenames; - while (roles != NULL) + run = 0; + while (run < sys->maxruns) { - xmlPrint (""); - xmlOutTerm ("name", roles->term); - xmlOutTerm ("agent", deVar (agentOfRunRole (sys, run, roles->term))); - xmlPrint (""); - roles = roles->next; + if (sys->runs[run].protocol == p) + { + return 1; + } + run++; } - - xmlindent--; - xmlPrint (""); -} - -//! Static information about a run -void -xmlRunInfo (const System sys, const int run) -{ - Role r; - Term oldagent; - - xmlOutInteger ("runid", run); - xmlIndentPrint (); - printf ("runs[run].protocol == INTRUDER) - { - printf (" intruder=\"true\""); - } - printf (">"); - xmlTermPrint (sys->runs[run].protocol->nameterm); - printf ("\n"); - r = sys->runs[run].role; - - /* undo substitution temporarily to retrieve role name */ - /* Note that this is fairly tailored towards the Arachne method, TODO: make - * more generic. */ - oldagent = r->nameterm->subst; - r->nameterm->subst = NULL; - xmlIndentPrint (); - printf (""); - roleTermPrint (r->nameterm); - printf ("\n"); - /* reinstate substitution */ - r->nameterm->subst = oldagent; - if (oldagent != NULL) - { - xmlOutTerm ("agent", r->nameterm); - } - xmlAgentsOfRunPrint (sys, run); + return 0; } //! Show a single event from a run @@ -312,6 +275,8 @@ xmlRunInfo (const System sys, const int run) * run and index will only be output if they are nonnegative. * Also prints any bindings, if this events follows some other events * (typically when this is a read). + * + * If run < 0, it is assumed to be a role event, and thus no bindings will be shown. */ void xmlOutEvent (const System sys, Roledef rd, const int run, const int index) @@ -412,7 +377,8 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index) } xmlindent++; - if (sys->bindings != NULL) + // Only if real run, and not a roledef + if (run >= 0 && sys->bindings != NULL) { list_iterate (sys->bindings, xmlBindingState); } @@ -423,6 +389,130 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index) xmlPrint (""); } +//! Print a list of role events, from a roledef pointer +void +xmlRoleEventlist (const System sys, Roledef rd, int index) +{ + while (rd != NULL) + { + xmlOutEvent (sys, rd, -1, index); + index++; + rd = rd->next; + } +} + +//! Show all protocol roles that are in the attack. +void +xmlInvolvedProtocolRoles (const System sys) +{ + Protocol p; + + p = sys->protocols; + while (p != NULL) + { + if (isProtocolInvolved (sys, p)) + { + Role r; + + xmlPrint (""); + xmlindent++; + xmlOutTerm ("name", p->nameterm); + r = p->roles; + while (r != NULL) + { + xmlPrint (""); + xmlindent++; + xmlOutTerm ("name", r->nameterm); + xmlRoleEventlist (sys, r->roledef, 0); + xmlindent--; + xmlPrint (""); + r = r->next; + } + xmlindent--; + xmlPrint (""); + } + p = p->next; + } +} + +//! Global system info +/** + * To be used by concrete trace as well as semitrace output + */ +void +xmlOutSysInfo (const System sys) +{ + xmlPrint (""); + xmlindent++; + + xmlOutInteger ("match", sys->match); + + xmlInitialKnowledge (sys); + xmlInvolvedProtocolRoles (sys); + xmlindent--; + xmlPrint (""); +} + +//! Nicely format the role and agents we think we're talking to. +void +xmlAgentsOfRunPrint (const System sys, const int run) +{ + Termlist roles; + + xmlPrint (""); + xmlindent++; + + roles = sys->runs[run].protocol->rolenames; + while (roles != NULL) + { + xmlPrint (""); + xmlOutTerm ("name", roles->term); + xmlOutTerm ("agent", deVar (agentOfRunRole (sys, run, roles->term))); + xmlPrint (""); + roles = roles->next; + } + + xmlindent--; + xmlPrint (""); +} + +//! Static information about a run +void +xmlRunInfo (const System sys, const int run) +{ + Role r; + Term oldagent; + + xmlOutInteger ("runid", run); + xmlIndentPrint (); + printf ("runs[run].protocol == INTRUDER) + { + printf (" intruder=\"true\""); + } + printf (">"); + xmlTermPrint (sys->runs[run].protocol->nameterm); + printf ("\n"); + r = sys->runs[run].role; + + /* undo substitution temporarily to retrieve role name */ + /* Note that this is fairly tailored towards the Arachne method, TODO: make + * more generic. */ + oldagent = r->nameterm->subst; + r->nameterm->subst = NULL; + xmlIndentPrint (); + printf (""); + roleTermPrint (r->nameterm); + printf ("\n"); + /* reinstate substitution */ + r->nameterm->subst = oldagent; + if (oldagent != NULL) + { + xmlOutTerm ("agent", r->nameterm); + } + xmlAgentsOfRunPrint (sys, run); +} + //! Display runs void xmlOutRuns (const System sys)