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

- Debug of optimization.

Browse Source 
- Put down skeleton of new idea, related to a lemma from Niek Palm's
  work. This needs more investigating though.
This commit is contained in:
ccremers 2004-07-13 15:24:47 +00:00
parent b6806f6aaf
commit 39a2b4878c
1 changed files with 55 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

94
src/modelchecker.c
View File

@ -208,61 +208,77 @@ explorify (const System sys, const int run)
flag = 0; flag = 0;
/* /*
* Special check: if agents have been instantiated in such a way that no more claims need to be evaluated, then we can skip * Special checks after (implicit) choose events; always first in run reads.
* further traversal.
* Two cases: internal read or first read of a run; both are the first event of a run.
*
* Efficiency of the next check heavily relies on lazy L-R evaluation
*/ */
if (rd == sys->runs[run].start && rd->type == READ) if (rd == sys->runs[run].start && rd->type == READ)
{ {
int rid;
if (inTermlist (sys->untrusted, agentOfRun (sys, run))) if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
{ {
/* this run is executed by an untrusted agent, do not explore */ /* this run is executed by an untrusted agent, do not explore */
return 0; return 0;
} }
else /* executed by trusted agent */
{
/* executed by trusted agent, but is there a claim left to explore? */
if (sys->secrets == NULL)
{ /* there are no remaining secrecy claims to be checked */
Roledef rdscan;
int rid;
int validclaim;
rid = 0; /* Special check 1: if agents have been instantiated in such a way that no more claims need to be evaluated, then we can skip
validclaim = 0; * further traversal.
/* check for each run */ */
while (rid < sys->maxruns) if (sys->secrets == NULL)
{ { /* there are no remaining secrecy claims to be checked */
/* are claims in this run evaluated anyway? */ Roledef rdscan;
if (!untrustedAgent (sys, sys->runs[rid].agents)) int validclaim;
{ /* possibly claims to be checked in this run */
rdscan = runPointerGet(sys, rid); rid = 0;
while (rdscan != NULL) validclaim = 0;
/* check for each run */
while (rid < sys->maxruns)
{
/* are claims in this run evaluated anyway? */
if (!untrustedAgent (sys, sys->runs[rid].agents))
{ /* possibly claims to be checked in this run */
rdscan = runPointerGet(sys, rid);
while (rdscan != NULL)
{
if (rdscan->type == CLAIM)
{ {
if (rdscan->type == CLAIM) /* force abort of loop */
{ validclaim = 1;
/* force abort of loop */ rdscan = NULL;
validclaim = 1; rid = sys->maxruns;
rdscan = NULL; }
rid = sys->maxruns; else
} {
else rdscan = rdscan->next;
{
rdscan = rdscan->next;
}
} }
} }
rid++;
}
if (validclaim == 0)
{ /* no valid claims, abort */
return 0;
} }
rid++;
}
if (validclaim == 0)
{ /* no valid claims, abort */
return 0;
} }
} }
/* Special check 2: if all agents in each run send only encrypted stuff, and all agents are trusted,
* there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not
* be violated anymore if they contain no terms that are encrypted with such keys */
//!@todo For now, there is no check that the runs only send publicly encrypted stuff! Just an assumption to be made true using static analysis.
/*
rid = 0;
while (rid < sys->maxruns)
{
if (!untrustedAgent (sys, sys->runs[rid].agents))
{
}
rid++;
}
*/
} }
/* Apparently, all is well, and we can explore further */
if (executeStep (sys, run)) if (executeStep (sys, run))
{ {
/* traverse the system after the step */ /* traverse the system after the step */