diff --git a/src/arachne.c b/src/arachne.c index cf51cb4..f571062 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -3260,6 +3260,210 @@ count_false () sys->current_claim->failed = statesIncrease (sys->current_claim->failed); } +//! Create a generic new term of the same type, with a new run identifier. +/** + * Output: the first element of the returned list. + */ +Termlist +createNewTermGeneric (Termlist tl, Term t) +{ + int freenumber; + Termlist tlscan; + Term newterm; + + /* Determine first free number */ + freenumber = 0; + tlscan = tl; + while (tlscan != NULL) + { + Term ts; + + ts = tlscan->term; + if (isLeafNameEqual (t, ts)) + { + if (TermRunid (ts) >= freenumber) + { + freenumber = TermRunid (ts) + 1; + } + } + tlscan = tlscan->next; + } + + /* Make a new term with the free number */ + newterm = (Term) memAlloc (sizeof (struct term)); + memcpy (newterm, t, sizeof (struct term)); + TermRunid (newterm) = freenumber; + + /* return */ + return termlistPrepend (tl, newterm); +} + +//! Create a new term with incremented run rumber, starting at sys->maxruns. +/** + * Output: the first element of the returned list. + */ +Termlist +createNewTerm (Termlist tl, Term t, int isagent) +{ + /* Does if have an explicit type? + * If so, we try to find a fresh name from the intruder knowledge first. + */ + if (isagent) + { + Termlist knowlist; + Termlist kl; + + knowlist = knowledgeSet (sys->know); + kl = knowlist; + while (kl != NULL) + { + Term k; + + k = kl->term; + if (isAgentType (k->stype)) + { + /* agent */ + /* We don't want to instantiate untrusted agents. */ + if (!inTermlist (sys->untrusted, k)) + { + /* trusted agent */ + if (!inTermlist (tl, k)) + { + /* This agent name is not in the list yet. */ + return termlistPrepend (tl, k); + } + } + } + kl = kl->next; + } + termlistDelete (knowlist); + } + + /* Not an agent or no free one found */ + return createNewTermGeneric (tl, t); +} + +//! Delete a term made in the previous constructions +void +deleteNewTerm (Term t) +{ + if (TermRunid (t) >= 0) + { + /* if it has a positive runid, it did not come from the intruder + * knowledge, so it must have been constructed. + */ + memFree (t, sizeof (struct term)); + } +} + +//! Make a trace concrete +Termlist +makeTraceConcrete (const System sys) +{ + Termlist changedvars; + Termlist tlnew; + int run; + + changedvars = NULL; + tlnew = NULL; + run = 0; + + while (run < sys->maxruns) + { + Termlist tl; + + tl = sys->runs[run].locals; + while (tl != NULL) + { + /* variable, and of some run? */ + if (isTermVariable (tl->term) && TermRunid (tl->term) >= 0) + { + Term var; + Term name; + Termlist vartype; + + var = deVar (tl->term); + vartype = var->stype; + // Determine class name + if (vartype != NULL) + { + // Take first type name + name = vartype->term; + } + else + { + // Just a generic name + name = TERM_Data; + } + // We should turn this into an actual term + tlnew = createNewTerm (tlnew, name, isAgentType (var->stype)); + var->subst = tlnew->term; + + // Store for undo later + changedvars = termlistAdd (changedvars, var); + } + tl = tl->next; + } + run++; + } + termlistDelete (tlnew); + return changedvars; +} + +//! Make a trace a class again +void +makeTraceClass (const System sys, Termlist varlist) +{ + Termlist tl; + + tl = varlist; + while (tl != NULL) + { + Term var; + + var = tl->term; + deleteNewTerm (var->subst); + var->subst = NULL; + + tl = tl->next; + } + termlistDelete (varlist); +} + +//! Output an attack in the desired way +void +arachneOutputAttack () +{ + Termlist varlist; + + if (switches.concrete) + { + varlist = makeTraceConcrete (sys); + } + else + { + varlist = NULL; + } + + if (switches.xml) + { + xmlOutSemitrace (sys); + } + else + { + if (switches.latex == 1) + { + latexSemiState (); + } + else + { + dotSemiState (); + } + } + + makeTraceClass (sys, varlist); +} + //------------------------------------------------------------------------ // Main logic core //------------------------------------------------------------------------ @@ -3283,21 +3487,7 @@ property_check () count_false (); if (switches.output == ATTACK) { - if (switches.xml) - { - xmlOutSemitrace (sys); - } - else - { - if (switches.latex == 1) - { - latexSemiState (); - } - else - { - dotSemiState (); - } - } + arachneOutputAttack (); } // Store attack length if shorter attack_this = get_semitrace_length (); diff --git a/src/specialterm.c b/src/specialterm.c index 742f0c9..34c0f44 100644 --- a/src/specialterm.c +++ b/src/specialterm.c @@ -19,6 +19,7 @@ Term TERM_Hidden; Term TERM_Type; Term TERM_Nonce; Term TERM_Ticket; +Term TERM_Data; Term TERM_Claim; Term CLAIM_Secret; @@ -43,6 +44,7 @@ specialTermInit (const System sys) langcons (TERM_Function, "Function", TERM_Type); langcons (TERM_Nonce, "Nonce", TERM_Type); langcons (TERM_Ticket, "Ticket", TERM_Type); + langcons (TERM_Data, "Data", TERM_Type); langcons (CLAIM_Secret, "Secret", TERM_Claim); langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim); diff --git a/src/specialterm.h b/src/specialterm.h index e19aab5..62e801b 100644 --- a/src/specialterm.h +++ b/src/specialterm.h @@ -11,6 +11,7 @@ extern Term TERM_Hidden; extern Term TERM_Type; extern Term TERM_Nonce; extern Term TERM_Ticket; +extern Term TERM_Data; extern Term TERM_Claim; extern Term CLAIM_Secret; diff --git a/src/switches.c b/src/switches.c index 9757ec9..94af867 100644 --- a/src/switches.c +++ b/src/switches.c @@ -67,6 +67,7 @@ switchesInit (int argc, char **argv) switches.arachneSelector = 3; // default goal selection method switches.maxIntruderActions = INT_MAX; // max number of encrypt/decrypt events switches.agentTypecheck = 1; // default do check agent types + switches.concrete = false; // default leaves variables in output to yield class // Misc switches.switchP = 0; // multi-purpose parameter @@ -291,7 +292,8 @@ switcher (const int process, int index) { if (!process) { - helptext ("-M,--modelchecker", "select Model checking engine [Arachne]"); + helptext ("-M,--modelchecker", + "select Model checking engine [Arachne]"); } else { @@ -318,7 +320,8 @@ switcher (const int process, int index) { if (!process) { - helptext ("-m,--match=", "matching method [0] (0:Typed,1:Basic,2:Typeless)"); + helptext ("-m,--match=", + "matching method [0] (0:Typed,1:Basic,2:Typeless)"); } else { @@ -405,11 +408,12 @@ switcher (const int process, int index) if (!process) { helptext ("-H,--human-readable", - "try to make the output human-friendly (e.g. in XML)"); + "try to make the output human-friendly (e.g. in XML). Implies --concrete."); } else { switches.human = true; + switches.concrete = true; return index; } } @@ -588,6 +592,19 @@ switcher (const int process, int index) } } + if (detect (' ', "concrete", 0)) + { + if (!process) + { + /* maybe add after testing */ + } + else + { + switches.concrete = true; + return index; + } + } + #ifdef DEBUG /* ================== * Experimental options diff --git a/src/switches.h b/src/switches.h index d7febe7..b1bebb2 100644 --- a/src/switches.h +++ b/src/switches.h @@ -46,6 +46,7 @@ struct switchdata int arachneSelector; //!< Goal selection method for Arachne engine int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt) int agentTypecheck; //!< Check type of agent variables in all matching modes + int concrete; //!< Swap out variables at the end. // Misc int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. diff --git a/src/term.c b/src/term.c index 0eb1930..70660d7 100644 --- a/src/term.c +++ b/src/term.c @@ -470,7 +470,7 @@ termNodeDuplicate (const Term term) //! Make a true deep copy of a term. /** - * Currently, it this function is not to be used, so we can be sure leaf nodes occur only once in the system. + * Currently, this function is not to be used, so we can be sure leaf nodes occur only once in the system. *@return New memory is allocated and the node is copied recursively. *\sa termDuplicate() */ @@ -1329,3 +1329,10 @@ termPrintDiff (Term t1, Term t2) } } } + +//! Test two leaf terms for abstract equality (abstracting from the run identifiers) +int +isLeafNameEqual (Term t1, Term t2) +{ + return (TermSymb (t1) == TermSymb (t2)); +} diff --git a/src/term.h b/src/term.h index d065946..c11ce7b 100644 --- a/src/term.h +++ b/src/term.h @@ -195,5 +195,6 @@ int term_encryption_level (const Term term); float term_constrain_level (const Term term); void term_set_keylevels (const Term term); void termPrintDiff (Term t1, Term t2); +int isLeafNameEqual (Term t1, Term t2); #endif diff --git a/src/termlist.h b/src/termlist.h index 84caf83..0df189e 100644 --- a/src/termlist.h +++ b/src/termlist.h @@ -32,6 +32,7 @@ __inline__ int inTermlist (Termlist tl, const Term term); __inline__ Termlist termlistFind (Termlist tl, const Term term); int isTermlistEqual (Termlist tl1, Termlist tl2); Termlist termlistAdd (Termlist tl, Term term); +#define termlistPrepend(tl,t) termlistAdd(tl,t) Termlist termlistAppend (const Termlist tl, const Term term); Termlist termlistAddNew (const Termlist tl, const Term t); Termlist termlistConcat (Termlist tl1, Termlist tl2); diff --git a/src/xmlout.c b/src/xmlout.c index 16e95a4..7b09e4c 100644 --- a/src/xmlout.c +++ b/src/xmlout.c @@ -26,6 +26,7 @@ * Externally defined */ extern Protocol INTRUDER; // from arachne.c +extern Term TERM_Data; // from specialterm.c /* * Global/static stuff. @@ -328,19 +329,19 @@ xmlTermType (const Term t) } xmlindent++; - xmlPrint(""); + xmlPrint (""); xmlindent++; xmlIndentPrint (); xmlTermPrint (t); printf ("\n"); xmlindent--; - xmlPrint(""); + xmlPrint (""); - xmlPrint(""); + xmlPrint (""); xmlindent++; xmlTermlistPrint (t->stype); xmlindent--; - xmlPrint(""); + xmlPrint (""); xmlindent--; if (realTermVariable (t)) @@ -373,9 +374,9 @@ xmlVariable (const System sys, const Term variable, const int run) xmlPrint (""); if (variable->subst != NULL) { - xmlPrint (""); + xmlPrint (""); xmlTermType (deVar (variable)); - xmlPrint (""); + xmlPrint (""); } xmlindent--; xmlPrint (""); @@ -902,7 +903,6 @@ xmlOutRuns (const System sys) } } - /* * ----------------------------------------------------------------------------------- * Publicly available functions