andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- From this version onwards, Scyther no longer supports the modelchecker

Browse Source 
method. A big cleanup has been started, but is not finished yet, so
  minor artefacts might still remain. These are to be cleaned up later.
This commit is contained in:
ccremers 2006-03-08 13:58:46 +00:00
parent 2830c8e8ff
commit 5487d3ae90
46 changed files with 127 additions and 5525 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/arachne.c
View File

@ -10,6 +10,7 @@
#include <stdlib.h>
#include <limits.h>
#include <float.h>
#include <string.h>
#ifdef DEBUG
#include <malloc.h>
#endif
@ -23,7 +24,6 @@
#include "states.h"
#include "mgu.h"
#include "arachne.h"
#include "memory.h"
#include "error.h"
#include "claim.h"
#include "debug.h"
@ -166,12 +166,9 @@ void
indentPrefixPrint (const int annotate, const int jumps)
{
void counterPrint ()
{
if (switches.engine == ARACHNE_ENGINE)
{
statesFormat (sys->current_claim->states);
eprintf ("\t");
}
eprintf ("%i", annotate);
eprintf ("\t");
}
@ -1770,7 +1767,7 @@ createNewTermGeneric (Termlist tl, Term t)
}
/* Make a new term with the free number */
newterm = (Term) memAlloc (sizeof (struct term));
newterm = (Term) malloc (sizeof (struct term));
memcpy (newterm, t, sizeof (struct term));
TermRunid (newterm) = freenumber;
@ -1839,7 +1836,7 @@ deleteNewTerm (Term t)
/* 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));
free (t);
}
}

142
src/attackminimize.c
View File

@ -1,142 +0,0 @@
#include <stdio.h>
#include <stdlib.h>
#include "system.h"
#include "tracebuf.h"
//! Help counter for the number of unknowns.
int cUnk = 0;
//! Help counter for the number of todos.
int cTod = 0;
//! Mark all events of the same run before the event as required.
/**
*@param sys The system.
*@param tb The attack buffer.
*@param ev The reference event index.
*/
void
markback (const System sys, struct tracebuf *tb, int ev)
{
int run = tb->run[ev];
while (ev >= 0)
{
if (tb->run[ev] == run)
{
switch (tb->event[ev]->type)
{
case READ:
switch (tb->status[ev])
{
case S_UNK:
cUnk--;
case S_RED:
tb->status[ev] = S_TOD;
cTod++;
break;
case S_TOD:
case S_OKE:
break;
}
break;
case SEND:
case CLAIM:
if (tb->status[ev] == S_UNK)
{
cUnk--;
}
tb->status[ev] = S_OKE;
break;
}
}
ev--;
}
}
//! Minimize the attack.
void
attackMinimize (const System sys, struct tracebuf *tb)
{
int i;
int j;
cUnk = 0;
cTod = 0;
for (i = 0; i < tb->length; i++)
{
switch (tb->status[i])
{
case S_UNK:
cUnk++;
break;
case S_TOD:
cTod++;
break;
default:
break;
}
}
markback (sys, tb, tb->violatedclaim);
while (cUnk + cTod > 0)
{
while (cTod > 0)
{
for (i = 0; i < tb->length; i++)
// kies een i; laten we de eerste maar pakken
{
if (tb->status[i] == S_TOD)
break;
}
if (i == tb->length)
{
eprintf ("Some step error.\n");
exit (1);
}
j = i;
while (j >= 0 && inKnowledge (tb->know[j], tb->event[i]->message))
{
// zoek waar m in de kennis komt
j--;
}
tb->status[i] = S_OKE;
cTod--;
if (j >= 0)
{
markback (sys, tb, j);
}
}
while (cTod == 0 && cUnk > 0)
{
for (i = tb->length - 1; i >= 0; i--)
// pak laatste i
{
if (tb->status[i] == S_UNK)
break;
}
if (i < 0)
{
eprintf ("Some i<0 error.\n");
exit (1);
}
tb->status[i] = S_RED;
cUnk--;
tb->reallength--;
j = tracebufRebuildKnow (tb);
if (j > -1)
{
tb->reallength++;
markback (sys, tb, i);
if (j < tb->length)
{
tb->link[j] = (tb->link[j] > i ? tb->link[j] : i);
}
}
}
}
}

1
src/attackminimize.h
View File

@ -1 +0,0 @@
void attackMinimize (const System sys, struct tracebuf *tb);

5
src/binding.c
View File

@ -8,7 +8,6 @@
#include "system.h"
#include "binding.h"
#include "warshall.h"
#include "memory.h"
#include "debug.h"
#include "term.h"
#include "termmap.h"
@ -34,7 +33,7 @@ binding_create (Term term, int run_to, int ev_to)
{
Binding b;
b = memAlloc (sizeof (struct binding));
b = malloc (sizeof (struct binding));
b->done = false;
b->blocked = false;
b->run_from = -1;
@ -54,7 +53,7 @@ binding_destroy (Binding b)
{
goal_unbind (b);
}
memFree (b, sizeof (struct binding));
free (b);
}
/*

1
src/claim.c
View File

@ -17,7 +17,6 @@
#include "arachne.h"
#include "specialterm.h"
#include "switches.h"
#include "memory.h"
//! When none of the runs match
#define MATCH_NONE 0

15
src/compiler.c
View File

@ -5,7 +5,6 @@
#include "term.h"
#include "termlist.h"
#include "label.h"
#include "memory.h"
#include "system.h"
#include "knowledge.h"
#include "symbol.h"
@ -438,7 +437,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
}
// Assert: label is unique, add claimlist info
cl = memAlloc (sizeof (struct claimlist));
cl = malloc (sizeof (struct claimlist));
cl->type = claim;
cl->label = label;
cl->parameter = msg;
@ -1003,15 +1002,9 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
Term rolename;
Role r;
if (switches.engine == ARACHNE_ENGINE)
{
rolename = levelVar (tcroles->t1.sym);
rolename->stype = termlistAdd (NULL, TERM_Agent);
}
else
{
rolename = levelConst (tcroles->t1.sym);
}
/* add name to list of role names */
pr->rolenames = termlistAppend (pr->rolenames, rolename);
/* make new (empty) current protocol with name */
@ -1402,7 +1395,7 @@ compute_prec_sets (const System sys)
//eprintf ("Maxevent : %i\n", sys->roleeventmax);
size = sys->rolecount * sys->roleeventmax;
rowsize = WORDSIZE (size);
eventlabels = memAlloc (size * sizeof (Term));
eventlabels = malloc (size * sizeof (Term));
prec = (unsigned int *) CALLOC (1, rowsize * size * sizeof (unsigned int));
// Assign labels
r1 = 0;
@ -1703,7 +1696,7 @@ compute_prec_sets (const System sys)
/*
* Cleanup
*/
memFree (eventlabels, size * sizeof (Term));
free (eventlabels);
FREE (prec);
#ifdef DEBUG

336
src/constraint.c
View File

@ -1,336 +0,0 @@
#include <stdio.h>
#include "memory.h"
#include "constraint.h"
#include "debug.h"
#include "system.h"
/* constraints currently are shallow copies */
Constraint
makeConstraint (Term term, Knowledge know)
{
/* maybe knowDup can just be a link, but then it needs to be moved from destroy as well */
Constraint co = memAlloc (sizeof (struct constraint));
co->term = term;
//co->know = knowledgeDuplicate(know);
co->know = know;
return co;
}
Constraint
constraintDuplicate (Constraint co)
{
return makeConstraint (co->term, co->know);
}
void
constraintDestroy (Constraint cons)
{
//knowledgeDelete(cons->know);
if (cons != NULL)
memFree (cons, sizeof (struct constraint));
}
/* constraints are typically added at the end, to maintain the order in which they were added */
Constraintlist
constraintlistAdd (Constraintlist cl, Constraint co)
{
Constraintlist clnew = memAlloc (sizeof (struct constraintlist));
clnew->constraint = co;
clnew->next = NULL;
if (cl == NULL)
{
clnew->prev = NULL;
return clnew;
}
else
{
Constraintlist scan;
scan = cl;
while (scan->next != NULL)
scan = scan->next;
scan->next = clnew;
clnew->prev = scan;
return cl;
}
}
Constraintlist
constraintlistConcat (Constraintlist cl1, Constraintlist cl2)
{
Constraintlist scan;
if (cl1 == NULL)
return cl2;
scan = cl1;
while (scan->next != NULL)
scan = scan->next;
scan->next = cl2;
return cl1;
}
Constraintlist
constraintlistRewind (Constraintlist cl)
{
if (cl == NULL)
return NULL;
while (cl->prev != NULL)
cl = cl->prev;
return cl;
}
Constraintlist
constraintlistInsert (Constraintlist cl, Term term, Knowledge know)
{
Constraintlist clnew = memAlloc (sizeof (struct constraintlist));
clnew->constraint = makeConstraint (term, know);
if (cl != NULL)
{
if (cl->next != NULL)
{
clnew->next = cl->next;
cl->next->prev = cl;
}
else
{
clnew->next = NULL;
}
clnew->prev = cl;
cl->next = clnew;
return constraintlistRewind (cl);
}
else
{
clnew->next = NULL;
clnew->prev = NULL;
return clnew;
}
}
/* unlink a single constraint */
Constraintlist
constraintlistUnlink (Constraintlist cl)
{
Constraintlist clnext, clprev;
if (cl == NULL)
return NULL;
clprev = cl->prev;
clnext = cl->next;
if (clnext != NULL)
{
clnext->prev = clprev;
cl->next = NULL;
}
if (clprev != NULL)
{
clprev->next = clnext;
cl->prev = NULL;
return constraintlistRewind (clprev);
}
else
{
return clnext;
}
}
/* remove a single constraint */
Constraintlist
constraintlistRemove (Constraintlist cl)
{
Constraintlist clnew;
clnew = constraintlistUnlink (cl);
memFree (cl, sizeof (struct constraintlist));
return clnew;
}
/* remove all constraints from this point onwards */
void
constraintlistDelete (Constraintlist cl)
{
Constraintlist cldel;
/* no empty cl */
if (cl == NULL)
return;
/* cut off previous */
if (cl->prev != NULL)
{
/* TODO maybe this should cause a warning? */
eprintf ("WARNING: clDelete with non-empty prev\n");
cl->prev->next = NULL;
}
while (cl != NULL)
{
cldel = cl;
cl = cl->next;
memFree (cldel, sizeof (struct constraintlist));
}
return;
}
void
constraintlistDestroy (Constraintlist cl)
{
Constraintlist cldel;
/* no empty cl */
if (cl == NULL)
return;
/* cut off previous */
if (cl->prev != NULL)
{
/* TODO maybe this should cause a warning? */
eprintf ("WARNING: clDestroy with non-empty prev\n");
cl->prev = NULL;
}
while (cl != NULL)
{
cldel = cl;
cl = cl->next;
constraintDestroy (cldel->constraint);
memFree (cldel, sizeof (struct constraintlist));
}
}
Constraintlist
constraintlistDuplicate (Constraintlist oldcl)
{
Constraintlist newcl = NULL;
while (oldcl != NULL)
{
newcl =
constraintlistAdd (newcl, constraintDuplicate (oldcl->constraint));
oldcl = oldcl->next;
}
return newcl;
}
Constraintlist
constraintlistShallow (Constraintlist oldcl)
{
Constraintlist newcl = NULL;
while (oldcl != NULL)
{
newcl = constraintlistAdd (newcl, oldcl->constraint);
oldcl = oldcl->next;
}
return newcl;
}
/* ----------------------------------------------------------
Print stuff
---------------------------------------------------------- */
void
constraintPrint (Constraint co)
{
indent ();
eprintf ("Constraint ");
if (co == NULL)
{
eprintf ("[empty]\n");
return;
}
termPrint (co->term);
eprintf (" :\n");
knowledgePrint (co->know);
}
void
constraintlistPrint (Constraintlist cl)
{
if (cl == NULL)
{
indent ();
eprintf ("[empty constraintlist]\n");
return;
}
while (cl != NULL)
{
constraintPrint (cl->constraint);
cl = cl->next;
}
}
/* ----------------------------------------------------------
Now some real logic for the constraints
---------------------------------------------------------- */
/* eliminate all standalone variables */
void
msElim (Constraint co)
{
Termlist tl;
/* simple variables can only exist in basic */
if (co->know == NULL)
{
#ifdef DEBUG
debug (5, "Exiting because co->know is empty.");
#endif
}
else
{
tl = co->know->basic;
while (tl != NULL)
{
if (isTermVariable (tl->term))
{
tl = termlistDelTerm (tl);
co->know->basic = tl;
}
else
tl = tl->next;
}
}
}
/* find the first constraint such that m is not a variable */
/* also, apply standalone elimination to it */
Constraintlist
firstNonVariable (Constraintlist cl)
{
while (cl != NULL && isTermVariable (cl->constraint->term))
{
cl = cl->next;
}
if (cl != NULL)
{
msElim (cl->constraint);
cl->constraint->term = deVar (cl->constraint->term);
return cl;
}
else
{
return NULL;
}
}

