NEW: Added SID & SKR dummy claims.
This allows for input file reuse among branches (i.e. compromise).
This commit is contained in:
parent
04787e5516
commit
6afcfe1d10
@ -2368,10 +2368,13 @@ arachneClaimTest (Claimlist cl)
|
||||
|
||||
//! Arachne single claim inspection
|
||||
int
|
||||
arachneClaim (Claimlist cl)
|
||||
arachneClaim ()
|
||||
{
|
||||
// Skip the dummy claims
|
||||
if (!isTermEqual (cl->type, CLAIM_Empty))
|
||||
Claimlist cl;
|
||||
|
||||
// Skip the dummy claims or SID markers
|
||||
cl = sys->current_claim;
|
||||
if (!isClaimSignal (cl))
|
||||
{
|
||||
// Some claims are always true!
|
||||
if (!cl->alwaystrue)
|
||||
@ -2472,9 +2475,13 @@ arachne ()
|
||||
/**
|
||||
* Check each claim
|
||||
*/
|
||||
if (arachneClaim (cl))
|
||||
sys->current_claim = cl;
|
||||
if (isClaimRelevant (cl)) // check for any filtered claims (switch)
|
||||
{
|
||||
count++;
|
||||
if (arachneClaim ())
|
||||
{
|
||||
count++;
|
||||
}
|
||||
}
|
||||
|
||||
// next
|
||||
|
68
src/claim.c
68
src/claim.c
@ -39,6 +39,7 @@
|
||||
#include "color.h"
|
||||
#include "cost.h"
|
||||
#include "timer.h"
|
||||
#include "compiler.h"
|
||||
|
||||
//! When none of the runs match
|
||||
#define MATCH_NONE 0
|
||||
@ -816,7 +817,7 @@ add_claim_specifics (const System sys, const Claimlist cl, const Roledef rd,
|
||||
// per default, all agents are trusted
|
||||
sys->trustedRoles = NULL;
|
||||
|
||||
if (cl->type == CLAIM_Secret)
|
||||
if (cl->type == CLAIM_Secret || cl->type == CLAIM_SKR)
|
||||
{
|
||||
int newgoals;
|
||||
int flag;
|
||||
@ -1153,3 +1154,68 @@ claimStatusReport (const System sys, Claimlist cl)
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
//! Check whether this claim needs to be verified according to filter settings
|
||||
int
|
||||
isClaimRelevant (const Claimlist cl)
|
||||
{
|
||||
// Is there something to filter?
|
||||
if (switches.filterProtocol == NULL)
|
||||
{
|
||||
// No: consider all claims
|
||||
return true;
|
||||
}
|
||||
else
|
||||
{
|
||||
// only this protocol
|
||||
if (!isStringEqual
|
||||
(switches.filterProtocol,
|
||||
TermSymb (((Protocol) cl->protocol)->nameterm)->text))
|
||||
{
|
||||
// not this protocol; return
|
||||
return false;
|
||||
}
|
||||
// and maybe also a specific cl->label?
|
||||
if (switches.filterLabel != NULL)
|
||||
{
|
||||
if (cl->label == NULL)
|
||||
{
|
||||
return false;
|
||||
}
|
||||
else
|
||||
{
|
||||
Term t;
|
||||
|
||||
t = cl->label;
|
||||
while (isTermTuple (t))
|
||||
{
|
||||
t = TermOp2 (t);
|
||||
}
|
||||
if (!isStringEqual (switches.filterLabel, TermSymb (t)->text))
|
||||
{
|
||||
// not this label; return
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
//! Check whether a claim is really just a signal, and not a claim
|
||||
/**
|
||||
* This piece of code effectively decides what is a signal and what not
|
||||
*/
|
||||
int
|
||||
isClaimSignal (const Claimlist cl)
|
||||
{
|
||||
if (isTermEqual (cl->type, CLAIM_Empty))
|
||||
{
|
||||
return true;
|
||||
}
|
||||
if (isTermEqual (cl->type, CLAIM_SID))
|
||||
{
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
@ -40,5 +40,7 @@ int add_claim_specifics (const System sys, const Claimlist cl, const
|
||||
void count_false_claim (const System sys);
|
||||
int property_check (const System sys);
|
||||
int claimStatusReport (const System sys, Claimlist cl);
|
||||
int isClaimRelevant (const Claimlist cl);
|
||||
int isClaimSignal (const Claimlist cl);
|
||||
|
||||
#endif
|
||||
|
@ -42,4 +42,6 @@ void levelTacDeclaration (Tac tc, int isVar);
|
||||
#define levelVar(s) symbolDeclare(s,1)
|
||||
#define levelConst(s) symbolDeclare(s,0)
|
||||
|
||||
int isStringEqual (const char *s1, const char *s2);
|
||||
|
||||
#endif
|
||||
|
@ -48,6 +48,8 @@ Term CLAIM_Nisynch;
|
||||
Term CLAIM_Niagree;
|
||||
Term CLAIM_Empty;
|
||||
Term CLAIM_Reachable;
|
||||
Term CLAIM_SID;
|
||||
Term CLAIM_SKR;
|
||||
|
||||
Term AGENT_Alice;
|
||||
Term AGENT_Bob;
|
||||
@ -85,6 +87,9 @@ specialTermInit (const System sys)
|
||||
langcons (CLAIM_Empty, "Empty", TERM_Claim);
|
||||
langcons (CLAIM_Reachable, "Reachable", TERM_Claim);
|
||||
|
||||
langcons (CLAIM_SID, "SID", TERM_Claim); // claim specifying session ID
|
||||
langcons (CLAIM_SKR, "SKR", TERM_Claim); // claim specifying session key : doubles as secrecy claim
|
||||
|
||||
/* Define default PKI using PK/SK/K */
|
||||
langcons (TERM_PK, "pk", TERM_Function);
|
||||
langcons (TERM_SK, "sk", TERM_Function);
|
||||
|
@ -42,6 +42,8 @@ extern Term CLAIM_Nisynch;
|
||||
extern Term CLAIM_Niagree;
|
||||
extern Term CLAIM_Empty;
|
||||
extern Term CLAIM_Reachable;
|
||||
extern Term CLAIM_SID;
|
||||
extern Term CLAIM_SKR;
|
||||
|
||||
extern Term AGENT_Alice;
|
||||
extern Term AGENT_Bob;
|
||||
|
Loading…
Reference in New Issue
Block a user