1124 lines
23 KiB
C
1124 lines
23 KiB
C
/*
|
|
* LaTeX output component
|
|
*/
|
|
|
|
#include <stdio.h>
|
|
#include <stdlib.h>
|
|
#include <time.h>
|
|
#include <limits.h>
|
|
#include "system.h"
|
|
#include "memory.h"
|
|
#include "modelchecker.h"
|
|
#include "tracebuf.h"
|
|
#include "varbuf.h"
|
|
#include "output.h"
|
|
#include "latex.h"
|
|
|
|
//! Multiplication factor for distance between events in an MSC diagram.
|
|
#define EVENTSPACE 1
|
|
//! Similarity factor required for connecting arrows. Ranges from 0 to 1.
|
|
#define LINKTHRESHOLD 0.95
|
|
|
|
extern const char *progname;
|
|
extern const char *releasetag;
|
|
extern int globalLatex;
|
|
extern Term TERM_Function;
|
|
|
|
/*! Additional information for an events. */
|
|
struct traceinfo
|
|
{
|
|
int match;
|
|
int position;
|
|
};
|
|
|
|
/* global variables for this module */
|
|
|
|
//! Additional information for each event in the trace.
|
|
struct traceinfo *tinfo;
|
|
//! The maximum run number involved, plus 1.
|
|
int width;
|
|
//! Landscape/portrait switch. Currently not used.
|
|
int landscape = 0;
|
|
|
|
//! Phase of MSC production.
|
|
/**
|
|
* In pass 1, the widths of the boxes are determined.
|
|
* In pass 2 the actual MSC is constructed.
|
|
*/
|
|
int pass;
|
|
|
|
/* code */
|
|
|
|
//! Start the latex output.
|
|
/** Prints some headers, and
|
|
* the command line that was used, as comments.
|
|
*@param sys The system buffer.
|
|
*@param argv The command line arguments as they were passed to the tool.
|
|
*@param argc The number of arguments.
|
|
*/
|
|
|
|
void
|
|
latexInit (const System sys, int argc, char **argv)
|
|
{
|
|
int i;
|
|
|
|
printf ("%%\n");
|
|
printf ("%% LaTeX output generated by %s\n", progname);
|
|
printf ("%% Input:\n");
|
|
|
|
/* print command line */
|
|
printf ("%% $");
|
|
for (i = 0; i < argc; i++)
|
|
printf (" %s", argv[i]);
|
|
printf ("\n");
|
|
|
|
printf ("%%\n");
|
|
|
|
/* comment macro (used for debugging) */
|
|
printf ("\\newcommand{\\comment}[1]{}\n");
|
|
}
|
|
|
|
//! Close up any LaTeX output.
|
|
/**
|
|
*@param sys The system state.
|
|
*/
|
|
|
|
void
|
|
latexDone (const System sys)
|
|
{
|
|
/* closing of the document */
|
|
}
|
|
|
|
//! Print a term using LaTeX and highlighting.
|
|
/**
|
|
* Basically a recode of termPrint, now specific using latex codes and with a
|
|
* highlighting feature. There is still some obsolete code to show variable mappings in a term.
|
|
*@param term a term to be printed.
|
|
*@param highlight a list of terms to be highlighted.
|
|
*/
|
|
|
|
void
|
|
latexTermPrint (Term term, Termlist highlight)
|
|
{
|
|
if (term == NULL)
|
|
{
|
|
printf ("Empty term");
|
|
return;
|
|
}
|
|
#ifdef DEBUG
|
|
if (!DEBUGL (1))
|
|
{
|
|
term = deVar (term);
|
|
}
|
|
#else
|
|
term = deVar (term);
|
|
#endif
|
|
if (realTermLeaf (term))
|
|
{
|
|
if (inTermlist (highlight, term))
|
|
printf ("\\mathbf{");
|
|
symbolPrint (TermSymb (term));
|
|
if (realTermVariable (term))
|
|
printf ("V");
|
|
if (TermRunid (term) >= 0)
|
|
{
|
|
printf ("\\sharp%i", TermRunid (term));
|
|
}
|
|
if (term->subst != NULL)
|
|
{
|
|
printf ("\\rightarrow");
|
|
latexTermPrint (term->subst, highlight);
|
|
}
|
|
if (inTermlist (highlight, term))
|
|
printf ("}");
|
|
}
|
|
if (realTermTuple (term))
|
|
{
|
|
printf ("(");
|
|
latexTermTuplePrint (term, highlight);
|
|
printf (")");
|
|
return;
|
|
}
|
|
if (realTermEncrypt (term))
|
|
{
|
|
if (isTermLeaf (TermKey (term))
|
|
&& inTermlist (TermKey (term)->stype, TERM_Function))
|
|
{
|
|
/* function application */
|
|
latexTermPrint (TermKey (term), highlight);
|
|
printf ("(");
|
|
latexTermTuplePrint (TermOp (term), highlight);
|
|
printf (")");
|
|
}
|
|
else
|
|
{
|
|
/* normal encryption */
|
|
printf ("\\{");
|
|
latexTermTuplePrint (TermOp (term), highlight);
|
|
printf ("\\}_{");
|
|
latexTermPrint (TermKey (term), highlight);
|
|
printf ("}");
|
|
}
|
|
}
|
|
}
|
|
|
|
//! Print an inner (tuple) term using LaTeX, without brackets.
|
|
/**
|
|
* The tuple printing only works correctly for normalized terms.
|
|
* If not, they might are displayed as "((x,y),z)". Maybe that is even
|
|
* desirable to distinguish them.
|
|
*/
|
|
void
|
|
latexTermTuplePrint (Term term, Termlist hl)
|
|
{
|
|
if (term == NULL)
|
|
{
|
|
printf ("Empty term");
|
|
return;
|
|
}
|
|
term = deVar (term);
|
|
while (realTermTuple (term))
|
|
{
|
|
// To remove any brackets, change this into latexTermTuplePrint.
|
|
latexTermPrint (TermOp1 (term), hl);
|
|
printf (",");
|
|
term = deVar (TermOp2 (term));
|
|
}
|
|
latexTermPrint (term, hl);
|
|
return;
|
|
}
|
|
|
|
//! Print a termlist in LaTeX using highlighting.
|
|
/**
|
|
* Extending LaTeX term printing to term list printing, again with highlight
|
|
* list parameter.
|
|
*@param tl A term list to print.
|
|
*@param highlight Any terms to be highlighted.
|
|
*/
|
|
|
|
void
|
|
latexTermlistPrint (Termlist tl, Termlist highlight)
|
|
{
|
|
if (tl == NULL)
|
|
{
|
|
printf ("\\emptyset");
|
|
return;
|
|
}
|
|
while (tl != NULL)
|
|
{
|
|
latexTermPrint (tl->term, highlight);
|
|
tl = tl->next;
|
|
if (tl != NULL)
|
|
printf (", ");
|
|
}
|
|
}
|
|
|
|
//! Display the timers and states traversed using LaTeX.
|
|
/**
|
|
* Obsolete: we will now only print timers on stderr.
|
|
*/
|
|
|
|
void
|
|
latexTimers (const System sys)
|
|
{
|
|
}
|
|
|
|
//! Start drawing MSC environment.
|
|
/**
|
|
* Includes printing title.
|
|
*@param protocolnames A termlist with protocol name terms.
|
|
*/
|
|
|
|
void
|
|
latexMSCStart (Termlist protocolnames)
|
|
{
|
|
if (landscape)
|
|
printf ("\\begin{landscape}\n");
|
|
|
|
printf ("\\begin{msc}{attack on $");
|
|
termlistPrint (protocolnames);
|
|
printf ("$}\n");
|
|
}
|
|
|
|
//! Close drawing MSC
|
|
|
|
void
|
|
latexMSCEnd ()
|
|
{
|
|
printf ("\\end{msc}\n");
|
|
|
|
if (landscape)
|
|
printf ("\\end{landscape}\n");
|
|
|
|
}
|
|
|
|
/**
|
|
* Declare the MSC stick for a single instance of a run participating in an
|
|
* attack.
|
|
* This involves layout of the partners roles, and the agent etc.
|
|
*@param sys System state.
|
|
*@param run The run to be declared.
|
|
*/
|
|
|
|
void
|
|
latexDeclInst (const System sys, int run)
|
|
{
|
|
Term myAgent;
|
|
Term myRole;
|
|
Termlist roles;
|
|
int first;
|
|
|
|
myAgent = agentOfRun (sys, run);
|
|
myRole = sys->runs[run].role->nameterm;
|
|
if (pass == 1)
|
|
{
|
|
printf ("\\maxlength{\\maxmscinst}{");
|
|
}
|
|
else
|
|
{
|
|
printf ("\\declinst{run%i}{", run);
|
|
}
|
|
|
|
/* display above assumptions */
|
|
roles = sys->runs[run].protocol->rolenames;
|
|
if (pass == 2)
|
|
{
|
|
printf ("assumes $");
|
|
first = 1;
|
|
while (roles != NULL)
|
|
{
|
|
if (!isTermEqual (myRole, roles->term))
|
|
{
|
|
if (!first)
|
|
printf (", ");
|
|
else
|
|
first = 0;
|
|
termPrint (agentOfRunRole (sys, run, roles->term));
|
|
printf (": ");
|
|
termPrint (roles->term);
|
|
}
|
|
roles = roles->next;
|
|
}
|
|
printf ("$}{");
|
|
}
|
|
|
|
/* display agent and role */
|
|
printf ("$\\mathbf{");
|
|
termPrint (myAgent);
|
|
printf ("}: ");
|
|
termPrint (myRole);
|
|
|
|
printf ("$}\n");
|
|
|
|
/* cleanup */
|
|
termDelete (myAgent);
|
|
}
|
|
|
|
//! Add vertical space in MSC diagrams.
|
|
/**
|
|
* Make some space in the diagram by nextlevels.
|
|
* TODO: can be incorporated in nextlevel[param] without loop.
|
|
*@param amount the line integer.
|
|
*/
|
|
|
|
void
|
|
latexEventSpace (int amount)
|
|
{
|
|
int i;
|
|
|
|
if (pass < 2)
|
|
{
|
|
/* not printing */
|
|
return;
|
|
}
|
|
|
|
//printf("%% number of newlines: %d\n",amount);
|
|
for (i = 0; i < EVENTSPACE * amount; i++)
|
|
printf ("\\nextlevel\n");
|
|
}
|
|
|
|
//! MSC message print.
|
|
/**
|
|
* Print an arrow with message from event i to event j, as defined in the
|
|
* tracebuffer. If either i or j are -1, the intruder is meant.
|
|
*/
|
|
|
|
void
|
|
latexMessagePrint (struct tracebuf *tb, int from, int to)
|
|
{
|
|
|
|
Term sendTerm = NULL;
|
|
Term readTerm = NULL;
|
|
|
|
if (pass < 2)
|
|
{
|
|
/* no measurement of messages yet */
|
|
return;
|
|
}
|
|
|
|
if (from == -1 && to == -1)
|
|
{
|
|
return;
|
|
}
|
|
if (from != -1)
|
|
{
|
|
sendTerm = tb->event[from]->message;
|
|
}
|
|
if (to != -1)
|
|
{
|
|
readTerm = tb->event[to]->message;
|
|
}
|
|
if (from == -1 && to != -1)
|
|
{
|
|
/* message from intruder into system */
|
|
printf ("\\mess{$");
|
|
termPrint (readTerm);
|
|
printf ("$}{eve}{run%d}\n", tb->run[to]);
|
|
}
|
|
else if (from != -1 && to == -1)
|
|
{
|
|
/* message from system to intruder */
|
|
printf ("\\mess{$");
|
|
termPrint (sendTerm);
|
|
printf ("$}{run%d}{eve}\n", tb->run[from]);
|
|
}
|
|
else if (from != -1 && to != -1)
|
|
{
|
|
/* message from one agent to another, possibly transformed */
|
|
|
|
printf ("\\mess{$");
|
|
|
|
termPrint (sendTerm);
|
|
|
|
if (!isTermEqual (sendTerm, readTerm))
|
|
{
|
|
printf ("\\rightarrow");
|
|
termPrint (readTerm);
|
|
}
|
|
|
|
printf ("$}{run%d", tb->run[from]);
|
|
printf ("}{run%d}[%d]", tb->run[to],
|
|
EVENTSPACE * (tinfo[to].position - tinfo[from].position));
|
|
|
|
printf ("\n");
|
|
}
|
|
}
|
|
|
|
/**
|
|
* hmm? TODO apparently, some other variant used, with duplicate handling of
|
|
* lost and found ??? But only using lost... weirdness.
|
|
*/
|
|
|
|
void
|
|
latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
|
|
Termlist highlight)
|
|
{
|
|
|
|
Term sendTerm = NULL;
|
|
Term readTerm = NULL;
|
|
|
|
if (pass < 2)
|
|
{
|
|
/* no measurements on message width yet */
|
|
return;
|
|
}
|
|
|
|
if (from == -1 && to == -1)
|
|
{
|
|
return;
|
|
}
|
|
if (from != -1)
|
|
{
|
|
sendTerm = tb->event[from]->message;
|
|
}
|
|
if (to != -1)
|
|
{
|
|
readTerm = tb->event[to]->message;
|
|
}
|
|
if (from == -1 && to != -1)
|
|
{
|
|
/* TODO redundant */
|
|
printf ("\\found{$");
|
|
latexTermPrint (readTerm, highlight);
|
|
printf ("$}{}{run%d}\n", tb->run[to]);
|
|
}
|
|
else if (from != -1 && to == -1)
|
|
{
|
|
printf ("\\mess{$");
|
|
latexTermPrint (sendTerm, highlight);
|
|
printf ("$}{run%d}{eve}\n", tb->run[from]);
|
|
}
|
|
else if (from != -1 && to != -1)
|
|
{
|
|
|
|
printf ("\\mess{$");
|
|
|
|
latexTermPrint (sendTerm, highlight);
|
|
|
|
if (!isTermEqual (sendTerm, readTerm))
|
|
{
|
|
printf ("\\rightarrow");
|
|
latexTermPrint (readTerm, highlight);
|
|
}
|
|
|
|
printf ("$}{run%d", tb->run[from]);
|
|
printf ("}{run%d}[%d]", tb->run[to],
|
|
EVENTSPACE * (tinfo[to].position - tinfo[from].position));
|
|
|
|
printf ("\n");
|
|
}
|
|
}
|
|
|
|
//! Display claim violation.
|
|
/**
|
|
* For now, only secrecy: TODO
|
|
*/
|
|
|
|
void
|
|
latexClaim (struct tracebuf *tb, int run, Termlist tl)
|
|
{
|
|
if (pass == 1)
|
|
{
|
|
printf ("\\maxlength{\\maxmsccondition}{");
|
|
}
|
|
else
|
|
{
|
|
printf ("\\condition{");
|
|
}
|
|
printf ("$\\neg secret ");
|
|
termlistPrint (tl);
|
|
printf ("$}");
|
|
if (pass == 1)
|
|
{
|
|
printf ("\n");
|
|
}
|
|
else
|
|
{
|
|
printf ("{run%d}\n", run);
|
|
}
|
|
}
|
|
|
|
//! Determine matching send event.
|
|
/**
|
|
* Given a read event, tries to find a corresponding send event in the trace
|
|
* buffer. Currently unused.
|
|
*/
|
|
|
|
int
|
|
latexCorrespondingSend (struct tracebuf *tb, 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 (tb->event[sendEvent]->type == SEND)
|
|
{
|
|
/* do all the different kind of matchings first */
|
|
|
|
labelMatch =
|
|
isTermEqual (tb->event[sendEvent]->label,
|
|
tb->event[readEvent]->label);
|
|
toMatch =
|
|
isTermEqual (tb->event[sendEvent]->to, tb->event[readEvent]->to);
|
|
fromMatch =
|
|
isTermEqual (tb->event[sendEvent]->from,
|
|
tb->event[readEvent]->from);
|
|
tofromMatch = toMatch || fromMatch;
|
|
messageMatch =
|
|
isTermEqual (tb->event[sendEvent]->message,
|
|
tb->event[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 (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;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
//bestSendEvent = NULL;
|
|
if (bestSendEvent == -1)
|
|
{
|
|
|
|
int u;
|
|
|
|
for (u = 0; u < rd; u++)
|
|
{
|
|
if (tb->event[u]->type == SEND)
|
|
{
|
|
//knowledgePrint(sys->traceKnow[u]);
|
|
if (inKnowledge
|
|
(tb->know[u + 1], tb->event[readEvent]->message))
|
|
{
|
|
bestSendEvent = u;
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (bestSendEvent == -1)
|
|
{
|
|
printf ("%% Could not find a matching SEND\n");
|
|
}
|
|
return bestSendEvent;
|
|
}
|
|
|
|
//! Determine matching send event.
|
|
/**
|
|
* Simplified variant of finding the matching send event.
|
|
* However, if it is introduced at a non-send event, things start to break
|
|
* done. REVIEW later.
|
|
*/
|
|
|
|
int
|
|
latexCorrespondingSend2 (struct tracebuf *tb, int readEvent)
|
|
{
|
|
int u;
|
|
|
|
for (u = tb->length - 1; u >= 0; u--)
|
|
{
|
|
if (tb->event[u]->type == SEND)
|
|
{
|
|
if (!inKnowledge (tb->know[u], tb->event[readEvent]->message))
|
|
{
|
|
/*
|
|
printf("%% term[");
|
|
printf("]#%d is introduced at traceEvent[%d] ",readEvent,u);
|
|
printf("\n");
|
|
*/
|
|
return u;
|
|
}
|
|
}
|
|
}
|
|
|
|
return -1;
|
|
|
|
}
|
|
|
|
//! Display knowledge in LaTeX.
|
|
|
|
void
|
|
knowledgePrintLatex (Knowledge know)
|
|
{
|
|
Termlist tl;
|
|
|
|
if (know == NULL)
|
|
{
|
|
printf ("\\emptyset");
|
|
}
|
|
else
|
|
{
|
|
tl = knowledgeSet (know);
|
|
latexTermlistPrint (tl, NULL);
|
|
termlistDelete (tl);
|
|
}
|
|
}
|
|
|
|
//! Display the attack in the systems attack buffer using LaTeX.
|
|
|
|
void
|
|
attackDisplayLatex (const System sys)
|
|
{
|
|
int i;
|
|
struct tracebuf *tb;
|
|
int *runPosition;
|
|
int currRun;
|
|
int position;
|
|
int eventSize;
|
|
Termlist tl;
|
|
Termlist newtl;
|
|
Termlist claimDetails;
|
|
Termlist highlights = NULL;
|
|
int cKnowledge;
|
|
int bestSend;
|
|
|
|
tb = sys->attack;
|
|
if (tb == NULL)
|
|
{
|
|
printf ("Attack pointer empty: nothing to display.\n");
|
|
exit (1);
|
|
}
|
|
/* set variables */
|
|
varbufSet (sys, tb->variables);
|
|
|
|
/* Rebuild knowledge. Strange, this ought to be good.
|
|
* Maybe reconstruct dependencies as well. */
|
|
tracebufRebuildKnow (tb);
|
|
|
|
/* Make a comment in which the trace is displayed, for debugging etc. */
|
|
printf ("\n\\comment{ TRACE\n\n");
|
|
printf ("Length: %i\n", tb->length);
|
|
printf ("Reallength: %i\n", tb->reallength);
|
|
printf ("\n");
|
|
i = 0;
|
|
while (i <= tb->length)
|
|
{
|
|
printf ("Knowledge %i:\n", i);
|
|
knowledgePrint (tb->know[i]);
|
|
printf (" [Inverses]: ");
|
|
knowledgeInversesPrint (tb->know[i]);
|
|
printf ("\n\n");
|
|
if (i < tb->length)
|
|
{
|
|
printf ("Event %i\t[", i);
|
|
switch (tb->status[i])
|
|
{
|
|
case S_UNK:
|
|
printf ("?");
|
|
break;
|
|
case S_RED:
|
|
printf ("redundant");
|
|
break;
|
|
case S_TOD:
|
|
printf ("to do");
|
|
break;
|
|
case S_OKE:
|
|
printf ("okay");
|
|
break;
|
|
default:
|
|
printf ("illegal status code");
|
|
break;
|
|
}
|
|
printf ("]\t");
|
|
termPrint (tb->event[i]->message);
|
|
printf ("\t#%i", tb->run[i]);
|
|
printf ("\n");
|
|
roledefPrint (tb->event[i]);
|
|
printf ("\n\n");
|
|
}
|
|
i++;
|
|
}
|
|
printf ("}\n\n");
|
|
|
|
tinfo =
|
|
(struct traceinfo *) memAlloc ((tb->length + 1) *
|
|
sizeof (struct traceinfo));
|
|
|
|
/*
|
|
* Determine width, which is the 1+max(runid involved in the attack)
|
|
*/
|
|
|
|
width = 1;
|
|
for (i = 0; i < tb->length; i++)
|
|
{
|
|
// TODO: I would expect here a redundancy test
|
|
if (tb->run[i] >= width)
|
|
width = tb->run[i] + 1;
|
|
}
|
|
|
|
/*
|
|
* Initialise tinfo arrays.
|
|
*/
|
|
|
|
for (i = 0; i < tb->length; i++)
|
|
{
|
|
tb->link[i] = -1;
|
|
tinfo[i].match = -1;
|
|
tinfo[i].position = i;
|
|
}
|
|
tinfo[i].match = -1;
|
|
tinfo[i].position = i;
|
|
|
|
/*
|
|
* Init array of positions (ordering) of the MSC lines.
|
|
*/
|
|
|
|
runPosition = (int *) memAlloc (width * sizeof (int));
|
|
for (i = 0; i < width; i++)
|
|
{
|
|
runPosition[i] = 0;
|
|
}
|
|
|
|
/*
|
|
* Determine corresponding sends and thus links
|
|
*/
|
|
|
|
for (i = tb->length - 1; i >= 0; i--)
|
|
{
|
|
if (tb->status[i] != S_RED)
|
|
{
|
|
if (tb->event[i]->type == READ && !tb->event[i]->internal)
|
|
{
|
|
bestSend = latexCorrespondingSend2 (tb, i);
|
|
printf ("%% match: %d <-> %d\n", i, bestSend);
|
|
if (bestSend == -1)
|
|
continue; // TODO major ugliness
|
|
|
|
tb->link[i] = bestSend;
|
|
tb->link[bestSend] = i;
|
|
}
|
|
if (tb->event[i]->type == CLAIM)
|
|
{
|
|
claimDetails =
|
|
claimViolationDetails (sys, tb->run[i], tb->event[i],
|
|
tb->know[i]);
|
|
}
|
|
}
|
|
}
|
|
printf ("\\comment{ claimDetails :\n");
|
|
termlistPrint (claimDetails);
|
|
printf ("\n}\n");
|
|
|
|
// landscape = (width > 4); // not for the time being
|
|
|
|
/*
|
|
* Apparently unlinks things that do not meet the threshold.
|
|
*/
|
|
|
|
position = 0;
|
|
currRun = 0;
|
|
eventSize = 0;
|
|
for (i = 0; i < tb->length; i++)
|
|
{
|
|
if (tb->status[i] != S_RED)
|
|
{
|
|
tinfo[i].position = position;
|
|
eventSize = 1;
|
|
currRun = tb->run[i];
|
|
|
|
switch (tb->event[i]->type)
|
|
{
|
|
case SEND:
|
|
position++;
|
|
tinfo[i].position++;
|
|
break;
|
|
case READ:
|
|
if (tb->link[i] != -1)
|
|
{
|
|
if (termDistance
|
|
(tb->event[i]->message,
|
|
tb->event[tb->link[i]]->message) < LINKTHRESHOLD)
|
|
{
|
|
/* disconnect read-send */
|
|
tb->link[tb->link[i]] = -1;
|
|
tb->link[i] = -1;
|
|
}
|
|
else
|
|
{
|
|
if (runPosition[currRun] <= tinfo[tb->link[i]].position
|
|
&& currRun != tb->run[tb->link[i]])
|
|
{
|
|
printf ("\\comment{\n");
|
|
termPrint (tb->event[i]->message);
|
|
printf ("\n");
|
|
termPrint (tb->event[tb->link[i]]->message);
|
|
printf ("\n");
|
|
printf ("%% termDistance: %f\n",
|
|
termDistance (tb->event[i]->message,
|
|
tb->event[tb->link[i]]->
|
|
message));
|
|
printf ("}\n");
|
|
tinfo[i].position = tinfo[tb->link[i]].position;
|
|
eventSize = 0;
|
|
}
|
|
}
|
|
}
|
|
if (tb->event[i]->internal)
|
|
{
|
|
eventSize = 0;
|
|
}
|
|
break;
|
|
case CLAIM:
|
|
if (claimDetails != NULL && claimDetails != (Termlist) - 1)
|
|
{
|
|
eventSize = 2;
|
|
}
|
|
else
|
|
{
|
|
eventSize = 0;
|
|
}
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
if (!(tb->event[i]->type == READ && tb->event[i]->internal))
|
|
runPosition[currRun] = tinfo[i].position + eventSize;
|
|
/* printf("%% Event %d at %d\n", i, position); */
|
|
position += eventSize;
|
|
}
|
|
}
|
|
|
|
/* ------------------------------------------------------
|
|
*
|
|
* Start of MSC creation (2-phase)
|
|
*
|
|
*
|
|
* ------------------------------------------------------
|
|
*/
|
|
|
|
/* 2 pass for widths */
|
|
|
|
for (pass = 1; pass <= 2; pass++)
|
|
{
|
|
printf ("%% Pass %i\n\n", pass);
|
|
|
|
if (pass == 1)
|
|
{
|
|
printf ("\\maxlength{\\maxmscaction}{knows}\n");
|
|
printf ("\\maxlength{\\maxmscaction}{creates}\n");
|
|
}
|
|
else
|
|
{
|
|
Termlist protocolnames;
|
|
Term pname;
|
|
|
|
/* slightly stretch measurements */
|
|
printf ("\\addtolength{\\maxmscall}{2\\mscspacer}\n");
|
|
printf ("\\addtolength{\\maxmscaction}{\\mscspacer}\n");
|
|
printf ("\\addtolength{\\maxmscinst}{\\mscspacer}\n");
|
|
printf ("\\addtolength{\\maxmsccondition}{\\mscspacer}\n");
|
|
|
|
/* put out computed widths */
|
|
|
|
printf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n");
|
|
printf ("\\setlength{\\instdist}{\\maxmscall}\n");
|
|
printf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
|
|
printf ("\\setlength{\\instwidth}{\\maxmscinst}\n");
|
|
printf ("\\setlength{\\conditionoverlap}{0.5\\maxmsccondition}\n");
|
|
|
|
/* create MSC title, involving protocol names and such. */
|
|
|
|
protocolnames = NULL;
|
|
for (i = 0; i < width; i++)
|
|
{
|
|
if (runPosition[i] > 0)
|
|
{
|
|
pname = sys->runs[i].protocol->nameterm;
|
|
if (!inTermlist (protocolnames, pname))
|
|
{
|
|
protocolnames = termlistAppend (protocolnames, pname);
|
|
}
|
|
}
|
|
}
|
|
latexMSCStart (protocolnames);
|
|
termlistDelete (protocolnames);
|
|
}
|
|
|
|
/* declare instances */
|
|
|
|
for (i = 0; i < width; i++)
|
|
{
|
|
if (runPosition[i] > 0)
|
|
latexDeclInst (sys, i);
|
|
}
|
|
/* Add the intruder instance */
|
|
if (pass == 2)
|
|
printf ("\\declinst{eve}{}{");
|
|
else
|
|
printf ("\\maxlength{\\maxmscinst}{");
|
|
printf ("{\\bf Eve}: Intruder}\n\n");
|
|
|
|
/* Print the local constants for each instance */
|
|
|
|
for (i = 0; i < width; i++)
|
|
{
|
|
if (runPosition[i] > 0)
|
|
{
|
|
Termlist tl = sys->runs[i].locals;
|
|
int first = 1;
|
|
while (tl != NULL)
|
|
{
|
|
/* detect whether it's really local to this run */
|
|
Term t = deVar (tl->term);
|
|
if (isTermLeaf (t) && TermRunid (t) == i)
|
|
{
|
|
if (first)
|
|
{
|
|
if (pass == 1)
|
|
printf ("\\maxlength{\\maxmscaction}{$");
|
|
else
|
|
printf ("\\ActionBox{creates \\\\\n$");
|
|
first = 0;
|
|
}
|
|
else
|
|
{
|
|
printf (", ");
|
|
}
|
|
termPrint (tl->term);
|
|
}
|
|
tl = tl->next;
|
|
}
|
|
if (!first)
|
|
{
|
|
if (pass == 1)
|
|
printf ("$}\n");
|
|
else
|
|
printf ("$}{run%i}\n", i);
|
|
}
|
|
}
|
|
}
|
|
|
|
/* Print the initial intruder knowledge */
|
|
|
|
if (pass == 2)
|
|
{
|
|
printf ("\\ActionBox{");
|
|
printf ("knows \\\\\n$");
|
|
knowledgePrintLatex (tb->know[0]);
|
|
printf ("$}");
|
|
printf ("{eve}\n");
|
|
printf ("\\nextlevel[3]\n");
|
|
printf ("\n");
|
|
}
|
|
|
|
/* print the events in the attack */
|
|
|
|
//for (j=-1; j<=sys->step; j++)
|
|
position = 0;
|
|
cKnowledge = 0;
|
|
for (i = 0; i < tb->length; i++)
|
|
{
|
|
if (tb->status[i] != S_RED)
|
|
{
|
|
latexEventSpace (tinfo[i].position - position);
|
|
if (tinfo[i].position >= position)
|
|
{
|
|
position = tinfo[i].position;
|
|
}
|
|
switch (tb->event[i]->type)
|
|
{
|
|
case SEND:
|
|
newtl = knowledgeNew (tb->know[i], tb->know[i + 1]);
|
|
highlights = NULL;
|
|
/* Build a Termlist of terms that from the claimViolationDetails,
|
|
that appear in the knowledge */
|
|
if (newtl != NULL)
|
|
{
|
|
tl = claimDetails;
|
|
while (tl != NULL)
|
|
{
|
|
if (inTermlist (newtl, tl->term))
|
|
{
|
|
highlights = termlistAdd (highlights, tl->term);
|
|
}
|
|
tl = tl->next;
|
|
}
|
|
|
|
}
|
|
|
|
if (tb->link[i] != -1 && i < tb->length)
|
|
{
|
|
latexMessagePrintHighlight (tb, i, tb->link[i],
|
|
highlights);
|
|
}
|
|
else
|
|
{
|
|
latexMessagePrintHighlight (tb, i, -1, highlights); //lost message
|
|
}
|
|
|
|
/* maybe extra knowledge? */
|
|
if (newtl != NULL)
|
|
{
|
|
/* print what was learned */
|
|
|
|
if (pass == 1)
|
|
{
|
|
printf ("\\maxlength{\\maxmscaction}{");
|
|
}
|
|
else
|
|
{
|
|
printf ("\\nextlevel[1]\n");
|
|
printf ("\\ActionBox{learns \\\\\n");
|
|
}
|
|
printf ("$");
|
|
cKnowledge++;
|
|
latexTermlistPrint (newtl, highlights);
|
|
printf ("$}");
|
|
if (pass == 1)
|
|
{
|
|
printf ("\n");
|
|
}
|
|
else
|
|
{
|
|
printf ("{eve}\n");
|
|
printf ("\\nextlevel[2]\n");
|
|
}
|
|
}
|
|
|
|
termlistDelete (highlights);
|
|
|
|
break;
|
|
case READ:
|
|
if (tb->event[i]->internal)
|
|
{
|
|
}
|
|
else if (tb->link[i] == -1)
|
|
{
|
|
latexMessagePrint (tb, -1, i); //found message
|
|
}
|
|
break;
|
|
case CLAIM:
|
|
if (claimDetails != NULL && claimDetails != (Termlist) - 1)
|
|
{
|
|
latexClaim (tb, tb->run[i], claimDetails);
|
|
}
|
|
break;
|
|
default:
|
|
break; //kannie!
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
* close up diagrams
|
|
*/
|
|
|
|
|
|
latexEventSpace (2);
|
|
latexMSCEnd ();
|
|
|
|
/*
|
|
* free used memory
|
|
*/
|
|
|
|
memFree (runPosition, width * sizeof (int));
|
|
memFree (tinfo, (tb->length + 1) * sizeof (struct traceinfo));
|
|
}
|