42
src/constraint.h
View File

@ -1,42 +0,0 @@
#ifndef CONSTRAINTS
#define CONSTRAINTS
#include "term.h"
#include "knowledge.h"
struct constraint
{
Term term;
Knowledge know;
};
typedef struct constraint *Constraint;
struct constraintlist
{
Constraint constraint;
struct constraintlist *next;
struct constraintlist *prev;
};
typedef struct constraintlist *Constraintlist;
Constraint makeConstraint (Term term, Knowledge know);
Constraint constraintDuplicate (Constraint co);
void constraintDestroy (Constraint cons);
Constraintlist constraintlistAdd (Constraintlist cl, Constraint co);
Constraintlist constraintlistConcat (Constraintlist cl1, Constraintlist cl2);
Constraintlist constraintlistRewind (Constraintlist cl);
Constraintlist constraintlistInsert (Constraintlist cl, Term term,
Knowledge know);
Constraintlist constraintlistUnlink (Constraintlist cl);
Constraintlist constraintlistRemove (Constraintlist cl);
void constraintlistDestroy (Constraintlist cl);
void constraintlistDelete (Constraintlist cl);
Constraintlist constraintlistShallow (Constraintlist oldcl);
Constraintlist constraintlistDuplicate (Constraintlist oldcl);
void constraintPrint (Constraint co);
void constraintlistPrint (Constraintlist cl);
Constraintlist firstNonVariable (Constraintlist cl);
#endif

2
src/depend.c
View File

@ -4,6 +4,8 @@
*
*/
#include <stdlib.h>
#include <string.h>
#include "depend.h"
#include "term.h"
#include "system.h"

11
src/dotout.c
View File

@ -1,9 +1,9 @@
#include <stdlib.h>
#include <limits.h>
#include "system.h"
#include "switches.h"
#include "memory.h"
#include "arachne.h"
#include "depend.h"
#include <limits.h>
extern Protocol INTRUDER; // Pointers, to be set by the Init of arachne.c
extern Role I_M; // Same here.
@ -238,8 +238,7 @@ iterate_outgoing_arrows (const System sys, void (*func) (), const int run,
//! Display the current semistate using dot output format.
/**
* This is not as nice as we would like it. Furthermore, the function is too big, and needs to be split into functional parts that
* will allow the generation of LaTeX code as well.
* This is not as nice as we would like it. Furthermore, the function is too big.
*/
void
dotSemiState (const System sys)
@ -288,7 +287,7 @@ dotSemiState (const System sys)
// Needed for the bindings later on: create graph
nodes = nodeCount ();
ranks = memAlloc (nodes * sizeof (int));
ranks = malloc (nodes * sizeof (int));
maxrank = graph_ranks (ranks, nodes); // determine ranks
#ifdef DEBUG
@ -669,7 +668,7 @@ dotSemiState (const System sys)
#endif
// clean memory
memFree (ranks, nodes * sizeof (int)); // ranks
free (ranks); // ranks
// close graph
eprintf ("};\n\n");

1
src/error.c
View File

@ -1,3 +1,4 @@
#include <stdlib.h>
#include <stdio.h>
#include <stdarg.h>
#include "error.h"

4
src/hidelevel.c
View File

@ -4,10 +4,10 @@
* instead of fully recomputing the required data each time again.
*/
#include <stdlib.h>
#include <limits.h>
#include "hidelevel.h"
#include "system.h"
#include "memory.h"
extern Term TERM_Hidden;
@ -115,7 +115,7 @@ hidelevelCompute (const System sys)
{
Hiddenterm ht;
ht = (Hiddenterm) memAlloc (sizeof (struct hiddenterm));
ht = (Hiddenterm) malloc (sizeof (struct hiddenterm));
ht->term = tl->term;
ht->hideminimum = l;
ht->hideprotocol = l2;

7
src/knowledge.c
View File

@ -8,7 +8,6 @@
#include <stdio.h>
#include "termlist.h"
#include "knowledge.h"
#include "memory.h"
#include "system.h"
#include "debug.h"
@ -47,7 +46,7 @@ knowledgeDone (void)
Knowledge
makeKnowledge ()
{
return (Knowledge) memAlloc (sizeof (struct knowledge));
return (Knowledge) malloc (sizeof (struct knowledge));
}
//! Create a new empty knowledge structure.
@ -107,7 +106,7 @@ knowledgeDelete (Knowledge know)
termlistDelete (know->basic);
termlistDelete (know->encrypt);
termlistDelete (know->vars);
memFree (know, sizeof (struct knowledge));
free (know);
}
}
@ -126,7 +125,7 @@ knowledgeDestroy (Knowledge know)
termlistDestroy (know->encrypt);
termlistDestroy (know->vars);
// termlistDestroy(know->inverses);
memFree (know, sizeof (struct knowledge));
free (know);
}
}

6
src/label.c
View File

@ -2,7 +2,7 @@
* Label info
*/
#include "memory.h"
#include <stdlib.h>
#include "term.h"
#include "label.h"
#include "list.h"
@ -14,7 +14,7 @@ label_create (const Term label, const Protocol protocol)
{
Labelinfo li;
li = (Labelinfo) memAlloc (sizeof (struct labelinfo));
li = (Labelinfo) malloc (sizeof (struct labelinfo));
li->label = label;
li->protocol = protocol;
li->sendrole = NULL;
@ -26,7 +26,7 @@ label_create (const Term label, const Protocol protocol)
void
label_destroy (Labelinfo linfo)
{
memFree (linfo, sizeof (struct labelinfo));
free (linfo);
}
//! Given a list of label infos, yield the correct one or NULL

1123
src/latex.c
View File

File diff suppressed because it is too large Load Diff

21
src/latex.h
View File

@ -1,21 +0,0 @@
/*
* LaTeX output component header
*/
#ifndef LATEX
#define LATEX
#include "system.h"
void latexInit (const System sys, int argc, char **argv);
void latexDone (const System sys);
void latexTimers (const System sys);
void latexMSCStart ();
void latexMSCEnd ();
void latexLearnComment (const System sys, Termlist tl);
void latexTracePrint (const System sys);
void attackDisplayLatex (const System sys);
void latexTermPrint (Term term, Termlist hl);
void latexTermTuplePrint (Term term, Termlist hl);
#endif

11
src/main-switches.c
View File

@ -46,7 +46,6 @@ enum exittypes
#include "system.h"
#include "debug.h"
#include "modelchecker.h"
#include "memory.h"
#include "symbol.h"
#include "pheading.h"
#include "symbol.h"
@ -54,8 +53,6 @@ enum exittypes
#include "tac.h"
#include "timer.h"
#include "compiler.h"
#include "latex.h"
#include "output.h"
#include "binding.h"
#include "version.h"
#include "specialterm.h"
@ -130,8 +127,6 @@ main (int argc, char **argv)
struct arg_int *switch_goal_select_method =
arg_int0 (NULL, "goal-select", NULL,
"use goal selection method <int> (default 3)");
struct arg_lit *switch_latex_output =
arg_lit0 (NULL, "latex", "output attacks in LaTeX format");
struct arg_lit *switch_empty =
arg_lit0 ("e", "empty", "do not generate output");
struct arg_lit *switch_progress_bar =
@ -343,8 +338,6 @@ main (int argc, char **argv)
#else
debugSet (0);
#endif
/* Initialize memory routines */
memInit ();
/* initialize symbols */
termsInit ();
@ -668,11 +661,8 @@ main (int argc, char **argv)
* Now we clean up any memory that was allocated.
*/
if (switches.engine == ARACHNE_ENGINE)
{
arachneDone ();
bindingDone ();
}
knowledgeDestroy (sys->know);
systemDone (sys);
compilerDone ();
@ -687,7 +677,6 @@ main (int argc, char **argv)
/* memory clean up? */
strings_cleanup ();
memDone ();
exit:
/* deallocate each non-null entry in argtable[] */

269
src/main.c
View File

@ -26,8 +26,6 @@
*
* 3 Okay Attack found
*
* However, if the --scenario=-1 switch is used, the exit code is used to return the number of scenarios.
*
* \section coding Coding conventions
*
* Usually, each source file except main.c has an myfileInit() and myfileDone() function
@ -43,8 +41,6 @@
#include <limits.h>
#include "system.h"
#include "debug.h"
#include "modelchecker.h"
#include "memory.h"
#include "symbol.h"
#include "pheading.h"
#include "symbol.h"
@ -52,8 +48,6 @@
#include "tac.h"
#include "timer.h"
#include "compiler.h"
#include "latex.h"
#include "output.h"
#include "binding.h"
#include "switches.h"
#include "specialterm.h"
@ -84,9 +78,6 @@ main (int argc, char **argv)
int nerrors;
int exitcode = EXIT_NOATTACK;
/* Initialize memory routines */
memInit ();
/* initialize symbols */
termsInit ();
termmapsInit ();
@ -126,16 +117,8 @@ main (int argc, char **argv)
/* compile */
if (switches.engine != ARACHNE_ENGINE)
{
// Compile as many runs as possible
compile (spdltac, switches.runs);
}
else
{
// Compile no runs for Arachne
compile (spdltac, 0);
}
scanner_cleanup ();
/* preprocess */
@ -173,11 +156,6 @@ main (int argc, char **argv)
* ---------------------------------------
*/
/* Latex only makes sense for attacks */
if (switches.latex && switches.output != ATTACK)
{
error ("Scyther can only generate LaTeX output for attacks.");
}
#ifdef DEBUG
if (DEBUGL (4))
{
@ -185,10 +163,8 @@ main (int argc, char **argv)
}
#endif
if (switches.engine == ARACHNE_ENGINE)
{
arachneInit (sys);
}
/*
* ---------------------------------------
* Start real stuff
@ -199,10 +175,6 @@ main (int argc, char **argv)
if (switches.xml)
xmlOutInit ();
/* latex header? */
if (switches.latex)
latexInit (sys, argc, argv);
/* model check system */
#ifdef DEBUG
if (DEBUGL (1))
@ -216,58 +188,19 @@ main (int argc, char **argv)
* ---------------------------------------
*/
/* Display shortest attack, if any */
/* Exitcodes are *not* correct anymore */
if (sys->attack != NULL && sys->attack->length != 0)
{
if (switches.output == ATTACK)
{
attackDisplay (sys);
}
/* mark exit code */
exitcode = EXIT_ATTACK;
}
else
{
/* check if there is a claim type that was never reached */
Claimlist cl_scan;
cl_scan = sys->claimlist;
while (cl_scan != NULL)
{
if (cl_scan->failed == STATES0)
{
/* mark exit code */
exitcode = EXIT_NOCLAIM;
}
cl_scan = cl_scan->next;
}
}
/* latex closeup */
if (switches.latex)
latexDone (sys);
/* xml closeup */
if (switches.xml)
xmlOutDone ();
/* Transfer any scenario counting to the exit code,
* assuming that there is no error. */
if (exitcode != EXIT_ERROR && switches.scenario < 0)
{
exitcode = sys->countScenario;
}
/*
* Now we clean up any memory that was allocated.
*/
if (switches.engine == ARACHNE_ENGINE)
{
arachneDone ();
}
knowledgeDestroy (sys->know);
systemDone (sys);
colorDone ();
@ -283,7 +216,6 @@ main (int argc, char **argv)
/* memory clean up? */
strings_cleanup ();
memDone ();
exit:
return exitcode;
@ -341,66 +273,6 @@ timersPrint (const System sys)
//**********************************************************************
/* states traversed */
if (switches.engine == POR_ENGINE)
{
eprintf ("states\t");
statesPrintShort (sys);
eprintf ("\n");
/* scenario info */
if (switches.scenario > 0)
{
eprintf ("scen_st\t");
statesFormat (sys->statesScenario);
eprintf ("\n");
}
/* flag
*
* L n Attack of length <n>
* None failed claim
* NoClaim no claims
*/
eprintf ("attack\t");
if (sys->claims == STATES0)
{
eprintf ("NoClaim\n");
}
else
{
if (sys->failed != STATES0)
eprintf ("L:%i\n", attackLength (sys->attack));
else
eprintf ("None\n");
}
#ifndef NOTIMERS
/* print time */
double seconds;
seconds = (double) clock () / CLOCKS_PER_SEC;
eprintf ("time\t%.3e\n", seconds);
/* states per second */
eprintf ("st/sec\t");
if (seconds > 0)
{
eprintf ("%.3e\n", statesDouble (sys->states) / seconds);
}
else
{
eprintf ("<inf>\n");
}
#endif
}
//**********************************************************************
/* Print also individual claims */
/* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing)
*/
@ -559,14 +431,11 @@ timersPrint (const System sys)
}
/* states (if asked) */
if (switches.engine == ARACHNE_ENGINE)
{
if (switches.countStates)
{
eprintf ("\tstates=");
statesFormat (cl_scan->states);
}
}
/* any warnings */
if (cl_scan->warnings)
@ -591,108 +460,7 @@ timersPrint (const System sys)
}
}
//! Analyse the model by incremental runs.
/*
* This procedure considers mainly incremental searches, and settings
* parameters for that. The real work is handled by modelCheck.
*/
void
MC_incRuns (const System sys)
{
/*
* incremental runs check
*
* note: we assume that at least one run needs to be checked.
*/
int maxruns = sys->maxruns;
int runs = 1;
int flag = 1;
int res;
do
{
systemReset (sys);
sys->maxruns = runs;
systemRuns (sys);
fprintf (stderr, "%i of %i runs in incremental runs search.\n",
runs, maxruns);
res = modelCheck (sys);
fprintf (stderr, "\n");
if (res)
{
/* Apparently a violation occurred. If we are searching
* the whole space, then we just continue. However, if
* we're looking to prune, ``the buck stops here''. */
if (switches.prune != 0)
{
flag = 0;
}
}
runs++;
}
while (flag && runs <= maxruns);
sys->maxruns = maxruns;
}
//! Analyse the model by incremental trace lengths.
/*
* This procedure considers mainly incremental searches, and settings
* parameters for that. The real work is handled by modelCheck.
*/
void
MC_incTraces (const System sys)
{
/*
* incremental traces check
*
* note: we assume that at least one run needs to be checked.
*/
int maxtracelen;
int tracelen;
int tracestep;
int flag;
int res;
tracestep = 3; /* what is a sensible stepping size? */
flag = 1;
maxtracelen = getMaxTraceLength (sys);
tracelen = maxtracelen - tracestep;
while (tracelen > 6) /* what is a reasonable minimum? */
tracelen -= tracestep;
flag = 1;
do
{
systemReset (sys);
sys->maxtracelength = tracelen;
systemRuns (sys);
fprintf (stderr,
"%i of %i trace length in incremental trace length search.\n",
tracelen, maxtracelen);
res = modelCheck (sys);
fprintf (stderr, "\n");
if (res)
{
/* Apparently a violation occurred. If we are searching
* the whole space, then we just continue. However, if
* we're looking to prune, ``the buck stops here''. */
if (switches.prune != 0)
{
flag = 0;
}
}
tracelen += tracestep;
}
while (flag && tracelen <= maxtracelen);
}
//! Analyse the model with a fixed scenario.
//! Analyse the model
/**
* Traditional handywork.
*/
@ -720,26 +488,8 @@ MC_single (const System sys)
int
modelCheck (const System sys)
{
if (switches.output == STATESPACE)
{
graphInit (sys);
}
/* modelcheck the system */
switch (switches.engine)
{
case POR_ENGINE:
if (sys->maxruns > 0)
traverse (sys);
else
warning ("Model checking system with empty scenario.");
break;
case ARACHNE_ENGINE:
arachne ();
break;
default:
error ("Unknown engine type %i.", switches.engine);
}
/* clean up any states display */
if (switches.reportStates > 0)
@ -749,18 +499,5 @@ modelCheck (const System sys)
}
timersPrint (sys);
if (switches.output == STATESPACE)
{
graphDone (sys);
}
if (switches.scenario > 0)
{
/* Traversing a scenario. Maybe we ran out. */
if (switches.scenario > sys->countScenario)
{
/* Signal as error */
exit (1);
}
}
return (sys->failed != STATES0);
}

