diff --git a/src/attacktemplate.tex b/src/attacktemplate.tex index 1390fc0..d2847d7 100644 --- a/src/attacktemplate.tex +++ b/src/attacktemplate.tex @@ -2,6 +2,11 @@ \usepackage{a4wide} \usepackage{msc} +\setlength{\instwidth}{3.0cm} +\setlength{\instdist}{4cm} +\setlength{\actionwidth}{3.6cm} +\setlength{\conditionoverlap}{1.9cm} + \begin{document} \input{attack} diff --git a/src/latex.c b/src/latex.c index ffaccfa..c5b90e4 100644 --- a/src/latex.c +++ b/src/latex.c @@ -279,19 +279,52 @@ latexMSCEnd () /* * 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. */ void latexDeclInst (const System sys, int run) { - Term bar = NULL; + Term myAgent; + Term myRole; + Termlist roles; + int first; - bar = agentOfRun (sys, run); - printf ("\\declinst{run%d}{$", run); - termPrint (bar); - printf ("\\sharp%i$}{$", run); - agentsOfRunPrint (sys, run); + myAgent = agentOfRun (sys, run); + myRole = sys->runs[run].role->nameterm; + printf ("\\declinst{run%i}{", run); + + /* display above assumptions */ + roles = sys->runs[run].protocol->rolenames; + 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); } /* @@ -908,9 +941,43 @@ attackDisplayLatex (System sys) latexDeclInst (sys, i); } /* Add the intruder instance */ - printf ("\\declinst{eve}{Eve}{Intruder}\n"); + printf ("\\declinst{eve}{}{{\\bf Eve}: Intruder}\n"); printf ("\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) && t->runid == i) + { + if (first) + { + printf ("\\action{creates $"); + first = 0; + } + else + { + printf (", "); + } + termPrint (tl->term); + } + tl = tl->next; + } + if (!first) + { + printf ("$}{run%i}\n", i); + } + } + } + /* Print the initial intruder knowledge */ printf ("\\action{knows $"); diff --git a/src/runs.c b/src/runs.c index b042ca8..b3b06b6 100644 --- a/src/runs.c +++ b/src/runs.c @@ -511,7 +511,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role, rd = rd->next; } termlistDelete (fromlist); - termlistDelete (tolist); + runs[rid].locals = tolist; } Roledef diff --git a/src/runs.h b/src/runs.h index fc41d04..6f8bd14 100644 --- a/src/runs.h +++ b/src/runs.h @@ -65,6 +65,7 @@ struct run Roledef index; Roledef start; Knowledge know; + Termlist locals; }; typedef struct run *Run; diff --git a/src/testl b/src/testl index 6b67fb6..03cc56e 100755 --- a/src/testl +++ b/src/testl @@ -20,9 +20,9 @@ then mv $template.dvi attack.dvi dvips attack.dvi -o attack.ps -# xdvi attack.dvi # for Xdvi + xdvi attack.dvi # for Xdvi # kdvi attack.dvi # for KDE environment - kghostview attack.ps # postscript in KDE +# kghostview attack.ps # postscript in KDE else