2004-04-23 11:58:43 +01:00
|
|
|
/*
|
|
|
|
* LaTeX output component
|
|
|
|
*/
|
|
|
|
|
|
|
|
#include <stdio.h>
|
|
|
|
#include <stdlib.h>
|
|
|
|
#include <time.h>
|
|
|
|
#include <limits.h>
|
|
|
|
#include "runs.h"
|
|
|
|
#include "memory.h"
|
|
|
|
#include "modelchecker.h"
|
|
|
|
#include "tracebuf.h"
|
|
|
|
#include "varbuf.h"
|
|
|
|
#include "output.h"
|
|
|
|
|
|
|
|
#define EVENTSPACE 1
|
|
|
|
#define LINKTHRESHOLD 0.95
|
|
|
|
|
|
|
|
extern const char *progname;
|
|
|
|
extern const char *releasetag;
|
|
|
|
extern int globalLatex;
|
|
|
|
extern Term TERM_Function;
|
|
|
|
|
|
|
|
/* struct for additional info */
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
struct traceinfo
|
|
|
|
{
|
|
|
|
int match;
|
|
|
|
int position;
|
2004-04-23 11:58:43 +01:00
|
|
|
};
|
|
|
|
|
|
|
|
/* global variables for this module */
|
|
|
|
|
|
|
|
struct traceinfo *tinfo;
|
|
|
|
int width;
|
|
|
|
int landscape = 0;
|
|
|
|
int *runPerm;
|
2004-05-13 15:49:04 +01:00
|
|
|
int pass;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
|
|
|
/* code */
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexInit (const System sys, int argc, char **argv)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
int i;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("%%\n");
|
|
|
|
printf ("%% LaTeX output generated by %s\n", progname);
|
|
|
|
printf ("%% Input:\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* print command line */
|
|
|
|
printf ("%% $");
|
|
|
|
for (i = 0; i < argc; i++)
|
|
|
|
printf (" %s", argv[i]);
|
|
|
|
printf ("\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("%%\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* comment macro (used for debugging) */
|
|
|
|
printf ("\\newcommand{\\comment}[1]{}\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexDone (const System sys)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 14:23:33 +01:00
|
|
|
/* closing of the document */
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* latexTermPrint
|
|
|
|
*
|
|
|
|
* basically a recode of termPrint, now specific using latex codes and with a
|
|
|
|
* highlighting feature.
|
|
|
|
*
|
|
|
|
* In:
|
|
|
|
* - a term to be printed.
|
|
|
|
* - a list of terms to be highlighted.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 11:58:43 +01:00
|
|
|
void
|
|
|
|
latexTermPrint (Term term, Termlist highlight)
|
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
if (term == NULL)
|
|
|
|
{
|
|
|
|
printf ("Empty term");
|
|
|
|
return;
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
#ifdef DEBUG
|
2004-04-23 12:03:07 +01:00
|
|
|
if (!DEBUGL (1))
|
|
|
|
{
|
|
|
|
term = deVar (term);
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
#else
|
2004-04-23 12:03:07 +01:00
|
|
|
term = deVar (term);
|
2004-04-23 11:58:43 +01:00
|
|
|
#endif
|
2004-04-23 12:03:07 +01:00
|
|
|
if (realTermLeaf (term))
|
|
|
|
{
|
|
|
|
if (inTermlist (highlight, term))
|
|
|
|
printf ("\\mathbf{");
|
|
|
|
symbolPrint (term->symb);
|
|
|
|
if (realTermVariable (term))
|
|
|
|
printf ("V");
|
|
|
|
if (term->runid >= 0)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\sharp%i", term->runid);
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
if (term->subst != NULL)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\rightarrow");
|
|
|
|
latexTermPrint (term->subst, highlight);
|
|
|
|
}
|
|
|
|
if (inTermlist (highlight, term))
|
|
|
|
printf ("}");
|
|
|
|
}
|
|
|
|
if (realTermTuple (term))
|
|
|
|
{
|
|
|
|
printf ("(");
|
|
|
|
while (realTermTuple (term))
|
|
|
|
{
|
|
|
|
latexTermPrint (term->op1, highlight);
|
|
|
|
printf (",");
|
|
|
|
term = term->op2;
|
|
|
|
if (!realTermTuple (term))
|
|
|
|
latexTermPrint (term, highlight);
|
2004-04-23 11:58:43 +01:00
|
|
|
|
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
printf (")");
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
if (realTermEncrypt (term))
|
|
|
|
{
|
|
|
|
if (isTermLeaf (term->key)
|
|
|
|
&& inTermlist (term->key->stype, TERM_Function))
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
/* function application */
|
|
|
|
latexTermPrint (term->key, highlight);
|
|
|
|
printf ("(");
|
|
|
|
latexTermPrint (term->op, highlight);
|
|
|
|
printf (")");
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
/* normal encryption */
|
|
|
|
printf ("\\{");
|
|
|
|
latexTermPrint (term->op, highlight);
|
|
|
|
printf ("\\}_{");
|
|
|
|
latexTermPrint (term->key, highlight);
|
|
|
|
printf ("}");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* extending LaTeX term printing to term list printing, again with highlight
|
|
|
|
* list parameter.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 11:58:43 +01:00
|
|
|
void
|
|
|
|
latexTermlistPrint (Termlist tl, Termlist highlight)
|
|
|
|
{
|
|
|
|
if (tl == NULL)
|
|
|
|
{
|
2004-05-12 16:16:11 +01:00
|
|
|
printf ("\\emptyset");
|
2004-04-23 11:58:43 +01:00
|
|
|
return;
|
|
|
|
}
|
|
|
|
while (tl != NULL)
|
|
|
|
{
|
|
|
|
latexTermPrint (tl->term, highlight);
|
|
|
|
tl = tl->next;
|
|
|
|
if (tl != NULL)
|
2004-04-23 12:03:07 +01:00
|
|
|
printf (", ");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Display the timers and states traversed, LaTeX version.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexTimers (const System sys)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
void endline (void)
|
|
|
|
{
|
|
|
|
printf ("\\\\ \\hline\n");
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\begin{tabular}{|r|r|c|r|} \\hline\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* display stats, header first */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("Time & States & Attack & st/sec");
|
|
|
|
endline ();
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* print time */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
double seconds;
|
|
|
|
seconds = (double) clock () / CLOCKS_PER_SEC;
|
|
|
|
printf ("$%.3e$ &", seconds);
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* states traversed */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("$");
|
|
|
|
statesPrintShort (sys);
|
|
|
|
printf ("$ &");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* flag
|
|
|
|
*
|
|
|
|
* L n Attack of length <n>
|
|
|
|
* None failed claim
|
|
|
|
* NoClaim no claims
|
|
|
|
*/
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (sys->claims == 0)
|
|
|
|
{
|
|
|
|
printf ("NoClaim & ");
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
if (sys->failed > 0)
|
|
|
|
printf ("L:%i & ", attackLength (sys->attack));
|
|
|
|
else
|
|
|
|
printf ("None & ");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/*
|
|
|
|
printf("%.3e (%li) claims encountered.\n",(double)
|
|
|
|
sys->claims, sys->claims);
|
|
|
|
printf("%.3e (%li) claims failed.\n",(double)
|
|
|
|
sys->failed, sys->failed);
|
|
|
|
*/
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
/* states per second */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (seconds > 0)
|
|
|
|
{
|
|
|
|
printf ("$%.3e$ ",
|
|
|
|
(double) (sys->statesLow +
|
|
|
|
(sys->statesHigh * ULONG_MAX)) / seconds);
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
printf ("$\\infty$ ");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
endline ();
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\end{tabular}\n\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Start drawing MSC environment.
|
|
|
|
*
|
|
|
|
* Includes printing title
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
2004-04-23 15:11:51 +01:00
|
|
|
latexMSCStart (Termlist protocolnames)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
if (landscape)
|
|
|
|
printf ("\\begin{landscape}\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 15:11:51 +01:00
|
|
|
printf ("\\begin{msc}{attack on $");
|
2004-05-12 16:19:40 +01:00
|
|
|
termlistPrint (protocolnames);
|
2004-04-23 15:11:51 +01:00
|
|
|
printf ("$}\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Close drawing MSC
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexMSCEnd ()
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\end{msc}\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (landscape)
|
|
|
|
printf ("\\end{landscape}\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Declare the MSC stick for a single instance of a run participating in an
|
|
|
|
* attack.
|
2004-05-13 11:06:21 +01:00
|
|
|
*
|
|
|
|
* This involves layout of the partners roles, and the agent etc.
|
2004-05-12 15:45:50 +01:00
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexDeclInst (const System sys, int run)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-05-13 11:06:21 +01:00
|
|
|
Term myAgent;
|
|
|
|
Term myRole;
|
|
|
|
Termlist roles;
|
|
|
|
int first;
|
|
|
|
|
|
|
|
myAgent = agentOfRun (sys, run);
|
|
|
|
myRole = sys->runs[run].role->nameterm;
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass == 1)
|
|
|
|
{
|
|
|
|
printf ("\\maxlength{\\maxmscinst}{");
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
printf ("\\declinst{run%i}{", run);
|
|
|
|
}
|
2004-05-13 11:06:21 +01:00
|
|
|
|
|
|
|
/* display above assumptions */
|
|
|
|
roles = sys->runs[run].protocol->rolenames;
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass == 2)
|
2004-05-13 11:06:21 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("assumes $");
|
|
|
|
first = 1;
|
|
|
|
while (roles != NULL)
|
2004-05-13 11:06:21 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (!isTermEqual (myRole, roles->term))
|
|
|
|
{
|
|
|
|
if (!first)
|
|
|
|
printf (", ");
|
|
|
|
else
|
|
|
|
first = 0;
|
|
|
|
termPrint (agentOfRunRole(sys,run,roles->term));
|
|
|
|
printf(": ");
|
|
|
|
termPrint (roles->term);
|
|
|
|
}
|
|
|
|
roles = roles->next;
|
2004-05-13 11:06:21 +01:00
|
|
|
}
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("$}{");
|
2004-05-13 11:06:21 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
|
2004-05-13 11:06:21 +01:00
|
|
|
/* display agent and role */
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("$\\mathbf{");
|
2004-05-13 11:06:21 +01:00
|
|
|
termPrint (myAgent);
|
|
|
|
printf("}: ");
|
|
|
|
termPrint (myRole);
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("$}\n");
|
2004-05-13 11:06:21 +01:00
|
|
|
|
|
|
|
/* cleanup */
|
|
|
|
termDelete (myAgent);
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Make some space in the diagram by nextlevels.
|
|
|
|
*
|
|
|
|
* TODO: can be incorporated in nextlevel[param] without loop.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexEventSpace (int amount)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass < 2)
|
|
|
|
{
|
|
|
|
/* not printing */
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
int i;
|
|
|
|
//printf("%% number of newlines: %d\n",amount);
|
|
|
|
for (i = 0; i < EVENTSPACE * amount; i++)
|
|
|
|
printf ("\\nextlevel\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* 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.
|
|
|
|
*/
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexMessagePrint (struct tracebuf *tb, int from, int to)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
Term sendTerm = NULL;
|
|
|
|
Term readTerm = NULL;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass < 2)
|
|
|
|
{
|
|
|
|
/* no measurement of messages yet */
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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)
|
|
|
|
{
|
2004-05-12 15:45:50 +01:00
|
|
|
/* message from intruder into system */
|
2004-05-12 15:56:45 +01:00
|
|
|
printf ("\\mess{$");
|
2004-04-23 12:03:07 +01:00
|
|
|
termPrint (readTerm);
|
2004-05-12 15:56:45 +01:00
|
|
|
printf ("$}{eve}{run%d}\n", tb->run[to]);
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
|
|
|
else if (from != -1 && to == -1)
|
|
|
|
{
|
2004-05-12 15:45:50 +01:00
|
|
|
/* message from system to intruder */
|
2004-05-12 15:56:45 +01:00
|
|
|
printf ("\\mess{$");
|
2004-04-23 12:03:07 +01:00
|
|
|
termPrint (sendTerm);
|
2004-05-12 15:56:45 +01:00
|
|
|
printf ("$}{run%d}{eve}\n", tb->run[from]);
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
|
|
|
else if (from != -1 && to != -1)
|
|
|
|
{
|
2004-05-12 15:45:50 +01:00
|
|
|
/* message from one agent to another, possibly transformed */
|
2004-04-23 12:03:07 +01:00
|
|
|
|
|
|
|
printf ("\\mess{$");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
termPrint (sendTerm);
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (!isTermEqual (sendTerm, readTerm))
|
|
|
|
{
|
|
|
|
printf ("\\rightarrow");
|
|
|
|
termPrint (readTerm);
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
|
|
|
|
printf ("$}{run%d", tb->run[from]);
|
|
|
|
printf ("}{run%d}[%d]", tb->run[to],
|
|
|
|
EVENTSPACE * (tinfo[to].position - tinfo[from].position));
|
|
|
|
|
|
|
|
printf ("\n");
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-05-12 15:45:50 +01:00
|
|
|
|
|
|
|
/*
|
2004-05-12 15:56:45 +01:00
|
|
|
* hmm? TODO apparently, some other variant used, with duplicate handling of
|
|
|
|
* lost and found ??? But only using lost... weirdness.
|
2004-05-12 15:45:50 +01:00
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
|
|
|
|
Termlist highlight)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
Term sendTerm = NULL;
|
|
|
|
Term readTerm = NULL;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass < 2)
|
|
|
|
{
|
|
|
|
/* no measurements on message width yet */
|
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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)
|
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
/* TODO redundant */
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\found{$");
|
|
|
|
latexTermPrint (readTerm, highlight);
|
|
|
|
printf ("$}{}{run%d}\n", tb->run[to]);
|
|
|
|
}
|
|
|
|
else if (from != -1 && to == -1)
|
|
|
|
{
|
2004-05-12 15:56:45 +01:00
|
|
|
printf ("\\mess{$");
|
2004-04-23 12:03:07 +01:00
|
|
|
latexTermPrint (sendTerm, highlight);
|
2004-05-12 15:56:45 +01:00
|
|
|
printf ("$}{run%d}{eve}\n", tb->run[from]);
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
|
|
|
else if (from != -1 && to != -1)
|
|
|
|
{
|
|
|
|
|
|
|
|
printf ("\\mess{$");
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
latexTermPrint (sendTerm, highlight);
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (!isTermEqual (sendTerm, readTerm))
|
|
|
|
{
|
|
|
|
printf ("\\rightarrow");
|
|
|
|
latexTermPrint (readTerm, highlight);
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
|
|
|
|
printf ("$}{run%d", tb->run[from]);
|
|
|
|
printf ("}{run%d}[%d]", tb->run[to],
|
|
|
|
EVENTSPACE * (tinfo[to].position - tinfo[from].position));
|
|
|
|
|
|
|
|
printf ("\n");
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-05-12 15:45:50 +01:00
|
|
|
|
|
|
|
/*
|
|
|
|
* ?? TODO
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexAction (struct tracebuf *tb, int te)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\action{$");
|
|
|
|
termPrint (tb->event[te]->message);
|
|
|
|
printf ("$}{run%d}\n", tb->run[te]);
|
|
|
|
//printf("\\nextlevel\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* display claim violation.
|
|
|
|
*
|
|
|
|
* for now, only secrecy: TODO
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
latexClaim (struct tracebuf *tb, int run, Termlist tl)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass == 1)
|
|
|
|
{
|
|
|
|
printf ("\\maxlength{\\maxmsccondition}{");
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
printf ("\\condition{");
|
|
|
|
}
|
|
|
|
printf ("$\\neg secret ");
|
2004-04-23 12:03:07 +01:00
|
|
|
termlistPrint (tl);
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("$}");
|
|
|
|
if (pass == 1)
|
|
|
|
{
|
|
|
|
printf ("\n");
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
printf ("{run%d}\n", run);
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Given a read event, tries to find a corresponding send event in the trace
|
|
|
|
* buffer.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
int
|
|
|
|
latexCorrespondingSend (struct tracebuf *tb, int rd)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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;
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
if (nMatches > maxNMatches)
|
|
|
|
{
|
|
|
|
if (labelMatch && messageMatch)
|
|
|
|
{
|
|
|
|
/* strongest restriction: message and label should match */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
maxNMatches = nMatches;
|
|
|
|
bestSendEvent = sendEvent;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
|
|
|
else if (messageMatch)
|
|
|
|
{
|
|
|
|
/* if label AND message don't match: */
|
|
|
|
/* at least message should match */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
maxNMatches = nMatches;
|
|
|
|
bestSendEvent = sendEvent;
|
|
|
|
}
|
|
|
|
else if (labelMatch)
|
|
|
|
{
|
|
|
|
/* if message doesn't match */
|
|
|
|
/* the label should matches */
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
maxNMatches = nMatches;
|
|
|
|
bestSendEvent = sendEvent;
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
//bestSendEvent = NULL;
|
|
|
|
if (bestSendEvent == -1)
|
|
|
|
{
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
int u;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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;
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (bestSendEvent == -1)
|
|
|
|
{
|
|
|
|
printf ("%% Could not find a matching SEND\n");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
return bestSendEvent;
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* VERY broken. Mindwipe and recursion using inKnowledge, so this can't work.
|
|
|
|
*
|
|
|
|
* Apparently, it's supposed to find any subterm and was added in revision 526
|
|
|
|
* by Lutger.
|
|
|
|
*/
|
2004-04-23 11:58:43 +01:00
|
|
|
|
|
|
|
int
|
|
|
|
newInKnowledge (const Knowledge know, Term term)
|
|
|
|
{
|
|
|
|
/* if there is no term, then it's okay 'fur sure' */
|
|
|
|
if (term == NULL)
|
|
|
|
return 1;
|
|
|
|
/* if there is a term, but no knowledge, we're in trouble */
|
|
|
|
if (know == NULL)
|
|
|
|
return 0;
|
|
|
|
|
|
|
|
mindwipe (know, inKnowledge (know, term));
|
|
|
|
|
|
|
|
term = deVar (term);
|
|
|
|
if (isTermLeaf (term))
|
|
|
|
{
|
|
|
|
return inTermlist (know->basic, term);
|
|
|
|
}
|
|
|
|
if (term->type == ENCRYPT)
|
|
|
|
{
|
|
|
|
return inTermlist (know->encrypt, term) ||
|
|
|
|
(inKnowledge (know, term->key) || inKnowledge (know, term->op));
|
|
|
|
}
|
|
|
|
if (term->type == TUPLE)
|
|
|
|
{
|
|
|
|
return (inTermlist (know->encrypt, term) ||
|
2004-04-23 12:03:07 +01:00
|
|
|
(inKnowledge (know, term->op1) ||
|
2004-04-23 11:58:43 +01:00
|
|
|
inKnowledge (know, term->op2)));
|
|
|
|
}
|
|
|
|
return 0; /* unrecognized term type, weird */
|
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* 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.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
int
|
|
|
|
latexCorrespondingSend2 (struct tracebuf *tb, int readEvent)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
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;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
/*
|
|
|
|
* Display knowledge in LaTeX format.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
knowledgePrintLatex (Knowledge know)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
Termlist tl;
|
2004-04-23 11:58:43 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
if (know == NULL)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
printf ("\\emptyset");
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
else
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
tl = knowledgeSet (know);
|
2004-05-12 16:19:40 +01:00
|
|
|
latexTermlistPrint (tl, NULL);
|
2004-04-23 12:03:07 +01:00
|
|
|
termlistDelete (tl);
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Display an attack
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
void
|
|
|
|
attackDisplayLatex (System sys)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
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));
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Determine width, which is the 1+max(runid involved in the attack)
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
width = 1;
|
|
|
|
for (i = 0; i < tb->length; i++)
|
|
|
|
{
|
2004-05-12 15:45:50 +01:00
|
|
|
// TODO: I would expect here a redundancy test
|
2004-04-23 12:03:07 +01:00
|
|
|
if (tb->run[i] >= width)
|
|
|
|
width = tb->run[i] + 1;
|
|
|
|
}
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Initialise tinfo arrays.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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;
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Init array of positions (ordering) of the MSC lines.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
runPosition = (int *) memAlloc (width * sizeof (int));
|
|
|
|
for (i = 0; i < width; i++)
|
|
|
|
{
|
|
|
|
runPosition[i] = 0;
|
|
|
|
}
|
2004-05-12 15:45:50 +01:00
|
|
|
|
|
|
|
/*
|
|
|
|
* Determine corresponding sends and thus links
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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)
|
2004-05-12 15:45:50 +01:00
|
|
|
continue; // TODO major ugliness
|
2004-04-23 12:03:07 +01:00
|
|
|
|
|
|
|
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
|
|
|
|
|
2004-05-12 15:45:50 +01:00
|
|
|
/*
|
|
|
|
* Apparently unlinks things that do not meet the threshold.
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
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)
|
2004-04-23 11:58:43 +01:00
|
|
|
{
|
2004-04-23 12:03:07 +01:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
}
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* ------------------------------------------------------
|
|
|
|
*
|
|
|
|
* Start of MSC creation (2-phase)
|
|
|
|
*
|
|
|
|
*
|
|
|
|
* ------------------------------------------------------
|
|
|
|
*/
|
2004-04-23 15:11:51 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* 2 pass for widths */
|
|
|
|
|
|
|
|
for (pass = 1; pass <= 2; pass++)
|
2004-04-23 15:11:51 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("%% Pass %i\n\n",pass);
|
|
|
|
|
|
|
|
if (pass == 1)
|
2004-04-23 15:11:51 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("\\maxlength{\\maxmscaction}{knows}\n");
|
|
|
|
printf ("\\maxlength{\\maxmscaction}{creates}\n");
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
/* 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.5\\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. */
|
|
|
|
|
|
|
|
Termlist protocolnames = NULL;
|
|
|
|
Term pname;
|
|
|
|
for (i = 0; i < width; i++)
|
2004-04-23 15:11:51 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (runPosition[i] > 0)
|
|
|
|
{
|
|
|
|
pname = sys->runs[i].protocol->nameterm;
|
|
|
|
if (!inTermlist (protocolnames, pname))
|
|
|
|
{
|
|
|
|
protocolnames = termlistAppend (protocolnames, pname);
|
|
|
|
}
|
|
|
|
}
|
2004-04-23 15:11:51 +01:00
|
|
|
}
|
2004-05-13 15:49:04 +01:00
|
|
|
latexMSCStart (protocolnames);
|
|
|
|
termlistDelete (protocolnames);
|
2004-04-23 15:11:51 +01:00
|
|
|
}
|
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* declare instances */
|
2004-04-23 15:11:51 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
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");
|
2004-04-23 12:03:07 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* Print the local constants for each instance */
|
2004-05-13 11:06:21 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
for (i = 0; i < width; i++)
|
2004-05-13 11:06:21 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (runPosition[i] > 0)
|
2004-05-13 11:06:21 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
Termlist tl = sys->runs[i].locals;
|
|
|
|
int first = 1;
|
|
|
|
while (tl != NULL)
|
2004-05-13 11:06:21 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
/* detect whether it's really local to this run */
|
|
|
|
Term t = deVar (tl->term);
|
|
|
|
if (isTermLeaf (t) && t->runid == i)
|
2004-05-13 11:06:21 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (first)
|
|
|
|
{
|
|
|
|
if (pass == 1)
|
|
|
|
printf ("\\maxlength{\\maxmscaction}{$");
|
|
|
|
else
|
|
|
|
printf ("\\ActionBox{creates \\\\\n$");
|
|
|
|
first = 0;
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
printf (", ");
|
|
|
|
}
|
|
|
|
termPrint (tl->term);
|
2004-05-13 11:06:21 +01:00
|
|
|
}
|
2004-05-13 15:49:04 +01:00
|
|
|
tl = tl->next;
|
|
|
|
}
|
|
|
|
if (!first)
|
|
|
|
{
|
|
|
|
if (pass == 1)
|
|
|
|
printf ("$}\n");
|
2004-05-13 11:06:21 +01:00
|
|
|
else
|
2004-05-13 15:49:04 +01:00
|
|
|
printf ("$}{run%i}\n", i);
|
2004-05-13 11:06:21 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* Print the initial intruder knowledge */
|
2004-05-12 16:07:33 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
if (pass == 2)
|
|
|
|
{
|
|
|
|
printf ("\\ActionBox{");
|
|
|
|
printf ("knows \\\\\n$");
|
|
|
|
knowledgePrintLatex (tb->know[0]);
|
|
|
|
printf ("$}");
|
|
|
|
printf ("{eve}\n");
|
|
|
|
printf ("\\nextlevel[3]\n");
|
|
|
|
printf ("\n");
|
|
|
|
}
|
2004-05-12 16:07:33 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* print the events in the attack */
|
2004-04-23 15:11:51 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
//for (j=-1; j<=sys->step; j++)
|
|
|
|
position = 0;
|
|
|
|
cKnowledge = 0;
|
|
|
|
for (i = 0; i < tb->length; i++)
|
2004-04-23 12:03:07 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (tb->status[i] != S_RED)
|
2004-04-23 12:03:07 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
latexEventSpace (tinfo[i].position - position);
|
|
|
|
if (tinfo[i].position >= position)
|
2004-04-23 12:03:07 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
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)
|
2004-04-23 12:03:07 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
tl = claimDetails;
|
|
|
|
while (tl != NULL)
|
2004-04-23 12:03:07 +01:00
|
|
|
{
|
2004-05-13 15:49:04 +01:00
|
|
|
if (inTermlist (newtl, tl->term))
|
|
|
|
{
|
|
|
|
highlights = termlistAdd (highlights, tl->term);
|
|
|
|
}
|
|
|
|
tl = tl->next;
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
2004-05-13 15:49:04 +01:00
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
2004-05-12 15:56:45 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
if (tb->link[i] != -1 && i < tb->length)
|
|
|
|
{
|
|
|
|
latexMessagePrintHighlight (tb, i, tb->link[i], highlights);
|
|
|
|
}
|
|
|
|
else
|
|
|
|
{
|
|
|
|
latexMessagePrintHighlight (tb, i, -1, highlights); //lost message
|
|
|
|
}
|
2004-04-23 12:03:07 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
/* maybe extra knowledge? */
|
|
|
|
if (newtl != NULL)
|
|
|
|
{
|
|
|
|
/* print what was learned */
|
2004-05-12 16:13:21 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
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");
|
|
|
|
}
|
|
|
|
}
|
2004-05-12 16:19:40 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
termlistDelete (highlights);
|
2004-04-23 12:03:07 +01:00
|
|
|
|
2004-05-13 15:49:04 +01:00
|
|
|
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!
|
2004-04-23 12:03:07 +01:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2004-05-13 15:49:04 +01:00
|
|
|
|
|
|
|
/*
|
|
|
|
* close up diagrams
|
|
|
|
*/
|
|
|
|
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
latexEventSpace (2);
|
|
|
|
latexMSCEnd ();
|
2004-05-13 15:49:04 +01:00
|
|
|
|
|
|
|
/*
|
|
|
|
* free used memory
|
|
|
|
*/
|
|
|
|
|
2004-04-23 12:03:07 +01:00
|
|
|
memFree (runPosition, width * sizeof (int));
|
|
|
|
memFree (tinfo, (tb->length + 1) * sizeof (struct traceinfo));
|
2004-04-23 11:58:43 +01:00
|
|
|
}
|