308
src/match_basic.c
View File

@ -1,308 +0,0 @@
/*!\file match_basic.c
*\brief Implements the match function.
*
* The match function here is integrated here with an enabled() function.
* It is also the basic match, so not suited for Constraint Logic Programming.
*/
#include <stdlib.h>
#include <stdio.h>
#include "memory.h"
#include "substitution.h"
#include "system.h"
#include "modelchecker.h"
#include "match_basic.h"
#include "switches.h"
//! Get the candidates list for typeless basic stuff
__inline__ Termlist
candidates (const Knowledge know)
{
return knowledgeGetBasics (know);
}
struct fvpass
{
int (*solution) ();
System sys;
int run;
Roledef roledef;
int (*proceed) (System, int);
};
//! Fix variables in a message, and check whether it can be accepted.
/**
* fp.sys is only accessed for the matching type.
*@returns 1 (true) if there exists a message that can be accepted, fvpass returns 1 on it.
*/
int
fixVariablelist (const struct fvpass fp, const Knowledge know,
Termlist varlist, const Term message)
{
int flag = 0;
Termlist tlscan;
Termlist candlist;
if (varlist != NULL)
{
if (!isTermVariable (varlist->term))
{
while (varlist != NULL && !isTermVariable (varlist->term))
{
varlist = varlist->next;
}
}
}
/* cond: varlist == NULL || isTermvariable(varlist->term) */
if (varlist == NULL)
{
/* there are no (more) variables to be fixed. */
/* actually trigger it if possible */
int copied;
Knowledge tempknow;
/* first we propagate the substitutions in the knowledge */
/* TODO this must also be done for all agent knowledge!! */
if (knowledgeSubstNeeded (know))
{
copied = 1;
tempknow = knowledgeSubstDo (know);
}
else
{
copied = 0;
tempknow = know;
}
if (inKnowledge (tempknow, message))
{
if (fp.solution != NULL)
{
flag = fp.solution (fp, tempknow);
}
else
{
/* signal that it was enabled, now we omit the pruning */
flag = 1;
}
}
else
{
/* not enabled */
flag = 0;
}
/* restore state */
if (copied)
{
knowledgeDelete (tempknow);
knowledgeSubstUndo (know);
}
return flag;
}
/* cond: isTermvariable(varlist->term) */
varlist->term = deVar (varlist->term);
/* cond: realTermvariable(varlist->term) */
candlist = candidates (know);
#ifdef DEBUG
if (DEBUGL (5))
{
indent ();
printf ("Set ");
termPrint (varlist->term);
printf (" with type ");
termlistPrint (varlist->term->stype);
printf (" from candidates ");
termlistPrint (candlist);
printf ("\n");
}
#endif
/* Now check all candidates. Do they work as candidates? */
tlscan = candlist;
while (tlscan != NULL && !(flag && fp.solution == NULL))
{
if (!isTermEqual (varlist->term, tlscan->term))
{
/* substitute */
varlist->term->subst = tlscan->term;
if (validSubst (switches.match, varlist->term))
{
#ifdef DEBUG
if (DEBUGL (5))
{
indent ();
printf ("Substituting ");
termPrint (varlist->term);
printf ("\n");
}
#endif
/* now we may need to substitute more */
flag = fixVariablelist (fp, know, varlist->next, message)
|| flag;
}
}
tlscan = tlscan->next;
}
/* restore state: variable is not instantiated. */
varlist->term->subst = NULL;
/* garbage collect */
termlistDelete (candlist);
return flag;
}
/*
* check whether a roledef, given some newer knowledge substitutions, can survive
*/
#define enabled_basic(sys,know,newterm) !inKnowledge(know,newterm)
//! Try to execute a read event.
/**
* Try to execute a read event. It must be able to be construct it from the
* current intruder knowledge (Inject), but not from the forbidden knowledge
* set, which we tried earlier.
*
*@returns 0 if it is not enabled, 1 if it was enabled (and routes explored)
*\sa explorify()
*/
int
matchRead_basic (const System sys, const int run,
int (*proceed) (System, int))
{
Roledef rd;
int flag = 0;
struct fvpass fp;
Termlist varlist;
int solution (struct fvpass fp, Knowledge know)
{
Knowledge oldknow;
Term newterm;
/* remove variable linkages */
newterm = termDuplicateUV (fp.roledef->message);
/* a candidate, but if this is a t4 traversal, is it also an old one? */
if (switches.traverse < 4 ||
fp.roledef->forbidden == NULL ||
enabled_basic (fp.sys, fp.roledef->forbidden, newterm))
{
/* it is possibly enabled, i.e. not forbidden */
int enabled;
oldknow = fp.sys->know;
fp.sys->know = know;
#ifdef DEBUG
if (DEBUGL (5))
{
printf ("+");
}
#endif
enabled = fp.proceed (fp.sys, fp.run); // flag determines the enabled status now
fp.sys->know = oldknow;
termDelete (newterm);
return enabled;
}
else
{
/* blocked */
#ifdef DEBUG
if (DEBUGL (5))
{
printf ("-");
}
#endif
termDelete (newterm);
return 0;
}
}
rd = runPointerGet (sys, run);
varlist = termlistAddVariables (NULL, rd->message);
fp.sys = sys;
fp.run = run;
fp.roledef = rd;
fp.proceed = proceed;
fp.solution = solution;
#ifdef DEBUG
if (DEBUGL (5))
{
indent ();
printf ("{\n");
}
#endif
flag = fixVariablelist (fp, sys->know, varlist, rd->message);
termlistDelete (varlist);
#ifdef DEBUG
if (DEBUGL (5))
{
indent ();
printf ("} with flag %i\n", flag);
}
#endif
return flag;
}
//! Skip an event
/**
* Skips over an event. Because the intruder knowledge is incremental, we can
* just overwrite the old value of forbidden.
*@returns 1
*/
int
block_basic (const System sys, const int run)
{
Knowledge pushKnow;
Roledef rd;
rd = runPointerGet (sys, run);
pushKnow = rd->forbidden;
rd->forbidden = sys->know;
traverse (sys);
rd->forbidden = pushKnow;
return 1;
}
//! Execute a send
/**
*@returns 1
*/
int
send_basic (const System sys, const int run)
{
Roledef rd = runPointerGet (sys, run);
/* execute send, push knowledge? */
if (inKnowledge (sys->know, rd->message))
{
/* no new knowledge, so this remains */
explorify (sys, run);
}
else
{
/* new knowledge, must store old state */
Knowledge oldknow = sys->know;
sys->know = knowledgeDuplicate (sys->know);
sys->knowPhase++;
knowledgeAddTerm (sys->know, rd->message);
explorify (sys, run);
sys->knowPhase--;
knowledgeDelete (sys->know);
sys->know = oldknow;
}
return 1;
}

