201 lines
4.8 KiB
C
201 lines
4.8 KiB
C
|
#ifndef RUNS
|
||
|
#define RUNS
|
||
|
|
||
|
#include "terms.h"
|
||
|
#include "termlists.h"
|
||
|
#include "knowledge.h"
|
||
|
#include "constraints.h"
|
||
|
|
||
|
#define READ 1
|
||
|
#define SEND 2
|
||
|
#define CLAIM 3
|
||
|
|
||
|
#define runPointerGet(sys,run) sys->runs[run].index
|
||
|
#define runPointerSet(sys,run,newp) sys->runs[run].index = newp
|
||
|
|
||
|
struct roledef
|
||
|
{
|
||
|
/* flag for internal actions (overriding normal type) */
|
||
|
int internal;
|
||
|
int type;
|
||
|
Term label;
|
||
|
Term from;
|
||
|
Term to;
|
||
|
Term message;
|
||
|
struct roledef *next;
|
||
|
|
||
|
/* illegal injections */
|
||
|
Knowledge forbidden;
|
||
|
/* knowledge transitions counter */
|
||
|
int knowPhase;
|
||
|
|
||
|
/* evt runid for synchronisation, but that is implied in the
|
||
|
base array */
|
||
|
};
|
||
|
|
||
|
typedef struct roledef *Roledef;
|
||
|
|
||
|
|
||
|
struct role
|
||
|
{
|
||
|
Term nameterm;
|
||
|
Roledef roledef;
|
||
|
Termlist locals;
|
||
|
struct role *next;
|
||
|
};
|
||
|
|
||
|
typedef struct role *Role;
|
||
|
|
||
|
struct protocol
|
||
|
{
|
||
|
Term nameterm;
|
||
|
Role roles;
|
||
|
Termlist rolenames;
|
||
|
Termlist locals;
|
||
|
struct protocol *next;
|
||
|
};
|
||
|
|
||
|
typedef struct protocol *Protocol;
|
||
|
|
||
|
struct run
|
||
|
{
|
||
|
Protocol protocol;
|
||
|
Role role;
|
||
|
Termlist agents;
|
||
|
Roledef index;
|
||
|
Roledef start;
|
||
|
Knowledge know;
|
||
|
};
|
||
|
|
||
|
typedef struct run *Run;
|
||
|
|
||
|
struct varbuf
|
||
|
{
|
||
|
Termlist from;
|
||
|
Termlist to;
|
||
|
Termlist empty;
|
||
|
};
|
||
|
|
||
|
typedef struct varbuf *Varbuf;
|
||
|
|
||
|
struct tracebuf
|
||
|
{
|
||
|
int length;
|
||
|
int reallength;
|
||
|
Roledef *event;
|
||
|
int *run;
|
||
|
int *status;
|
||
|
int *link;
|
||
|
int violatedclaim; // index of violated claim in trace
|
||
|
Knowledge *know;
|
||
|
Termlist requiredterms;
|
||
|
Varbuf variables;
|
||
|
};
|
||
|
|
||
|
struct system
|
||
|
{
|
||
|
int step; // can be managed globally
|
||
|
Knowledge know;
|
||
|
struct parameters *parameters; // misc
|
||
|
/* static run info, maxruns */
|
||
|
Run runs;
|
||
|
|
||
|
/* global */
|
||
|
int maxruns;
|
||
|
|
||
|
/* properties */
|
||
|
Termlist secrets; // integrate secrets list into system
|
||
|
int shortestattack; // length of shortest attack trace
|
||
|
|
||
|
/* switches */
|
||
|
int report;
|
||
|
int prune; // type of pruning
|
||
|
int switch_maxtracelength; // helps to remember the length of the last trace
|
||
|
int maxtracelength; // helps to remember the length of the last trace
|
||
|
int switchM; // memory
|
||
|
int switchT; // time
|
||
|
int switchS; // progress (traversed states)
|
||
|
int porparam; // a multi-purpose integer parameter, passed to the partial order reduction method selected
|
||
|
int latex; // latex output switch
|
||
|
|
||
|
/* traversal */
|
||
|
int traverse; // traversal method
|
||
|
int explore; // boolean: explore states after actions or not
|
||
|
|
||
|
/* counters */
|
||
|
unsigned long int statesLow;
|
||
|
unsigned long int statesHigh;
|
||
|
unsigned long int claims; // number of claims encountered
|
||
|
unsigned long int failed; // number of claims failed
|
||
|
|
||
|
/* matching */
|
||
|
int match; // matching type
|
||
|
int clp; // do we use clp?
|
||
|
|
||
|
/* protocol definition */
|
||
|
Protocol protocols;
|
||
|
Termlist locals;
|
||
|
Termlist variables;
|
||
|
Termlist untrusted;
|
||
|
|
||
|
/* constructed trace pointers, static */
|
||
|
Roledef *traceEvent; // MaxRuns * maxRoledef
|
||
|
int *traceRun; // MaxRuns * maxRoledef
|
||
|
Knowledge *traceKnow; // Maxruns * maxRoledef
|
||
|
|
||
|
/* POR reduction assistance */
|
||
|
int PORphase; // -1: init (all sends), 0...: recurse reads
|
||
|
int PORdone; // simple bit to denote something was done.
|
||
|
int knowPhase; // which knowPhase have we already explored?
|
||
|
Constraintlist constraints; // only needed for CLP match
|
||
|
|
||
|
/* relevant: storage of shortest attack */
|
||
|
struct tracebuf* attack;
|
||
|
};
|
||
|
|
||
|
typedef struct system *System;
|
||
|
|
||
|
System systemInit ();
|
||
|
void systemReset (const System sys);
|
||
|
System systemDuplicate (System fromsys);
|
||
|
void statesPrint (System sys);
|
||
|
void statesPrintShort (System sys);
|
||
|
void systemDestroy (System sys);
|
||
|
void systemDone (System sys);
|
||
|
void ensureValidRun (System sys, int run);
|
||
|
void runAdd (System sys, int run, int type, Term label, Term from, Term to,
|
||
|
Term msg);
|
||
|
void roledefPrint (Roledef rd);
|
||
|
void runPrint (Roledef rd);
|
||
|
void runsPrint (System sys);
|
||
|
Term agentOfRunRole (const System sys, const int run, const Term role);
|
||
|
Term agentOfRun (const System sys, const int run);
|
||
|
Roledef roledefDuplicate1 (const Roledef rd);
|
||
|
Roledef roledefDuplicate (Roledef rd);
|
||
|
void roledefDelete (Roledef rd);
|
||
|
void roledefDestroy (Roledef rd);
|
||
|
void roleInstance (const System sys, const Protocol protocol, const Role role,
|
||
|
const Termlist tolist);
|
||
|
Roledef roledefInit (int type, Term label, Term from, Term to, Term msg);
|
||
|
Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to,
|
||
|
Term msg);
|
||
|
void systemStart (System sys);
|
||
|
void indentActivate ();
|
||
|
void indentSet (int i);
|
||
|
void indent ();
|
||
|
|
||
|
Protocol protocolCreate (Term nameterm);
|
||
|
Role roleCreate (Term nameterm);
|
||
|
void locVarPrint (Termlist tl);
|
||
|
void protocolPrint (Protocol p);
|
||
|
void protocolsPrint (Protocol p);
|
||
|
void rolePrint (Role r);
|
||
|
void rolesPrint (Role r);
|
||
|
int untrustedAgent (System sys, Termlist agents);
|
||
|
int getMaxTraceLength (const System sys);
|
||
|
void agentsOfRunPrint (const System sys, const int run);
|
||
|
void violatedClaimPrint (const System sys, int i);
|
||
|
int attackLength(struct tracebuf* tb);
|
||
|
|
||
|
#endif
|