Merge branch 'manual' into 'master'.
This commit is contained in:
Cas Cremers
commit
52e23f5c86
@ -1,86 +0,0 @@
|
|||||||
#
|
|
||||||
# Scyther Makefile
|
|
||||||
#
|
|
||||||
|
|
||||||
#
|
|
||||||
# DEBUG or optimization settings: uncomment a single line:
|
|
||||||
#
|
|
||||||
CFLAGS = -g3 -D DEBUG # default usage, for e.g. with valgrind
|
|
||||||
#CFLAGS = -g3 -D DEBUG -pg # for code profiling with gprof
|
|
||||||
#CFLAGS = -O3 -static -finline-functions -fomit-frame-pointer
|
|
||||||
|
|
||||||
#
|
|
||||||
# Compiler and linkage
|
|
||||||
#
|
|
||||||
CC = gcc
|
|
||||||
# Note that these paths must include the path to the argtable library.
|
|
||||||
CPPFLAGS = -I/scratch/ccremers/include -I/usr/local/include -Wall
|
|
||||||
LDFLAGS = -L/scratch/ccremers/lib -L/usr/local/lib
|
|
||||||
LOADLIBS = -lfl
|
|
||||||
LDLIBS = -largtable2
|
|
||||||
OPTIONS = ${CPPFLAGS} ${CFLAGS} ${LDFLAGS}
|
|
||||||
|
|
||||||
#
|
|
||||||
# Module set for the modelchecker
|
|
||||||
#
|
|
||||||
MODULES=memory.o terms.o termlists.o symbols.o knowledge.o runs.o modelchecker.o \
|
|
||||||
report.o debug.o mgu.o substitutions.o \
|
|
||||||
match_basic.o \
|
|
||||||
match_clp.o constraints.o \
|
|
||||||
output.o latex.o \
|
|
||||||
varbuf.o tracebuf.o attackminimize.o \
|
|
||||||
tac.o parser.o compiler.o
|
|
||||||
|
|
||||||
#
|
|
||||||
# Dependencies
|
|
||||||
#
|
|
||||||
MODELCHECKER = ${MODULES} main.o
|
|
||||||
|
|
||||||
all: scyther tags
|
|
||||||
|
|
||||||
${Target}.o: ${Target}.c
|
|
||||||
$(CC) $(OPTIONS) ${Target}.c -c
|
|
||||||
|
|
||||||
scanner.c: scanner.lex
|
|
||||||
flex scanner.lex
|
|
||||||
cp lex.yy.c scanner.c
|
|
||||||
|
|
||||||
tok.h: parser.c
|
|
||||||
|
|
||||||
parser.c: parser.y
|
|
||||||
bison -d -v parser.y
|
|
||||||
cp parser.tab.c parser.c
|
|
||||||
cmp -s parser.tab.h tok.h || cp parser.tab.h tok.h
|
|
||||||
|
|
||||||
tags: *.c *.h
|
|
||||||
ctags *.c *.h
|
|
||||||
|
|
||||||
modules: $(MODULES)
|
|
||||||
|
|
||||||
scyther: scanner.o $(MODELCHECKER)
|
|
||||||
$(CC) $(OPTIONS) $(MODELCHECKER) -o scyther $(LOADLIBS) $(LDLIBS)
|
|
||||||
|
|
||||||
ptestmain.o scanner.o : tok.h
|
|
||||||
|
|
||||||
#
|
|
||||||
# Cleanup
|
|
||||||
#
|
|
||||||
clean:
|
|
||||||
rm -f *.o
|
|
||||||
rm -f scyther
|
|
||||||
rm -f scanner.c
|
|
||||||
rm -f parser.c
|
|
||||||
rm -f tok.h
|
|
||||||
#
|
|
||||||
# Clean and rebuild: 'make new'
|
|
||||||
#
|
|
||||||
new:
|
|
||||||
make clean
|
|
||||||
make all
|
|
||||||
|
|
||||||
#
|
|
||||||
# Make doxygen reference manuals. (in ../refman)
|
|
||||||
#
|
|
||||||
refman: doxyconfig
|
|
||||||
doxygen doxyconfig
|
|
||||||
|
|
||||||
119
src/bugs.txt
119
src/bugs.txt
@ -1,119 +0,0 @@
|
|||||||
--+++ Crititcal Bugs
|
|
||||||
|
|
||||||
* soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version.
|
|
||||||
* './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. The main reason is that the Archne engine uses runs in a different way.
|
|
||||||
Maybe it is best to disable --increment rules for non-ModelChecker verification.
|
|
||||||
|
|
||||||
---+++ Bugs
|
|
||||||
|
|
||||||
* Problem with goal bindings: instantiation of variable with a tuple might
|
|
||||||
introduce a tuple goal, which is forbidden. We must find a way to deal with this. This typically occurs in type flaw searches.
|
|
||||||
* Arachne seems to trip over claims with empty prec sets. Maybe we
|
|
||||||
simply should not test these.
|
|
||||||
* Splice/AS does not work well because priority key search stumbles over the
|
|
||||||
public key search stuff. That is a flaw in the heuristic: we should not look
|
|
||||||
for anything that is in the intruder knowledge already. In fact, it is a
|
|
||||||
problem with branching. We should not look for PK(X), even if X is a
|
|
||||||
variable. Priority should go to keys of which the constructor is not in M_0,
|
|
||||||
maybe that heuristic works.
|
|
||||||
However, there seems to be an infinite loop for this in the algorithm, which
|
|
||||||
I did not anticipate. Investigate!
|
|
||||||
<br>
|
|
||||||
Maybe self-loops are the problem. This has to do with tuple alternation
|
|
||||||
decoding. Consider re-introducing explicit intruder strands OR self-loop
|
|
||||||
pruning.
|
|
||||||
|
|
||||||
---+++ Would like to have
|
|
||||||
|
|
||||||
---++++ ArachneEngine
|
|
||||||
|
|
||||||
* There is no good test on the correct workings of
|
|
||||||
add_goals/destruction of these. We can test this if after
|
|
||||||
termination, we have 0 goals; for this we need to store the
|
|
||||||
initially added goals as well. Furthermore, we can generate an
|
|
||||||
error when <0 goals occur.
|
|
||||||
* Consider where in Arachne dependency graph is used. If this is only for
|
|
||||||
pruning states, we can construct it there only. However, the base 'role
|
|
||||||
defs/bindings' graph might be re-used.
|
|
||||||
* Add switch for arachne to prune encryption levels when using -m2.
|
|
||||||
* To store attacks for arachne, maybe the following is needed:
|
|
||||||
* The roles for each run
|
|
||||||
* The variable bindings for all (local) variables
|
|
||||||
* The goal bindings
|
|
||||||
* Agent terms must have keylevel 0; enforce this!
|
|
||||||
* Select_goal should consider, for singular variables, whether their
|
|
||||||
type can be found in M_0. If so, the goal can be ignored.
|
|
||||||
* Fix 'never sent secrets' list, that are e.g. secret keys of regular agents
|
|
||||||
and such. The intruder can never learn these, we need this for pruning.
|
|
||||||
If a goal is such a term, we prune. Investigate how this can be incorporated.
|
|
||||||
Investigate also whether this actually makes a difference.
|
|
||||||
* Make 'generate_trace_bindings' to create the bindings for a given trace.
|
|
||||||
Note that there can be multiple solutions; for now, simply try to take the
|
|
||||||
shortest one.
|
|
||||||
|
|
||||||
---++++ ModelChecker
|
|
||||||
|
|
||||||
* For secrecy, one trusted agent and one untrusted agent suffices.
|
|
||||||
Implement this in the modelchecker.
|
|
||||||
* Implement delayed protocol compiler (on run demand only) for the modelchecker?
|
|
||||||
|
|
||||||
---++++ Misc
|
|
||||||
|
|
||||||
* Make different error codes for compilation error/ other error. This can be
|
|
||||||
useful for scripts. However, it might shift some constants for the Elegast
|
|
||||||
scripts.
|
|
||||||
* Rewrite termMguTerm such that it iterates and adapt all functions
|
|
||||||
using it. This is to allow for associative tupling later.
|
|
||||||
* Fix constants in intruder knowledge. Auto add single one of each type,
|
|
||||||
when typed expl. Add single constant when untyped. Fix this also in
|
|
||||||
semantics, and add proof to establish sufficiency.
|
|
||||||
* Fix function handling (signatures).
|
|
||||||
* Move initial intruder knowledge maybe into the title of the MSC.
|
|
||||||
* Implement run knowledge, and use this in protocol compiler.
|
|
||||||
* Introduce 'Ticket' default type in the compiler, along with some
|
|
||||||
handling for that.
|
|
||||||
* The 'choose' operator must always be typed, I think. Yes.
|
|
||||||
* The woolam-ce is incorrect because it is illegal to have a variable
|
|
||||||
term in a key that is read, by CMV semantics. I don't know what it
|
|
||||||
means for CE semantics (yet).
|
|
||||||
* Idea: run bla.bla(params) [compromised <localterm> [,<localterm>] ];
|
|
||||||
1. These local terms are given to the intruder. Technically this
|
|
||||||
should only happen _after_ they are first sent in the run. Maybe add
|
|
||||||
this to send semantics: if termOccurs(sendterm, compromisedterm) then
|
|
||||||
add compromisedterm to M, remove compromisedterm from list of terms to
|
|
||||||
compromise.
|
|
||||||
1. All claims in the run are ignored (add untrusted flag to run)
|
|
||||||
Alternative: run x.x(x) untrusted; or just compromised, to give up
|
|
||||||
all constants.
|
|
||||||
Note this is not sufficient yet, because it does not consider any
|
|
||||||
partner runs. Maybe declare a 'compromised' section first; other runs
|
|
||||||
will only activate after these have completed. Note this is much more
|
|
||||||
expensive.
|
|
||||||
* Woolam-ce gives nothing. But then again, it's a wrong impl.
|
|
||||||
* Global/protocol variables should not exist in the current system.
|
|
||||||
* run nsl.initiator(alice, all Agent) constructs?
|
|
||||||
* 'all' would generate the roles with the corresponding type.
|
|
||||||
* or maybe for clarity/complexity control: use 'runs' for constructs
|
|
||||||
with 'all' in it.
|
|
||||||
* Maybe function application ought to be a different basic term type.
|
|
||||||
* After role construction, msc consistency can be checked.
|
|
||||||
* Reduce knowledge to a simple term list? That would simplify a number
|
|
||||||
of things, and also allow for easier addition of stuff.
|
|
||||||
* How is % notation handled in Casper?
|
|
||||||
* Vernam encryption?
|
|
||||||
|
|
||||||
---++++ ConstraintLogic (and thus obsolete)
|
|
||||||
|
|
||||||
* CLP: variables in keys must be branched: maybe even in three situations
|
|
||||||
(have key and contents, have inverse key and content, nothing)
|
|
||||||
* How should claims behave (trusted/untrusted) wrt uninstantiated
|
|
||||||
agents? Branch again? That's what is causing the nsl3-var problem.
|
|
||||||
* Constraints might be a part of a knowledge thing, because with we
|
|
||||||
might now have a number of local knowledge sets, each with their own
|
|
||||||
constraint sets. That doesn't make it easier though :( and will cause
|
|
||||||
some performance loss I suppose. Each local set has to remain
|
|
||||||
solveable as well.
|
|
||||||
* Issue: how do untrusted claims work in the context of an intruder?
|
|
||||||
Claim must be checked if it can be solved such that at least one of
|
|
||||||
the agents is trusted.
|
|
||||||
|
|
||||||
@ -6,13 +6,19 @@ Needed:
|
|||||||
|
|
||||||
gcc
|
gcc
|
||||||
If you don't know what this is, please stop reading.
|
If you don't know what this is, please stop reading.
|
||||||
scons
|
cmake
|
||||||
A Python script set to replace the make etc. toolchain.
|
A Makefile generator, available on almost any platform.
|
||||||
|
|
||||||
For cross-compilation (Windows):
|
For cross-compilation (Windows):
|
||||||
|
|
||||||
[mingw32][universe]
|
[mingw32][universe]
|
||||||
GCC variant to compile for windows + w32 binutils.
|
GCC variant to compile for windows + w32 binutils.
|
||||||
|
|
||||||
Use 'scons arch=windows' to generate the binary.
|
|
||||||
|
The best is to simply execute:
|
||||||
|
|
||||||
|
./build.sh
|
||||||
|
|
||||||
|
This should compile everything for your platform and will copy the
|
||||||
|
binaries into the correct location.
|
||||||
|
|
||||||
|
|||||||
@ -1,46 +0,0 @@
|
|||||||
Language
|
|
||||||
--------
|
|
||||||
|
|
||||||
language := (<def>)*
|
|
||||||
def := (<directive> | <protocol> | <rundef> | <unstrusted>)
|
|
||||||
|
|
||||||
//directive := <dir_require>
|
|
||||||
//dir_require := require <filename>;
|
|
||||||
|
|
||||||
protocol := protocol <protocolname> ( <rolelist> ) { <roledef>* } optsc
|
|
||||||
protocolname := <id>
|
|
||||||
|
|
||||||
intruderknow := public <termlist>;
|
|
||||||
roledef := role <rolename> { <actions> } optsc
|
|
||||||
rolename := <id>
|
|
||||||
actions := (<action>;)+
|
|
||||||
action := (<read> | <send> | <claim>)
|
|
||||||
decl := (<const> | <var>)+
|
|
||||||
const := const <termlist> [ : <typeterm> ];
|
|
||||||
var := var <termlist> [ : <typelist> ];
|
|
||||||
|
|
||||||
read := read [_<label>] (<term>,<term>,<term>);
|
|
||||||
send := send [_<label>] (<term>,<term>,<term>);
|
|
||||||
claim := claim [_<label>] (<term>,<termlist>);
|
|
||||||
label := <id>;
|
|
||||||
|
|
||||||
rundef := <protocolname>.<rolename> ( <instancelist> ) ;
|
|
||||||
instancelist := (<agent>|<typeterm>)*
|
|
||||||
|
|
||||||
agent := <term>
|
|
||||||
typeterm := <term>
|
|
||||||
typelist := <termlist>
|
|
||||||
|
|
||||||
untrusted := untrusted <termlist>;
|
|
||||||
|
|
||||||
termlist := <term> [, <termlist>]
|
|
||||||
term := (<baseterm> | <encterm> | <tupleterm> | <function>)
|
|
||||||
encterm := { <term> } <term>
|
|
||||||
function := <term> ( <term> )
|
|
||||||
baseterm := (<variable> | <const>)
|
|
||||||
variable := <id>
|
|
||||||
const := <id>
|
|
||||||
|
|
||||||
optsc := [ ; ]
|
|
||||||
id := (<digit>|<uppercase>|<lowercase>)+
|
|
||||||
|
|
||||||
@ -1,3 +0,0 @@
|
|||||||
- GNU getopt
|
|
||||||
- GNU bison/flex
|
|
||||||
- de rest (c) Cas
|
|
||||||
@ -1,17 +0,0 @@
|
|||||||
- (!!) Are the Arachne rules for keys that are variables sane? E.g. what
|
|
||||||
is their inverse key? Check! Intuition: one cannot know what the
|
|
||||||
inverse is of a non-instantiated key variable, given the current
|
|
||||||
semantics, if asymmetric keys are allowed.
|
|
||||||
Consequence: the current implementation is just fine, because
|
|
||||||
asymmetric key variables cannot be defined in the language. Thus, the
|
|
||||||
rules are fine. Investigate for the other case.
|
|
||||||
- If no attack/state output is needed, maybe the attack heuristic should
|
|
||||||
be simpler (which means just weighting the trace length etc.) in order
|
|
||||||
to avoid uneccesary continuation of the search. Maybe even stop
|
|
||||||
altogether after finding *an* attack.
|
|
||||||
- For the TimeStamps etc, we can implement an 'auto-leak' of such local
|
|
||||||
constants. This should works also with a modifier of sorts (e.g.
|
|
||||||
'predictable') and such constants should be leaked to the intruder at
|
|
||||||
the start of the run, possibly by prefixing a send.
|
|
||||||
- knowledgeAddTerm might be improved by scanning through key list only with
|
|
||||||
things that are newly added.
|
|
||||||
@ -1,25 +0,0 @@
|
|||||||
// BAN modified version of the yahalom protocol
|
|
||||||
// Type flaw
|
|
||||||
|
|
||||||
usertype Server;
|
|
||||||
|
|
||||||
const a,b,c : Agent;
|
|
||||||
const s : Server;
|
|
||||||
secret k : Function;
|
|
||||||
|
|
||||||
protocol yahalomBan(A,B,S)
|
|
||||||
{
|
|
||||||
role B
|
|
||||||
{
|
|
||||||
const nb;
|
|
||||||
var na;
|
|
||||||
var kab;
|
|
||||||
|
|
||||||
read_!1(A,B, A,na,B,S);
|
|
||||||
send_!2(B,S, B,nb, {A,na}k(B,S) );
|
|
||||||
read_!4(A,B, {A,kab,nb}k(B,S) , {nb}kab );
|
|
||||||
claim_6(B, Secret,kab);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
24
src/todo.txt
24
src/todo.txt
@ -14,9 +14,9 @@
|
|||||||
cumbersome and might impact on performance. Alternatively, iterators
|
cumbersome and might impact on performance. Alternatively, iterators
|
||||||
can be implemented as macros, which is probably the fastest, but maybe
|
can be implemented as macros, which is probably the fastest, but maybe
|
||||||
less readable.
|
less readable.
|
||||||
- --check is slightly f***ed up because there is no good semantics for
|
- The (currently not advised) switch --check is slightly off because
|
||||||
the --disable intruder check. As a result, it is now too strict can
|
there is no good semantics for the --disable intruder check. As a
|
||||||
cause correct protocols to fail. Fix.
|
result, it is now too strict can cause correct protocols to fail. Fix.
|
||||||
- When *not* asking for attack output, maybe we should default to
|
- When *not* asking for attack output, maybe we should default to
|
||||||
--prune = 1. Then, if we ask for --xml output or --dot, we do:
|
--prune = 1. Then, if we ask for --xml output or --dot, we do:
|
||||||
if --prune == 1 then --prune == 2 now :) unless otherwise specified.
|
if --prune == 1 then --prune == 2 now :) unless otherwise specified.
|
||||||
@ -52,3 +52,21 @@
|
|||||||
- SConstruct file should check whether ctags actually exists (avoiding
|
- SConstruct file should check whether ctags actually exists (avoiding
|
||||||
errors)
|
errors)
|
||||||
- Proof output should be XML, with an external converter to dot format.
|
- Proof output should be XML, with an external converter to dot format.
|
||||||
|
- Are the Arachne rules for keys that are variables sufficiently sane in
|
||||||
|
general? E.g. what is their inverse key? Intuition: one cannot know
|
||||||
|
what the inverse is of a non-instantiated key variable, given the
|
||||||
|
current semantics, if asymmetric keys are allowed. Consequence: the
|
||||||
|
current implementation is just fine, because asymmetric key variables
|
||||||
|
cannot be defined in the language. Thus, the rules are fine.
|
||||||
|
Investigate for future extensions what the consequences of this are.
|
||||||
|
- If no attack/state output is needed, maybe the attack heuristic should
|
||||||
|
be simpler (which means just weighting the trace length etc.) in order
|
||||||
|
to avoid uneccesary continuation of the search. Maybe even stop
|
||||||
|
altogether after finding *an* attack.
|
||||||
|
- For the TimeStamps etc, we can implement an 'auto-leak' of such local
|
||||||
|
constants. This should works also with a modifier of sorts (e.g.
|
||||||
|
'predictable') and such constants should be leaked to the intruder at
|
||||||
|
the start of the run, possibly by prefixing a send.
|
||||||
|
- knowledgeAddTerm might be improved by scanning through key list only with
|
||||||
|
things that are newly added.
|
||||||
|
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user