11
src/match_basic.h
View File

@ -1,11 +0,0 @@
#ifndef MATCHBASIC
#define MATCHBASIC
int matchRead_basic (const System sys, const int run,
int (*proceed) (System, int));
int enabled_basic (const System sys, const Knowledge know,
const Term newterm);
int block_basic (const System sys, const int run);
int send_basic (const System sys, const int run);
#endif

1
src/match_clp.c
View File

@ -11,7 +11,6 @@
#include <stdio.h>
#include "match_clp.h"
#include "system.h"
#include "memory.h"
#include "constraint.h"
#include "mgu.h"
#include "memory.h"

63
src/memory.c
View File

@ -1,63 +0,0 @@
/**
*@file
* \brief Memory functions
*
* These are not really used anymore, so maybe they should be removed.
*
* \par Performance
* Tests showed that memory pooling was actually much less efficient than
* having \c malloc() trying to fit stuff into the memory caches.
*/
/* my own memory functions (not yet) */
#include <stdlib.h>
#include <stdio.h>
#include <malloc.h>
#ifdef DEBUG
#include <mcheck.h>
#endif
#include "memory.h"
#include "debug.h"
/* for displaying the sizes */
#include "term.h"
#include "termlist.h"
#include "knowledge.h"
#include "substitution.h"
#include "system.h"
//! Open memory code.
void
memInit ()
{
#ifdef DEBUG
if (DEBUGL (5))
{
void sp (char *txt, int size)
{
printf ("Size of %s : %i\n", txt, size);
}
printf ("Data structure size.\n\n");
sp ("pointer", sizeof (Term));
sp ("term node", sizeof (struct term));
sp ("termlist node", sizeof (struct termlist));
sp ("knowledge node", sizeof (struct knowledge));
sp ("substituition node", sizeof (struct substitution));
sp ("substlist node", sizeof (struct substitutionlist));
sp ("roledef node", sizeof (struct roledef));
sp ("system node", sizeof (struct system));
printf ("\n");
}
mtrace ();
#endif
return;
}
//! Close memory code.
void
memDone (int sw)
{
return;
}

35
src/memory.h
View File

@ -1,35 +0,0 @@
#ifndef MEMORY
#define MEMORY
#include "string.h"
#include "debug.h"
#include <malloc.h>
void memInit ();
void memDone ();
#define memAlloc(t) malloc(t)
#define memFree(p,t) free(p)
#define memRealloc(p,t) realloc(p,t);
#ifdef DEBUG
#define findLoserBegin(ign) int mem_before; \
int mem_diff; \
static int mem_errorcount = 0; \
struct mallinfo mi; \
mi = mallinfo(); \
mem_before = mi.uordblks - ign;
#define findLoserEnd(ign,t) mi = mallinfo(); \
mem_diff = mi.uordblks - ign - mem_before; \
if (mem_diff != 0) \
{ \
warning ("Memory leak in [%s] of %i", t, mem_diff); \
mem_errorcount++; \
if (mem_errorcount >= 1) \
error ("More than enough leaks."); \
}
#else
#define findLoserBegin(ign) ;
#define findLoserEnd(ign,t) ;
#endif
#endif

1
src/mgu.c
View File

@ -4,7 +4,6 @@
#include "termlist.h"
#include "substitution.h"
#include "mgu.h"
#include "memory.h"
#include "type.h"
#include "specialterm.h"

1458
src/modelchecker.c
View File

File diff suppressed because it is too large Load Diff

7
src/modelchecker.h
View File

@ -1,7 +0,0 @@
#define MAX_GRAPH_STATES 1000 //!< Maximum number of state space nodes drawn
int traverse (const System oldsys);
int explorify (const System sys, const int run);
int executeStep (const System sys, const int run);
int propertyCheck (const System sys);
Termlist claimViolationDetails (const System sys, const int run, const Roledef
rd, const Knowledge know);

703
src/output.c
View File

@ -1,703 +0,0 @@
/*
* output.c
*
* Outputs an attack.
* Currently, every attack is printed.
*/
#include <stdlib.h>
#include <stdio.h>
#include "system.h"
#include "latex.h"
#include "switches.h"
void
linePrint (int i)
{
indent ();
while (i > 0)
{
printf ("--------");
i--;
}
printf ("\n");
}
int
correspondingSend (const System sys, int rd)
{
int labelMatch = 0;
int toMatch = 0;
int fromMatch = 0;
int tofromMatch = 0;
int messageMatch = 0;
int nMatches = 0;
int maxNMatches = 0;
int readEvent = rd;
int sendEvent = -1;
int bestSendEvent = -1;
for (sendEvent = readEvent; sendEvent >= 0; sendEvent--)
{
if (sys->traceEvent[sendEvent]->type == SEND)
{
/* do all the different kind of matchings first */
labelMatch =
isTermEqualFn (sys->traceEvent[sendEvent]->label,
sys->traceEvent[readEvent]->label);
toMatch =
isTermEqualFn (sys->traceEvent[sendEvent]->to,
sys->traceEvent[readEvent]->to);
fromMatch =
isTermEqualFn (sys->traceEvent[sendEvent]->from,
sys->traceEvent[readEvent]->from);
tofromMatch = toMatch || fromMatch;
messageMatch =
isTermEqualFn (sys->traceEvent[sendEvent]->message,
sys->traceEvent[readEvent]->message);
/* calculate the score */
nMatches = labelMatch + tofromMatch + messageMatch;
if (nMatches == 3)
{
/* bingo! success on all matches */
//printf("Found perfect match: %d\n", s);
bestSendEvent = sendEvent;
break;
}
if (nMatches > maxNMatches)
{
/* if we found a better candidate than we already had, we'll update */
//printf("Comparing SEND #%d: ",s);
//if (labelMatch) printf("label ");
//if (toMatch) printf("to ");
//if (fromMatch) printf("from ");
//if (messageMatch) printf("message ");
//printf("\n");
/* however, we first want to be sure that at least some matches are successful */
if (labelMatch && messageMatch)
{
/* strongest restriction: message and label should match */
maxNMatches = nMatches;
bestSendEvent = sendEvent;
}
else if (messageMatch)
{
/* if label AND message don't match: */
/* at least message should match */
maxNMatches = nMatches;
bestSendEvent = sendEvent;
}
else if (labelMatch)
{
/* if message doesn't match */
/* the label should matches */
maxNMatches = nMatches;
bestSendEvent = sendEvent;
}
//printf("Best match: %d maxNMatches: %d\n", s, maxNMatches);
}
}
}
//bestSendEvent = NULL;
if (bestSendEvent == -1)
{
/*Termlist tl;
Term t;
//newtl = knowledgeNew(sys->traceKnow[i],sys->traceKnow[i+1]);
for (tl = sys->traceKnow[rd]->basic; tl != NULL; tl = tl->next)
{
t = tl->term;
termPrint(t);
printf(" - ");
}
printf("\n");
for (tl = sys->traceKnow[rd]->encrypt; tl != NULL; tl = tl->next)
{
t = tl->term;
termPrint(t);
printf(" - ");
}
printf("\n");
for (tl = sys->traceKnow[rd]->inverses; tl != NULL; tl = tl->next)
{
t = tl->term;
termPrint(t);
printf(" - ");
}
printf("\n"); */
int u;
for (u = 0; u < rd; u++)
{
if (sys->traceEvent[u]->type == SEND)
{
//termPrint(readEvent->message);
//printf("\n");
knowledgePrint (sys->traceKnow[u]);
//printf("Is received message in knowledge after SEND %d? %d\n", u, inKnowledge(sys->traceKnow[u+1],readEvent->message));
if (inKnowledge
(sys->traceKnow[u + 1],
sys->traceEvent[readEvent]->message))
{
bestSendEvent = u;
break;
}
}
}
}
if (bestSendEvent == -1)
{
printf ("!! Could not find a matching SEND\n");
}
else
{
//latexMessagePrint(sys, bestSendEvent, readEvent);
//printf("Latex: ");
//termPrint(bestSendEvent->from);
//printf(" -> ");
if (!isTermEqualFn
(sys->traceEvent[bestSendEvent]->to,
sys->traceEvent[readEvent]->to))
{
//termPrint(bestSendEvent->to);
//printf(" -> ");
}
if (!isTermEqualFn
(sys->traceEvent[bestSendEvent]->from,
sys->traceEvent[readEvent]->from))
{
//termPrint(readEvent->from);
//printf(" -> ");
}
//termPrint(readEvent->to);
//printf("\n");
}
return bestSendEvent;
}
void
tracePrint (const System sys)
{
int i, j;
int lastrid;
int width;
Termlist newtl;
void sticks (int i)
{
while (i > 0)
{
printf ("|\t");
i--;
}
}
void sticksLine (void)
{
sticks (width);
printf ("\n");
}
if (switches.latex)
{
//latexTracePrint(sys);
return;
}
/* fix the 'next' knowledge, this is required because sometimes
* when calling this function, the next knowledge is not stored
* yet, but required for the general form of the output . */
sys->traceKnow[sys->step + 1] = sys->know;
/* how wide is the trace? */
width = 0;
for (i = 0; i <= sys->step; i++)
{
if (sys->traceRun[i] >= width)
width = sys->traceRun[i] + 1;
}
linePrint (width);
indent ();
printf ("Dumping trace:\n");
linePrint (width);
/* first some parameter issues */
knowledgePrint (sys->traceKnow[0]);
/* also print inverses */
indent ();
printf ("Inverses: ");
knowledgeInversesPrint (sys->traceKnow[0]);
printf ("\n");
/* Trace columns header. First the run identifier and role. On the
* second line we have the perceived agents for each partner role.
* These are printed in the same order as the role specification in the
* protocol. */
linePrint (width);
indent ();
for (i = 0; i < width; i++)
{
termPrint (sys->runs[i].role->nameterm);
printf ("#%i\t", i);
}
printf ("\n");
for (i = 0; i < width; i++)
{
termPrint (agentOfRun (sys, i));
printf ("\t");
}
printf ("\n");
for (i = 0; i < width; i++)
{
agentsOfRunPrint (sys, i);
printf ("\t");
}
printf ("\n");
/* now we print the actual trace */
linePrint (width);
lastrid = -1;
for (i = 0; i <= sys->step; i++)
{
/* yields extra newlines between switching of runs */
j = sys->traceRun[i];
if (j != lastrid)
{
sticksLine ();
lastrid = j;
}
/* print the actual event */
indent ();
sticks (j);
roledefPrint (sys->traceEvent[i]);
//if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal)
//{
/* calls routine to find the best SEND-candidate */
/* the result is not yet being used */
// printf("\n");
// correspondingSend(sys, i);
//}
/* have we learnt anything new? */
newtl = knowledgeNew (sys->traceKnow[i], sys->traceKnow[i + 1]);
if (newtl != NULL)
{
printf ("\n");
sticksLine ();
sticks (width);
printf ("/* Intruder learns ");
termlistPrint (newtl);
termlistDelete (newtl);
printf (" */");
lastrid = -1;
}
/* new line */
printf ("\n");
}
switch (switches.clp)
{
case 1:
indent ();
printf ("---[ constraints ]-----\n");
constraintlistPrint (sys->constraints);
break;
default:
break;
}
linePrint (width);
}
void
attackDisplayAscii (const System sys)
{
int i, j;
int length;
int lastrid;
int width;
Termlist newtl;
struct tracebuf *tb;
void sticks (int i)
{
while (i > 0)
{
printf ("|\t");
i--;
}
}
void sticksLine (void)
{
sticks (width);
printf ("\n");
}
/* attack trace buffer */
tb = sys->attack;
length = sys->attack->length;
/* set variables */
varbufSet (sys, tb->variables);
/* how wide is the trace? */
width = 0;
for (i = 0; i < length; i++)
{
if (tb->run[i] >= width)
width = tb->run[i] + 1;
}
linePrint (width);
indent ();
printf ("Dumping trace:\n");
linePrint (width);
/* first some parameter issues */
knowledgePrint (tb->know[0]);
printf ("Variables: ");
termlistPrint (sys->variables);
printf ("\n");
/* Trace columns header. First the run identifier and role. On the
* second line we have the perceived agents for each partner role.
* These are printed in the same order as the role specification in the
* protocol. */
linePrint (width);
indent ();
for (i = 0; i < width; i++)
{
termPrint (sys->runs[i].role->nameterm);
printf ("#%i\t", i);
}
printf ("\n");
for (i = 0; i < width; i++)
{
termPrint (agentOfRun (sys, i));
printf ("\t");
}
printf ("\n");
for (i = 0; i < width; i++)
{
agentsOfRunPrint (sys, i);
printf ("\t");
}
printf ("\n");
/* now we print the actual trace */
linePrint (width);
lastrid = -1;
for (i = 0; i < length; i++)
{
/* yields extra newlines between switching of runs */
j = tb->run[i];
if (j != lastrid)
{
sticksLine ();
lastrid = j;
}
/* print the actual event */
indent ();
sticks (j);
roledefPrint (tb->event[i]);
//if (sys->traceEvent[i]->type == READ && !sys->traceEvent[i]->internal)
//{
/* calls routine to find the best SEND-candidate */
/* the result is not yet being used */
// printf("\n");
// correspondingSend(sys, i);
//}
/* have we learnt anything new? */
newtl = knowledgeNew (tb->know[i], tb->know[i + 1]);
if (newtl != NULL)
{
printf ("\n");
sticksLine ();
sticks (width);
printf ("/* Intruder learns ");
termlistPrint (newtl);
termlistDelete (newtl);
printf (" */");
lastrid = -1;
}
/* new line */
printf ("\n");
}
linePrint (width);
}
void
attackDisplay (const System sys)
{
if (switches.latex)
{
attackDisplayLatex (sys);
}
else
{
attackDisplayAscii (sys);
}
}
/*
*-------------------------------------------
* state space graph section
*-------------------------------------------
*/
void
graphInit (const System sys)
{
Termlist tl;
/* drawing state space. */
printf ("digraph Statespace {\n");
/* label */
printf ("\tcomment = \"$");
commandlinePrint (stdout);
printf ("\";\n");
/* fit stuff onto the page */
printf ("\trankdir=LR;\n");
printf ("\tsize=\"8.5,11\";\n");
//printf ("\tpage=\"8.5,11\";\n");
printf ("\tfontsize=\"6\";\n");
printf ("\tfontname=\"Helvetica\";\n");
printf ("\tmargin=0.5;\n");
printf ("\tnodesep=0.06;\n");
printf ("\tranksep=0.01;\n");
printf ("\torientation=landscape;\n");
printf ("\tcenter=true;\n");
// printf ("\tlabeljust=\"r\";\n");
printf ("\tconcentrate=true;\n");
/* node/edge defaults */
printf
("\tnode [shape=\"point\",fontsize=\"4\",fontname=\"Helvetica\"];\n");
printf ("\tedge [fontsize=\"4\",fontname=\"Helvetica\"];\n");
/* start with initial node 0 */
printf ("\tn");
statesFormat (STATES0);
printf (" [shape=box,height=0.2,label=\"M0: ");
tl = knowledgeSet (sys->know);
termlistPrint (tl);
termlistDelete (tl);
printf ("\"];\n");
}
void
graphDone (const System sys)
{
/* drawing state space. close up. */
printf ("}\n");
}
void
graphNode (const System sys)
{
Termlist newtl;
states_t thisNode, parentNode;
int index;
int run;
Roledef rd;
/* determine node numbers */
index = sys->step - 1;
parentNode = sys->traceNode[index];
thisNode = sys->states;
rd = sys->traceEvent[index];
run = sys->traceRun[index];
/* add node */
printf ("\tn");
statesFormat (thisNode);
printf (" [");
newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index + 1]);
if (newtl != NULL)
{
/* knowledge added */
printf ("shape=box,height=0.2,label=\"M + ");
termlistPrint (newtl);
termlistDelete (newtl);
printf ("\"");
}
else
{
/* no added knowledge */
if (switches.scenario != 0 &&
rd != NULL &&
rd == sys->runs[run].start &&
rd->type == READ && run == sys->lastChooseRun)
{
/* last choose; scenario selected */
printf ("shape=box,height=0.2,label=\"Scenario %i: ",
sys->countScenario);
scenarioPrint (sys);
printf ("\"");
}
else
{
printf ("label=\"\"");
}
}
printf ("];\n");
/* add edge */
printf ("\tn");
statesFormat (parentNode);
printf (" -> n");
statesFormat (thisNode);
/* add label */
printf (" [label=\"");
// Print step
printf ("%i:", sys->runs[run].step - 1);
if (rd->type == CLAIM && (!isRunTrusted (sys, run)))
{
printf ("Skip claim in #%i\"", run);
}
else
{
// Print event
roledefPrint (rd);
printf ("#%i\"", run);
if (rd->type == CLAIM)
{
printf (",shape=house,color=green");
}
}
/* a choose? */
if (rd->type == READ && rd->internal)
{
printf (",color=blue");
//printf (",style=dotted");
}
printf ("]");
printf (";\n");
}
void
graphNodePath (const System sys, const int length, const char *nodepar)
{
int i;
states_t thisNode;
i = 0;
while (i < length)
{
/* determine node number */
thisNode = sys->traceNode[i];
/* color node */
printf ("\tn");
statesFormat (thisNode);
printf (" [%s];\n", nodepar);
i++;
}
}
void
graphEdgePath (const System sys, const int length, const char *edgepar)
{
int i;
states_t thisNode, prevNode;
i = 0;
prevNode = sys->traceNode[i];
while (i < length)
{
/* determine node number */
thisNode = sys->traceNode[i + 1];
/* color edge */
printf ("\tn");
statesFormat (prevNode);
printf (" -> n");
statesFormat (thisNode);
printf (" [%s];\n", edgepar);
prevNode = thisNode;
i++;
}
}
void
graphPath (const System sys, int length)
{
graphNodePath (sys, length, "style=bold,color=red");
graphEdgePath (sys, length - 1, "style=bold,color=red");
}
//! Scenario for graph; bit of a hack
void
graphScenario (const System sys, const int run, const Roledef rd)
{
/* Add scenario node */
printf ("\ts%i [shape=box,height=0.2,label=\"Scenario %i: ",
sys->countScenario, sys->countScenario);
scenarioPrint (sys);
printf ("\"];\n");
/* draw edge */
printf ("\tn%i -> s%i", sys->traceNode[sys->step], sys->countScenario);
printf (" [color=blue,label=\"");
printf ("%i:", sys->runs[run].step);
roledefPrint (rd);
printf ("#%i", run);
printf ("\"];\n");
}

