- Added 'singular' directive for roles. Syntax:

protocol ns3 (I,R)
  {
    singular role I:
    {
    }
  }
This commit is contained in:
ccremers 2006-01-02 16:05:53 +00:00
parent 724faa8949
commit e21627442a
8 changed files with 75 additions and 5 deletions

View File

@ -2483,6 +2483,9 @@ bind_goal (const Binding b)
//! Prune determination because of theorems //! Prune determination because of theorems
/** /**
* When something is pruned because of this function, the state space is still
* considered to be complete.
*
*@returns true iff this state is invalid because of a theorem *@returns true iff this state is invalid because of a theorem
*/ */
int int
@ -2724,11 +2727,49 @@ prune_theorems ()
bl = bl->next; bl = bl->next;
} }
/* check for singular roles */
run = 0;
while (run < sys->maxruns)
{
if (sys->runs[run].role->singular)
{
// This is a singular role: it therefore should not occur later on again.
int run2;
Term rolename;
rolename = sys->runs[run].role->nameterm;
run2 = run + 1;
while (run2 < sys->maxruns)
{
Term rolename2;
rolename2 = sys->runs[run2].role->nameterm;
if (isTermEqual (rolename, rolename2))
{
// This is not allowed: the singular role occurs twice in the semitrace.
// Thus we prune.
if (switches.output == PROOF)
{
indentPrint ();
eprintf ("Pruned because the singular role ");
termPrint (rolename);
eprintf (" occurs more than once in the semitrace.\n");
}
return 1;
}
run2++;
}
}
run++;
}
return 0; return 0;
} }
//! Prune determination for bounds //! Prune determination for bounds
/** /**
* When something is pruned here, the state space is not complete anymore.
*
*@returns true iff this state is invalid for some reason *@returns true iff this state is invalid for some reason
*/ */
int int

View File

@ -762,6 +762,12 @@ claimAddAll (const System sys, const Protocol protocol, const Role role)
claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL); claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL);
} }
//! Compile a role
/**
* Input: a name and a roledef tac
*
* Upon return, thisRole should contain the role definition
*/
void void
roleCompile (Term nameterm, Tac tc) roleCompile (Term nameterm, Tac tc)
{ {
@ -1023,7 +1029,13 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
t = levelFind (tc->t1.sym, level); t = levelFind (tc->t1.sym, level);
if (t != NULL) if (t != NULL)
{ {
// Compile a role
roleCompile (t, tc->t2.tac); roleCompile (t, tc->t2.tac);
// singular?
if (tc->t3.value != 0)
{
thisRole->singular = true;
}
} }
else else
{ {

View File

@ -14,6 +14,7 @@ int yylex(void);
char* str; char* str;
struct tacnode* tac; struct tacnode* tac;
Symbol symb; Symbol symb;
int value;
} }
%token <symb> ID %token <symb> ID
@ -30,6 +31,7 @@ int yylex(void);
%token INVERSEKEYS %token INVERSEKEYS
%token UNTRUSTED %token UNTRUSTED
%token USERTYPE %token USERTYPE
%token SINGULAR
%type <tac> spdlcomplete %type <tac> spdlcomplete
%type <tac> spdlrep %type <tac> spdlrep
@ -47,6 +49,8 @@ int yylex(void);
%type <tac> key %type <tac> key
%type <tac> roleref %type <tac> roleref
%type <value> singular
%type <symb> label %type <symb> label
%type <symb> optlabel %type <symb> optlabel
@ -106,15 +110,23 @@ roles : /* empty */
{ $$ = tacCat($1,$2); } { $$ = tacCat($1,$2); }
; ;
role : ROLE ID '{' roledef '}' optclosing role : singular ROLE ID '{' roledef '}' optclosing
{ {
// TODO process singular (0/1)
Tac t = tacCreate(TAC_ROLE); Tac t = tacCreate(TAC_ROLE);
t->t1.sym = $2; t->t1.sym = $3;
t->t2.tac = $4; t->t2.tac = $5;
t->t3.value = $1;
$$ = t; $$ = t;
} }
; ;
singular : /* empty */
{ $$ = 0; }
| SINGULAR
{ $$ = 1; }
;
optclosing : /* empty */ optclosing : /* empty */
{ } { }
| ';' | ';'

View File

@ -243,6 +243,7 @@ roleCreate (Term name)
r->declaredvars = NULL; r->declaredvars = NULL;
r->declaredconsts = NULL; r->declaredconsts = NULL;
r->initiator = 1; //! Will be determined later, if a read is the first action (in compiler.c) r->initiator = 1; //! Will be determined later, if a read is the first action (in compiler.c)
r->singular = false; // by default, a role is not singular
r->next = NULL; r->next = NULL;
return r; return r;
} }

View File

@ -132,6 +132,8 @@ struct role
Termlist declaredvars; Termlist declaredvars;
//! Flag for initiator roles //! Flag for initiator roles
int initiator; int initiator;
//! Flag for singular roles
int singular;
//! Pointer to next role definition. //! Pointer to next role definition.
struct role *next; struct role *next;
}; };

View File

@ -94,6 +94,7 @@ inversekeys { return INVERSEKEYS; }
untrusted { return UNTRUSTED; } untrusted { return UNTRUSTED; }
compromised { return COMPROMISED; } compromised { return COMPROMISED; }
usertype { return USERTYPE; } usertype { return USERTYPE; }
singular { return SINGULAR; }
{id} { {id} {
yylval.symb = mkstring(yytext); yylval.symb = mkstring(yytext);
return ID; return ID;

View File

@ -43,18 +43,21 @@ struct tacnode
Symbol sym; Symbol sym;
struct tacnode *tac; struct tacnode *tac;
char *str; char *str;
int value;
} t1; } t1;
union union
{ {
Symbol sym; Symbol sym;
struct tacnode *tac; struct tacnode *tac;
char *str; char *str;
int value;
} t2; } t2;
union union
{ {
Symbol sym; Symbol sym;
struct tacnode *tac; struct tacnode *tac;
char *str; char *str;
int value;
} t3; } t3;
}; };

View File

@ -1,5 +1,3 @@
- Add 'singular' keyword for roles, and think about support for
strand-space like templates.
- Simple timestamps could be added by prefixing send message before the - Simple timestamps could be added by prefixing send message before the
role, sending any timestamp constants out first to the intruder. These role, sending any timestamp constants out first to the intruder. These
should of course be hidden in the output somehow. should of course be hidden in the output somehow.