16
src/output.h
View File

@ -1,16 +0,0 @@
#ifndef OUTPUT
#define OUTPUT
#include "system.h"
void tracePrint (const System sys);
void attackDisplay (const System sys);
void graphInit (const System sys);
void graphDone (const System sys);
void graphNode (const System sys);
void graphNodePath (const System sys, const int length, const char *nodepar);
void graphEdgePath (const System sys, const int length, const char *edgepar);
void graphPath (const System sys, int length);
void graphScenario (const System sys, const int run, const Roledef rd);
#endif

76
src/report.c
View File

@ -1,76 +0,0 @@
#include <stdio.h>
#include <stdlib.h>
#include "term.h"
#include "system.h"
#include "debug.h"
#include "output.h"
#include "switches.h"
extern int globalLatex;
/* reportQuit is called after each violation, because it might need to abort the process */
void
reportQuit (const System sys)
{
/* determine quit or not */
if (switches.prune >= 3)
{
indent ();
printf ("Quitting after %li claims, at the first violated claim.\n",
sys->claims);
sys->maxtracelength = 0;
}
}
void
reportStart (const System sys)
{
if (!switches.latex)
{
indent ();
printf ("<REPORT>\n");
indent ();
}
statesPrint (sys);
}
void
reportMid (const System sys)
{
indent ();
printf ("Trace length %i.\n", 1 + sys->step);
if (globalLatex)
printf ("\n");
tracePrint (sys);
}
void
reportEnd (const System sys)
{
if (!switches.latex)
{
indent ();
printf ("<REPORT>\n");
}
reportQuit (sys);
}
void
reportSecrecy (const System sys, Term t)
{
if (switches.output != ATTACK)
{
reportQuit (sys);
return;
}
reportStart (sys);
indent ();
printf ("Secrecy violation of $");
termPrint (t);
printf ("$\n");
if (globalLatex)
printf ("\n");
reportMid (sys);
reportEnd (sys);
}

6
src/report.h
View File

@ -1,6 +0,0 @@
#ifndef REPORT
#define REPORT
void reportSecrecy (const System sys, Term t);
#endif

28
src/role.c
View File

@ -4,26 +4,22 @@
*/
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <limits.h>
#include "term.h"
#include "termlist.h"
#include "knowledge.h"
#include "system.h"
#include "memory.h"
#include "constraint.h"
#include "debug.h"
#include "output.h"
#include "tracebuf.h"
#include "role.h"
extern int globalLatex; // from system.c
extern int protocolCount; // from system.c
//! Allocate memory the size of a roledef struct.
Roledef
makeRoledef ()
{
return (Roledef) memAlloc (sizeof (struct roledef));
return (Roledef) malloc (sizeof (struct roledef));
}
//! Print a role event.
@ -71,21 +67,9 @@ roledefPrintGeneric (Roledef rd, int print_actor)
label = TermOp2 (label);
}
//! Print latex/normal
if (globalLatex)
{
eprintf ("$_{");
termPrint (label);
eprintf ("}$");
}
else
{
eprintf ("_");
termPrint (label);
}
}
if (globalLatex)
eprintf ("$");
eprintf ("(");
if (!(rd->from == NULL && rd->to == NULL))
{
@ -104,8 +88,6 @@ roledefPrintGeneric (Roledef rd, int print_actor)
}
termPrint (rd->message);
eprintf (" )");
if (globalLatex)
eprintf ("$");
}
//! Print a roledef
@ -166,7 +148,7 @@ roledefDelete (Roledef rd)
if (rd == NULL)
return;
roledefDelete (rd->next);
memFree (rd, sizeof (struct roledef));
free (rd);
return;
}
@ -180,7 +162,7 @@ roledefDestroy (Roledef rd)
termDelete (rd->from);
termDelete (rd->to);
termDelete (rd->message);
memFree (rd, sizeof (struct roledef));
free (rd);
return;
}
@ -237,7 +219,7 @@ roleCreate (Term name)
{
Role r;
r = memAlloc (sizeof (struct role));
r = malloc (sizeof (struct role));
r->nameterm = name;
r->roledef = NULL;
r->locals = NULL;

1
src/role.h
View File

@ -5,7 +5,6 @@
#include "termmap.h"
#include "termlist.h"
#include "knowledge.h"
#include "constraint.h"
#include "states.h"
enum eventtype

8
src/scanner.l
View File

@ -122,8 +122,8 @@ Symbol mkstring(char *name)
}
// make new name
len = strlen(name);
s = (char *)memAlloc(len+1);
sl = (Stringlist) memAlloc(sizeof(struct stringlist));
s = (char *)malloc(len+1);
sl = (Stringlist) malloc(sizeof(struct stringlist));
strncpy(s,name,len);
sl->next = allocatedStrings;
allocatedStrings = sl;
@ -151,8 +151,8 @@ void strings_cleanup(void)
{
sl = allocatedStrings;
allocatedStrings = sl->next;
memFree(sl->string, strlen(sl->string)+1);
memFree(sl, sizeof(struct stringlist));
free(sl->string);
free(sl);
}
}

81
src/switches.c
View File

@ -5,18 +5,16 @@
* Contains the main switch handling.
*/
#include "string.h"
#include <stdlib.h>
#include <string.h>
#include <limits.h>
#include "system.h"
#include "debug.h"
#include "version.h"
#include "timer.h"
#include "switches.h"
#include "error.h"
#include "string.h"
#include "specialterm.h"
#include "memory.h"
#include <limits.h>
#include <stdlib.h>
struct switchdata switches;
@ -37,9 +35,7 @@ void
switchesInit (int argc, char **argv)
{
// Methods
switches.engine = ARACHNE_ENGINE; // default is arachne engine
switches.match = 0; // default matching
switches.clp = 0;
switches.tupling = 0;
// Pruning and Bounding
@ -50,20 +46,6 @@ switchesInit (int argc, char **argv)
switches.filterClaim = NULL; // default check all claims
switches.maxAttacks = 0; // no maximum default
// Modelchecker
switches.traverse = 12; // default traversal method
switches.forceChoose = 1; // force explicit chooses by default
switches.chooseFirst = 0; // no priority to chooses by default
switches.readSymmetries = 0; // don't force read symmetries by default
switches.agentSymmetries = 1; // default enable agent symmetry
switches.orderSymmetries = 0; // don't force symmetry order reduction by default
switches.pruneNomoreClaims = 1; // default cutter when there are no more claims
switches.reduceEndgame = 1; // default cutter of last events in a trace
switches.reduceClaims = 1; // default remove claims from duplicate instance choosers
// Parallellism
switches.scenario = 0;
switches.scenarioSize = 0;
// Arachne
switches.heuristic = 3; // default goal selection method
switches.maxIntruderActions = INT_MAX; // max number of encrypt/decrypt events
@ -95,9 +77,6 @@ switchesInit (int argc, char **argv)
switches.extendTrivial = 0; // default off
switches.plain = false; // default colors
// Obsolete
switches.latex = 0; // latex output?
// Process the environment variable SCYTHERFLAGS
process_environment ();
// Process the command-line switches
@ -147,7 +126,7 @@ openFileStdin (char *filename)
nameindex++;
}
buffer = (char *) memAlloc (buflen);
buffer = (char *) malloc (buflen);
memcpy (buffer, prefix, prefixlen);
memcpy (buffer + nameindex, filename, namelen);
buffer[buflen - 1] = '\0';
@ -164,7 +143,7 @@ openFileStdin (char *filename)
result = true;
}
memFree (buffer, buflen);
free (buffer);
return result;
}
@ -379,41 +358,6 @@ switcher (const int process, int index, int commandline)
/* ==================
* Generic options
*/
if (detect (' ', "arachne", 0))
{
if (!process)
{
/*
* Obsolete switch, as it is now the default behaviour.
*/
}
else
{
// Select arachne engine
switches.engine = ARACHNE_ENGINE;
return index;
}
}
if (detect (' ', "modelchecker", 0))
{
if (!process)
{
/*
* Discourage
*
helptext (" --modelchecker",
"select Model checking engine [Arachne]");
*/
}
else
{
// Select arachne engine
switches.engine = POR_ENGINE;
return index;
}
}
if (detect ('d', "dot-output", 0))
{
if (!process)
@ -786,19 +730,6 @@ switcher (const int process, int index, int commandline)
/* obsolete, worked for modelchecker
*
if (detect (' ', "latex", 0))
{
if (!process)
{
helptext (" --latex", "output attacks in LaTeX format [ASCII]");
}
else
{
switches.latex = 1;
return index;
}
}
if (detect (' ', "state-space", 0))
{
if (!process)
@ -1225,7 +1156,7 @@ process_environment (void)
char *argn;
/* make a safe copy */
args = (char *) memAlloc (slen + 1);
args = (char *) malloc (slen + 1);
memcpy (args, flags, slen + 1);
/* warning */

23
src/switches.h
View File

@ -15,9 +15,7 @@ struct switchdata
char **argv;
// Methods
int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE)
int match; //!< Matching type.
int clp; //!< Do we use clp?
int tupling; //!< Tupling is by default 0: right-associative, optionally 1: left-associative.
// Pruning and Bounding
@ -28,20 +26,6 @@ struct switchdata
Term filterClaim; //!< Which claim should be checked?
int maxAttacks; //!< When not 0, maximum number of attacks
// Modelchecker
int traverse; //!< Traversal method
int forceChoose; //!< Force chooses for each run, even if involved in first read
int chooseFirst; //!< Priority to chooses, implicit and explicit
int readSymmetries; //!< Enable read symmetry reduction
int agentSymmetries; //!< Enable agent symmetry reduction
int orderSymmetries; //!< Enable symmetry order reduction
int pruneNomoreClaims; //!< Enable no more claims cutter
int reduceEndgame; //!< Enable endgame cutter
int reduceClaims; //!< Symmetry reduction on claims (only works when switchAgentSymm is true)
// Parallellism
int scenario; //!< -1 to count, 0 for disable, 1-n to select the choose scenario
int scenarioSize; //!< Scenario size, also called fixed trace prefix length
// Arachne
int heuristic; //!< Goal selection method for Arachne engine
int maxIntruderActions; //!< Maximum number of intruder actions in the semitrace (encrypt/decrypt)
@ -72,13 +56,6 @@ struct switchdata
int extendNonReads; //!< Show further events in arachne xml output.
int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
int plain; //!< Disable color output
//! Latex output switch.
/**
* Obsolete. Use globalLatex instead.
*\sa globalLatex
*/
int latex;
};
extern struct switchdata switches; //!< pointer to switchdata structure

11
src/symbol.c
View File

@ -1,11 +1,11 @@
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include <string.h>
#include <limits.h>
#include "symbol.h"
#include "debug.h"
#include "memory.h"
/*
Symbol processor.
@ -59,7 +59,7 @@ symbolsDone (void)
{
s = symb_alloc;
symb_alloc = s->allocnext;
memFree (s, sizeof (struct symbol));
free (s);
}
}
@ -79,7 +79,7 @@ get_symb (void)
}
else
{
t = (Symbol) memAlloc (sizeof (struct symbol));
t = (Symbol) malloc (sizeof (struct symbol));
t->allocnext = symb_alloc;
symb_alloc = t;
}
@ -225,13 +225,14 @@ symbolNextFree (Symbol prefixsymbol)
if (prefixsymbol != NULL)
{
prefixstr = (char *) prefixsymbol->text;
len = strlen (prefixstr);
}
else
{
prefixstr = "";
len = 0;
}
len = strlen (prefixstr);
n = 1;
while (n <= 9999)
{
@ -250,7 +251,7 @@ symbolNextFree (Symbol prefixsymbol)
* Thus, some precaution is necessary.
* [x][CC]
*/
newstring = (char *) memAlloc (slen + 1);
newstring = (char *) malloc (slen + 1);
memcpy (newstring, buffer, slen + 1);
/* This persistent string can be used to return a fresh symbol */

294
src/system.c
View File

@ -9,11 +9,7 @@
#include "termlist.h"
#include "knowledge.h"
#include "system.h"
#include "memory.h"
#include "constraint.h"
#include "debug.h"
#include "output.h"
#include "tracebuf.h"
#include "role.h"
#include "mgu.h"
#include "switches.h"
@ -21,12 +17,6 @@
#include "depend.h"
#include "specialterm.h"
//! Global flag that signals LaTeX output.
/**
* True iff LaTeX output is desired.
*/
int globalLatex;
//! Global count of protocols
int protocolCount;
@ -42,7 +32,7 @@ static int indentDepth = 0;
Run
makeRun ()
{
return (Run) memAlloc (sizeof (struct run));
return (Run) malloc (sizeof (struct run));
}
@ -54,12 +44,11 @@ makeRun ()
System
systemInit ()
{
System sys = (System) memAlloc (sizeof (struct system));
System sys = (System) malloc (sizeof (struct system));
/* initially, no trace ofcourse */
sys->step = 0;
sys->shortestattack = INT_MAX;
sys->attack = tracebufInit ();
sys->maxtracelength = INT_MAX;
/* init rundefs */
@ -75,7 +64,6 @@ systemInit ()
sys->hidden = NULL;
sys->secrets = NULL; // list of claimed secrets
sys->synchronising_labels = NULL;
sys->attack = NULL; // clash with prev. attack declaration TODO
/* no protocols => no protocol preprocessed */
sys->rolecount = 0;
sys->roleeventmax = 0;
@ -83,14 +71,7 @@ systemInit ()
sys->labellist = NULL;
sys->attackid = 0; // First attack will have id 1, because the counter is increased before any attacks are displayed.
/* matching CLP */
sys->constraints = NULL; // no initial constraints
/* Arachne assist */
if (switches.engine == ARACHNE_ENGINE)
{
bindingInit (sys);
}
sys->bindings = NULL;
sys->current_claim = NULL;
@ -126,23 +107,12 @@ systemReset (const System sys)
cl = cl->next;
}
sys->knowPhase = 0; // knowledge transition id
termlistDestroy (sys->secrets); // remove old secrets list
sys->secrets = NULL; // list of claimed secrets
/* transfer switches */
sys->maxtracelength = switches.maxtracelength;
/* POR init */
sys->PORphase = -1;
sys->PORdone = 1; // mark as 'something done' with previous reads
/* global latex switch: ugly, but otherwise I must carry it into every
* single subprocedure such as termPrint */
globalLatex = switches.latex;
/* propagate mgu_mode */
setMguMode (switches.match);
@ -188,10 +158,10 @@ systemDone (const System sys)
/* clear globals, which were defined in systemStart */
s = sys->maxtracelength + 1;
memFree (sys->traceEvent, s * sizeof (Roledef));
memFree (sys->traceRun, s * sizeof (int));
memFree (sys->traceKnow, s * sizeof (Knowledge));
memFree (sys->traceNode, s * sizeof (states_t));
free (sys->traceEvent);
free (sys->traceRun);
free (sys->traceKnow);
free (sys->traceNode);
/* clear roledefs */
while (sys->maxruns > 0)
@ -201,10 +171,7 @@ systemDone (const System sys)
/* undo bindings (for arachne) */
if (switches.engine == ARACHNE_ENGINE)
{
bindingDone ();
}
/* clear substructures */
termlistDestroy (sys->secrets);
@ -226,8 +193,6 @@ statesPrint (const System sys)
{
statesFormat (sys->states);
eprintf (" states traversed.\n");
if (globalLatex)
eprintf ("\n");
}
//! Destroy a system memory block and system::runs
@ -238,8 +203,8 @@ statesPrint (const System sys)
void
systemDestroy (const System sys)
{
memFree (sys->runs, sys->maxruns * sizeof (struct run));
memFree (sys, sizeof (struct system));
free (sys->runs);
free (sys);
}
//! Ensures that a run can be added to the system.
@ -263,8 +228,7 @@ ensureValidRun (const System sys, int run)
/* update size parameter */
oldsize = sys->maxruns;
sys->maxruns = run + 1;
sys->runs =
(Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns));
sys->runs = (Run) realloc (sys->runs, sizeof (struct run) * (sys->maxruns));
/* create runs, set the new pointer(s) to NULL */
for (i = oldsize; i < sys->maxruns; i++)
@ -282,15 +246,7 @@ ensureValidRun (const System sys, int run)
myrun.artefacts = NULL;
myrun.substitutions = NULL;
if (switches.engine == POR_ENGINE)
{
myrun.know = knowledgeDuplicate (sys->know);
}
else
{
// Arachne etc.
myrun.know = NULL;
}
myrun.prevSymmRun = -1;
myrun.firstNonAgentRead = -1;
@ -366,40 +322,6 @@ not_read_first (const Roledef rdstart, const Term t)
Term
agentOfRunRole (const System sys, const int run, const Term role)
{
if (switches.engine != ARACHNE_ENGINE)
{
// Non-arachne
Termlist roles;
Termlist agents;
roles = sys->runs[run].protocol->rolenames;
agents = sys->runs[run].agents;
/* TODO stupid reversed order, lose that soon */
if (agents != NULL)
{
agents = termlistForward (agents);
while (agents != NULL && roles != NULL)
{
if (isTermEqual (roles->term, role))
{
return agents->term;
}
agents = agents->prev;
roles = roles->next;
}
}
else
{
error
("Agent list for run %i is empty, so agentOfRunRole is not usable.",
run);
}
return NULL;
}
else
{
// Arachne engine
Termlist agents;
// Agent variables have the same symbol as the role names, so
@ -420,7 +342,6 @@ agentOfRunRole (const System sys, const int run, const Term role)
}
}
return NULL;
}
}
//! Yield the actor agent of a run in the system.
@ -837,148 +758,9 @@ roleInstanceArachne (const System sys, const Protocol protocol,
}
//! Instantiate a role by making a new run for the Modelchecker
/**
* This involves creation of a new run(id).
* Copy & subst of Roledef, Agent knowledge.
* Tolist might contain type constants.
*/
void
roleInstanceModelchecker (const System sys, const Protocol protocol,
const Role role, const Termlist paramlist,
Termlist substlist)
{
int rid;
Run runs;
Roledef rd;
Termlist scanfrom, scanto;
Termlist fromlist = NULL;
Termlist tolist = NULL;
Termlist artefacts = NULL;
Term extterm = NULL;
/* claim runid, allocate space */
rid = sys->maxruns;
ensureValidRun (sys, rid);
runs = sys->runs;
/* duplicate roledef in buffer rd */
rd = roledefDuplicate (role->roledef);
/* set parameters */
/* generic setup */
runs[rid].protocol = protocol;
runs[rid].role = role;
runs[rid].step = 0;
runs[rid].firstReal = 0;
/* scan for types in agent list */
/* scanners */
// Default engine adheres to scenario
scanfrom = protocol->rolenames;
scanto = paramlist;
while (scanfrom != NULL && scanto != NULL)
{
fromlist = termlistAdd (fromlist, scanfrom->term);
if (scanto->term->stype != NULL &&
inTermlist (scanto->term->stype, TERM_Type))
{
Term newvar;
/* There is a TYPE constant in the parameter list.
* Generate a new local variable for this run, with this type */
newvar = makeTermType (VARIABLE, TermSymb (scanfrom->term), rid);
artefacts = termlistAdd (artefacts, newvar);
sys->variables = termlistAdd (sys->variables, newvar);
newvar->stype = termlistAdd (NULL, scanto->term);
tolist = termlistAdd (tolist, newvar);
/* newvar is apparently new, but it might occur
* in the first event if it's a read, in which
* case we forget it */
if (switches.forceChoose || not_read_first (rd, scanfrom->term))
{
/* this term is forced as a choose, or it does not occur in the (first) read event */
if (extterm == NULL)
{
extterm = newvar;
}
else
{
extterm = makeTermTuple (newvar, extterm);
artefacts = termlistAdd (artefacts, extterm);
}
}
}
else
{
/* not a type constant, add to list */
tolist = termlistAdd (tolist, scanto->term);
}
scanfrom = scanfrom->next;
scanto = scanto->next;
}
/* set agent list */
runs[rid].agents = termlistDuplicate (tolist);
run_prefix_read (sys, rid, rd, extterm);
/* duplicate all locals form this run */
scanto = role->locals;
while (scanto != NULL)
{
Term t = scanto->term;
if (!inTermlist (fromlist, t))
{
Term newt;
newt = create_new_local (t, rid);
if (newt != NULL)
{
artefacts = termlistAdd (artefacts, newt);
if (realTermVariable (newt))
{
sys->variables = termlistAdd (sys->variables, newt);
}
fromlist = termlistAdd (fromlist, t);
tolist = termlistAdd (tolist, newt);
}
}
scanto = scanto->next;
}
/* TODO this is not what we want yet, also local knowledge. The local
* knowledge (list?) also needs to be substituted on invocation. */
runs[rid].know = knowledgeDuplicate (sys->know);
/* now adjust the local run copy */
run_localize (sys, rid, fromlist, tolist, substlist);
termlistDelete (fromlist);
runs[rid].locals = tolist;
runs[rid].artefacts = artefacts;
/* erase any substitutions in the role definition, as they are now copied */
termlistSubstReset (role->variables);
if (switches.engine == POR_ENGINE)
{
/* Determine symmetric run */
runs[rid].prevSymmRun = staticRunSymmetry (sys, rid); // symmetry reduction static analysis
/* Determine first read with variables besides agents */
runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid); // symmetry reduction type II
}
/* length */
runs[rid].rolelength = roledef_length (runs[rid].start);
}
//! Instantiate a role by making a new run
/**
* Generic splitter. Splits into the arachne version, or the modelchecker version.
* Just forwards to Arachne version.
*
* This involves creation of a new run(id).
* Copy & subst of Roledef, Agent knowledge.
@ -988,14 +770,7 @@ void
roleInstance (const System sys, const Protocol protocol, const Role role,
const Termlist paramlist, Termlist substlist)
{
if (switches.engine == ARACHNE_ENGINE)
{
roleInstanceArachne (sys, protocol, role, paramlist, substlist);
}
else
{
roleInstanceModelchecker (sys, protocol, role, paramlist, substlist);
}
}
//! Destroy roleInstance
@ -1015,10 +790,7 @@ roleInstanceDestroy (const System sys)
myrun = sys->runs[runid];
// Reset graph
if (switches.engine == ARACHNE_ENGINE)
{
dependPopRun ();
}
// Destroy roledef
roledefDestroy (myrun.start);
@ -1056,17 +828,14 @@ roleInstanceDestroy (const System sys)
* Arachne does real-time reduction of memory, POR does not
* Artefact removal can only be done if knowledge sets are empty, as with Arachne
*/
if (switches.engine == ARACHNE_ENGINE)
{
Termlist artefacts;
// Remove artefacts
artefacts = myrun.artefacts;
while (artefacts != NULL)
{
memFree (artefacts->term, sizeof (struct term));
free (artefacts->term);
artefacts = artefacts->next;
}
}
/**
* Undo the local copies of the substitutions. We cannot restore them however, so this might
@ -1096,7 +865,7 @@ roleInstanceDestroy (const System sys)
// Reduce run count
sys->maxruns = sys->maxruns - 1;
sys->runs =
(Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns));
(Run) realloc (sys->runs, sizeof (struct run) * (sys->maxruns));
}
}
@ -1132,10 +901,10 @@ systemStart (const System sys)
s = sys->maxtracelength + 1;
/* freed in systemDone */
sys->traceEvent = memAlloc (s * sizeof (Roledef));
sys->traceRun = memAlloc (s * sizeof (int));
sys->traceKnow = memAlloc (s * sizeof (Knowledge));
sys->traceNode = memAlloc (s * sizeof (states_t));
sys->traceEvent = malloc (s * sizeof (Roledef));
sys->traceRun = malloc (s * sizeof (int));
sys->traceKnow = malloc (s * sizeof (Knowledge));
sys->traceNode = malloc (s * sizeof (states_t));
/* clear, for niceties */
for (i = 0; i < s; i++)
@ -1182,7 +951,7 @@ protocolCreate (Term name)
{
Protocol p;
p = memAlloc (sizeof (struct protocol));
p = malloc (sizeof (struct protocol));
p->nameterm = name;
p->roles = NULL;
p->rolenames = NULL;
@ -1358,35 +1127,6 @@ violatedClaimPrint (const System sys, const int i)
eprintf ("Claim stuk");
}
//! Yield the real length of an attack.
/**
* AttackLength yields the real (user friendly) length of an attack by omitting
* the redundant events but also the choose events.
*/
int
attackLength (struct tracebuf *tb)
{
int len, i;
len = 0;
i = 0;
while (i < tb->length)
{
if (tb->status[i] != S_RED)
{
/* apparently not redundant */
if (!(tb->event[i]->type == READ && tb->event[i]->internal))
{
/* and no internal read, so it counts */
len++;
}
}
i++;
}
return len;
}
void
commandlinePrint (FILE * stream)
{

39
src/system.h
View File

@ -5,7 +5,6 @@
#include "termmap.h"
#include "termlist.h"
#include "knowledge.h"
#include "constraint.h"
#include "states.h"
#include "role.h"
#include "list.h"
@ -73,34 +72,6 @@ struct varbuf
//! Shorthand for varbuf pointer.
typedef struct varbuf *Varbuf;
//! Trace buffer.
struct tracebuf
{
//! Length of trace.
int length;
//! Length of trace minus the redundant events.
int reallength;
//! Array of events.
Roledef *event;
//! Array of run identifiers for each event.
int *run;
//! Array of status flags for each event.
/**
*\sa S_OKE, S_RED, S_TOD, S_UNK
*/
int *status;
//! Array for matching sends to reads.
int *link;
//! Index of violated claim in trace.
int violatedclaim;
//! Array of knowledge sets for each event.
Knowledge *know;
//! List of terms required to be in the final knowledge.
Termlist requiredterms;
//! List of variables in the system.
Varbuf variables;
};
//! Structure for information on special terms (cacheing)
struct hiddenterm
{
@ -166,18 +137,9 @@ struct system
Knowledge *traceKnow; //!< Trace intruder knowledge: Maxruns * maxRoledef
states_t *traceNode; //!< Trace node traversal: Maxruns * maxRoledef
/* POR reduction assistance */
int PORphase; //!< -1: init (all sends), 0...: recurse reads
int PORdone; //!< Simple bit to denote something was done.
int knowPhase; //!< Which knowPhase have we already explored?
Constraintlist constraints; //!< Only needed for CLP match
/* Arachne assistance */
List bindings; //!< List of bindings
Claimlist current_claim; //!< The claim under current investigation
//! Shortest attack storage.
struct tracebuf *attack;
};
typedef struct system *System;
@ -212,7 +174,6 @@ int untrustedAgent (const System sys, Termlist agents);
int getMaxTraceLength (const System sys);
void agentsOfRunPrint (const System sys, const int run);
void violatedClaimPrint (const System sys, int i);
int attackLength (struct tracebuf *tb);
void commandlinePrint (FILE * stream);
int compute_rolecount (const System sys);

4
src/tac.c
View File

@ -27,7 +27,7 @@ tacDone (void)
tf = ts;
ts = ts->allnext;
memFree (tf, sizeof (struct tacnode));
free (tf);
}
}
@ -37,7 +37,7 @@ tacCreate (int op)
{
/* maybe even store in scrapping list, so we could delete them
* all later */
Tac t = memAlloc (sizeof (struct tacnode));
Tac t = malloc (sizeof (struct tacnode));
t->allnext = allocatedTacs;
allocatedTacs = t;
t->lineno = yylineno;

35
src/term.c
View File

@ -10,13 +10,12 @@
* pointer comparison, which is what we want.
*/
#include <string.h>
#include <stdlib.h>
#include <stdio.h>
#include <limits.h>
#include <string.h>
#include "term.h"
#include "debug.h"
#include "memory.h"
#include "ctype.h"
#include "specialterm.h"
@ -26,7 +25,6 @@ int rolelocal_variable;
/* external definitions */
extern int inTermlist (); // suppresses a warning, but at what cost?
extern int globalLatex;
/* forward declarations */
@ -63,7 +61,7 @@ termsDone (void)
Term
makeTerm ()
{
return (Term) memAlloc (sizeof (struct term));
return (Term) malloc (sizeof (struct term));
}
//! Create a fresh encrypted term from two existing terms.
@ -335,16 +333,10 @@ termPrint (Term term)
eprintf ("V");
if (TermRunid (term) >= 0)
{
if (globalLatex && globalError == 0)
eprintf ("\\sharp%i", TermRunid (term));
else
eprintf ("#%i", TermRunid (term));
}
if (term->subst != NULL)
{
if (globalLatex)
eprintf ("\\rightarrow");
else
eprintf ("->");
termPrint (term->subst);
}
@ -370,23 +362,12 @@ termPrint (Term term)
else
{
/* normal encryption */
if (globalLatex)
{
eprintf ("\\{");
termTuplePrint (TermOp (term));
eprintf ("\\}_{");
termPrint (TermKey (term));
eprintf ("}");
}
else
{
eprintf ("{");
termTuplePrint (TermOp (term));
eprintf ("}");
termPrint (TermKey (term));
}
}
}
}
//! Print an inner (tuple) term to stdout, without brackets.
@ -432,7 +413,7 @@ termDuplicate (const Term term)
if (realTermLeaf (term))
return term;
newterm = (Term) memAlloc (sizeof (struct term));
newterm = (Term) malloc (sizeof (struct term));
memcpy (newterm, term, sizeof (struct term));
if (realTermEncrypt (term))
{
@ -464,7 +445,7 @@ termNodeDuplicate (const Term term)
if (realTermLeaf (term))
return term;
newterm = (Term) memAlloc (sizeof (struct term));
newterm = (Term) malloc (sizeof (struct term));
memcpy (newterm, term, sizeof (struct term));
return newterm;
}
@ -485,7 +466,7 @@ termDuplicateDeep (const Term term)
if (term == NULL)
return NULL;
newterm = (Term) memAlloc (sizeof (struct term));
newterm = (Term) malloc (sizeof (struct term));
memcpy (newterm, term, sizeof (struct term));
if (!realTermLeaf (term))
{
@ -519,7 +500,7 @@ termDuplicateUV (Term term)
if (realTermLeaf (term))
return term;
newterm = (Term) memAlloc (sizeof (struct term));
newterm = (Term) malloc (sizeof (struct term));
memcpy (newterm, term, sizeof (struct term));
if (realTermEncrypt (term))
{
@ -543,7 +524,7 @@ realTermDuplicate (const Term term)
if (term == NULL)
return NULL;
newterm = (Term) memAlloc (sizeof (struct term));
newterm = (Term) malloc (sizeof (struct term));
if (realTermLeaf (term))
{
memcpy (newterm, term, sizeof (struct term));
@ -587,7 +568,7 @@ termDelete (const Term term)
termDelete (TermOp1 (term));
termDelete (TermOp2 (term));
}
memFree (term, sizeof (struct term));
free (term);
}
}

9
src/termlist.c
View File

@ -3,7 +3,6 @@
#include "termlist.h"
#include "specialterm.h"
#include "debug.h"
#include "memory.h"
/*
* Shared stuff
@ -45,7 +44,7 @@ Termlist
makeTermlist ()
{
/* inline candidate */
return (Termlist) memAlloc (sizeof (struct termlist));
return (Termlist) malloc (sizeof (struct termlist));
}
//! Duplicate a termlist.
@ -113,7 +112,7 @@ termlistDelete (Termlist tl)
}
#endif
termlistDelete (tl->next);
memFree (tl, sizeof (struct termlist));
free (tl);
}
@ -129,7 +128,7 @@ termlistDestroy (Termlist tl)
return;
termlistDestroy (tl->next);
termDelete (tl->term);
memFree (tl, sizeof (struct termlist));
free (tl);
}
//! Determine whether a term is an element of a termlist.
@ -345,7 +344,7 @@ termlistDelTerm (Termlist tl)
}
if (tl->next != NULL)
(tl->next)->prev = tl->prev;
memFree (tl, sizeof (struct termlist));
free (tl);
return newhead;
}

5
src/termmap.c
View File

@ -2,7 +2,6 @@
#include <stdio.h>
#include "termmap.h"
#include "debug.h"
#include "memory.h"
//! Open termmaps code.
void
@ -26,7 +25,7 @@ Termmap
makeTermmap (void)
{
/* inline candidate */
return (Termmap) memAlloc (sizeof (struct termmap));
return (Termmap) malloc (sizeof (struct termmap));
}
//! Get function result
@ -102,7 +101,7 @@ termmapDelete (const Termmap f)
if (f != NULL)
{
termmapDelete (f->next);
memFree (f, sizeof (struct termmap));
free (f);
}
}

202
src/tracebuf.c
View File

@ -1,202 +0,0 @@
/*
* tracebuf.c
*
* trace buffer operations
*/
#include <stdio.h>
#include <stdlib.h>
#include "system.h"
#include "memory.h"
#include "tracebuf.h"
#include "varbuf.h"
/* reconstruct the knowledge sequence, -1 if it can be done, event nr of last depending read otherwise.
* There is one exception: if it returns tb->length, the required terms are not in the last knowledge
*/
int
tracebufRebuildKnow (struct tracebuf *tb)
{
Knowledge k;
Roledef rd;
int i;
int flag;
Termlist tl;
if (tb == NULL || tb->length == 0)
{
/* stupid, but true */
return -1;
}
flag = -1;
k = knowledgeDuplicate (tb->know[0]);
i = 0;
while (i < tb->length)
{
rd = tb->event[i];
if (tb->status[i] != S_RED)
{
/* simulate execution of the event */
switch (rd->type)
{
case READ:
if (!inKnowledge (k, rd->message))
{
flag = i;
}
break;
case SEND:
knowledgeAddTerm (k, rd->message);
break;
case CLAIM:
/* TODO parse term requirements ? */
/* Probably not needed */
break;
default:
/* Anything else */
break;
}
}
/* write the new knowledge, overwriting old stuff */
knowledgeDelete (tb->know[i + 1]);
tb->know[i + 1] = knowledgeDuplicate (k);
i++;
}
tl = tb->requiredterms;
while (tl != NULL)
{
if (!inKnowledge (k, tl->term))
{
flag = tb->length;
}
tl = tl->next;
}
knowledgeDelete (k);
return flag;
}
/*
* traceBufInit
*
* initializes the trace buffer.
*/
struct tracebuf *
tracebufInit (void)
{
struct tracebuf *tb =
(struct tracebuf *) memAlloc (sizeof (struct tracebuf));
tb->length = 0;
tb->reallength = 0;
tb->event = NULL;
tb->know = NULL;
tb->run = NULL;
tb->status = NULL;
tb->link = NULL;
tb->requiredterms = NULL;
tb->violatedclaim = 0;
tb->variables = NULL;
return tb;
}
void
tracebufDone (struct tracebuf *tb)
{
Roledef rd;
if (tb == NULL)
{
return;
}
varbufDone (tb->variables);
if (tb->length > 0)
{
int i;
i = 0;
/* note: knowledge domain is length+1 */
knowledgeDelete (tb->know[0]);
while (i < tb->length)
{
rd = tb->event[i];
termDelete (rd->from);
termDelete (rd->to);
termDelete (rd->message);
roledefDelete (rd);
knowledgeDelete (tb->know[i + 1]);
i++;
}
memFree (tb->know, (i + 1) * sizeof (struct knowledge *));
memFree (tb->event, i * sizeof (struct roledef *));
memFree (tb->run, i * sizeof (int));
memFree (tb->status, i * sizeof (int));
memFree (tb->link, i * sizeof (int));
}
memFree (tb, sizeof (tracebuf));
}
struct tracebuf *
tracebufSet (const System sys, int length, int claimev)
{
struct tracebuf *tb;
int i;
Roledef rd;
/* TODO For the constraint logic approach, we would simply insert
* any constant from the constraint for a variable.
*/
tb = tracebufInit ();
if (length == 0)
{
return tb;
}
tb->length = length;
tb->reallength = length;
tb->variables = (Varbuf) varbufInit (sys);
tb->event = (Roledef *) memAlloc (length * sizeof (struct roledef *));
tb->status = (int *) memAlloc (length * sizeof (int));
tb->link = (int *) memAlloc (length * sizeof (int));
tb->run = (int *) memAlloc (length * sizeof (int));
tb->know =
(Knowledge *) memAlloc ((length + 1) * sizeof (struct knowledge *));
/* when duplicating the knowledge, we want to instantiate the variables as well
*/
tb->know[0] = knowledgeSubstDo (sys->traceKnow[0]);
i = 0;
while (i < length)
{
rd = roledefDuplicate1 (sys->traceEvent[i]);
if (rd == NULL)
{
printf ("Empty event in trace at %i of %i?\n", i, length);
exit (1);
}
/* make a copy without variables */
rd->to = termDuplicateUV (rd->to);
rd->from = termDuplicateUV (rd->from);
rd->message = termDuplicateUV (rd->message);
tb->event[i] = rd;
tb->link[i] = -1;
tb->status[i] = S_UNK;
tb->run[i] = sys->traceRun[i];
tb->know[i + 1] = NULL;
i++;
}
/* mark claim */
tb->violatedclaim = claimev;
tb->status[claimev] = S_OKE;
tracebufRebuildKnow (tb);
return tb;
}

29
src/tracebuf.h
View File

@ -1,29 +0,0 @@
#ifndef TRACEBUF
#define TRACEBUF
#include "term.h"
#include "termlist.h"
#include "knowledge.h"
#include "system.h"
/* STATUS symbols */
enum statussymbols
{
S_UNK, // UNKnown : unprocessed.
S_OKE, // OKE : done, but required for the attack.
S_RED, // REDundant : is not needed for attack, we're sure.
S_TOD // TODo : The previous suggestion REQ was too similar to RED. This is reserved for reads.
};
/*
* tracebuf struct is defined in system.h to avoid loops.
*/
int tracebufRebuildKnow (struct tracebuf *tb);
struct tracebuf *tracebufInit (void);
void tracebufDone (struct tracebuf *tb);
struct tracebuf *tracebufSet (const System sys, int length, int claimev);
#endif

92
src/varbuf.c
View File

@ -1,92 +0,0 @@
/*
* varbuf.c
*
* Operations on a variable substitutions buffer.
* The type is actually defined in system.h
*/
#include "memory.h"
#include "system.h"
/*
* create a new varbuffer from the current state of the system
*/
Varbuf
varbufInit (const System sys)
{
Varbuf vb;
Termlist tl;
Term termfrom, termto;
vb = (Varbuf) memAlloc (sizeof (struct varbuf));
vb->from = NULL;
vb->to = NULL;
vb->empty = NULL;
tl = sys->variables;
while (tl != NULL)
{
if (realTermVariable (tl->term))
{
/* this is actually a variable */
if (tl->term->subst == NULL)
{
/* non-instantiated */
vb->empty = termlistAdd (vb->empty, tl->term);
}
else
{
/* store instantiation */
termfrom = tl->term;
termto = termfrom->subst;
termfrom->subst = NULL; // temp disable
vb->from = termlistAdd (vb->from, termfrom);
vb->to = termlistAdd (vb->to, termto);
termfrom->subst = termto; // restore
}
}
tl = tl->next;
}
return vb;
}
/*
* copy the variable state back into the system
*/
void
varbufSet (const System sys, Varbuf vb)
{
Termlist tl1, tl2;
tl1 = vb->from;
tl2 = vb->to;
while (tl1 != NULL && tl2 != NULL)
{
tl1->term->subst = tl2->term;
tl1 = tl1->next;
tl2 = tl2->next;
}
tl1 = vb->empty;
while (tl1 != NULL)
{
tl1->term->subst = NULL;
tl1 = tl1->next;
}
}
/*
* cleanup
*/
void
varbufDone (Varbuf vb)
{
if (vb != NULL)
{
termlistDelete (vb->from);
termlistDelete (vb->to);
termlistDelete (vb->empty);
memFree (vb, sizeof (struct varbuf));
}
}

10
src/varbuf.h
View File

@ -1,10 +0,0 @@
#ifndef VARBUF
#define VARBUF
#include "system.h"
Varbuf varbufInit (const System sys);
void varbufSet (const System sys, Varbuf vb);
void varbufDone (Varbuf vb);
#endif