Commit Graph

776 Commits

Author SHA1 Message Date
Cas Cremers
a03f06ea41 BUGFIX: Auto-claim naming scheme was context dependent.
The automatic mechanism to assign labels to claims was dependent on the
context. In practice, a claim could get a different label when analyzed in
isolation compared to when analyzed in parallel with some other protocols. This
caused problems for the multi-protocol analysis.
2011-01-27 14:12:51 +01:00
Cas Cremers
fea2bcf477 Reindenting code. 2011-01-25 17:33:12 +01:00
Cas Cremers
1814a2d7b3 BUGFIX: Removed obsolete code that was destroying commit/agreement functionality when filtering.
This is now (and has been for a while) handled by other code.
2011-01-25 17:30:59 +01:00
Cas Cremers
f883499d07 CHANGE: Changed setup of running & commit.
Now:

claim(A,Commit,B,data) => claim(B,Running,A,data) and also B is running the right protocol and role.
2011-01-24 17:32:24 +01:00
Cas Cremers
fda39f7eab BUGFIX: Skipping running/commit signals caused bugs in graphviz output. 2011-01-21 17:40:10 +01:00
Cas Cremers
5f7138c300 BUGFIX: Partial implementation of chosen name attacks could yield false type flaw attacks.
For the typed model, this was not an issue.
2011-01-18 17:03:20 +01:00
Cas Cremers
b7ab9aefeb NEW: Added default SessionKey type. 2011-01-04 15:50:47 +01:00
Cas Cremers
66e18deb3f NEW: Added claims: Commit and Running.
There are two new claims:

  claim(X,Commit,t)  : check for agreement on data
  claim(X,Running,t) : signaling claim

The property checked is that each claim Commit needs to be preceded by a Running
with an identical term t.

Cherry-picked from commit 99a6be00e9d3d219ec73665607e8a3a7d65d04d1
2011-01-04 15:50:25 +01:00
Cas Cremers
2fb0ecde97 NEW: Added Aliveness and Weak Agreement claims. 2011-01-04 15:50:25 +01:00
Cas Cremers
6afcfe1d10 NEW: Added SID & SKR dummy claims.
This allows for input file reuse among branches (i.e. compromise).
2011-01-04 15:50:25 +01:00
Cas Cremers
9624c49885 Disable some aggressive error reporting: unclear why this is actually invalid per se
in the presence of agent name variables (role names) with non-basic typing.
2010-12-31 15:43:00 +01:00
Cas Cremers
266e5fb26b BRUTUS: Added special build script.
Originates in newCompromise branch.
2010-11-11 12:14:49 +01:00
Cas Cremers
01eb5854cf EFFICIENCY: If a new dependency overlaps with an old one, we don't have to recompute the closure. 2010-11-11 10:37:18 +01:00
Cas Cremers
6cd8007ab0 EFFICIENCY: New (default) heuristic.
Given that sk/pk/k are now hardcoded, we can exploit their occurrences with this
new heuristic.

The heuristic can now scan for the lowest term depth at which either sk or k occur.
This will cause the heuristic to favor looking for sk, then sk(x), and only later
other terms. In a small test this was twice as fast. For protocols based on pk only
the performance loss should be negligible.

The old heuristic was 162, now it is 162+512 = 674.
2010-11-11 10:37:18 +01:00
Cas Cremers
fcf694dbd9 CLEANUP: Reindenting code. 2010-11-11 00:09:16 +01:00
Cas Cremers
619ecf7673 Added commented-out code to use llvm as a compiler instead of gcc when needed. 2010-11-11 00:02:36 +01:00
Cas Cremers
c25f6efd6a SPDL: Introduced 'hashfunction f;' construct to input language. 2010-11-11 00:01:31 +01:00
Cas Cremers
4ac74f321f SPDL: Introduced preconstructed PKI with pk/sk/k.
Introduced K(A1...AN) constant function for symmetric pre-shared keys.
Added inverses (pk,sk) as default constructs.
2010-11-11 00:01:31 +01:00
Cas Cremers
03a8a1b6e7 BUGFIX: Redundant parameter to eprint. 2010-11-11 00:01:17 +01:00
Cas Cremers
2557d308bb CLEANUP: Add timing output to proof output. 2010-11-11 00:01:12 +01:00
Cas Cremers
6b3d572e3b BUGFIX: Fixed long-standing bug with timer values, wrongly using CLOCKS_PER_SEC. 2010-11-10 23:55:57 +01:00
Cas Cremers
5c53d4bb9e Better reindent script (from newCompromise branch) 2010-11-10 23:55:21 +01:00
Cas Cremers
6d9d89eca2 Introduced 'fresh' for fresh value generation and added deprecation warning for 'const' usage. 2010-11-10 10:37:57 +01:00
Cas Cremers
519a9d0a81 Added factored-out 'warning_pre' function. 2010-11-10 10:37:57 +01:00
Cas Cremers
d633a62f0d BUGFIX: C-minimality was tripping over claims. 2009-01-28 20:45:58 +01:00
Cas Cremers
f21c02e772 BUGFIX: Build scripts did not always build unix version correctly. 2008-09-15 16:48:39 +02:00
Cas Cremers
6ffdda4a3c BUGFIX: Graph output correct removal of function applications.
The graph output edge remover was incorrect, and would also
remove applications that were not completely triggered by M_0 alone.
2008-08-26 13:25:43 +02:00
Cas Cremers
77cc97c03b Added a note for code cleanup. 2008-08-21 22:32:19 +02:00
Cas Cremers
0c06cb7a30 Added debug build script. 2008-08-21 21:57:42 +02:00
Cas Cremers
3e3c2d7b07 Rewrote some code for humans to read, i.e. strcmp wrapper. 2008-08-21 16:59:05 +02:00
Cas Cremers
8f01637528 Output should also yield 'recv' instead of 'read'. 2008-08-21 16:58:57 +02:00
Cas Cremers
aaf27779a3 Allow for use of RECV instead of READ.
Read will become deprecated later on.
2008-08-21 16:58:53 +02:00
Cas Cremers
739f59174f Removed unused functions. 2008-08-21 16:58:12 +02:00
Cas Cremers
1a7aa73b26 Created a small program that can find unused functions. 2008-08-21 16:56:12 +02:00
Cas Cremers
a0a377a84f Added switch to disable verbose exit codes.
In the near future, the default exit code behavior should be made obsolete anyway,
as the exit codes are not a nice way to report status.
It used to be convenient for shell scripting in early times,
when the parallel tests were run using the forward model
checker, but no modern script should be relying on it.
2008-06-16 18:57:28 +02:00
Cas Cremers
c729d13a00 Reindent of the code revealed that some was not indented nicely yet. Silly. 2008-03-23 15:56:09 +09:00
Cas Cremers
27521d0e87 Added notes. 2008-03-13 10:24:13 +01:00
Cas Cremers
0709539737 Merge branch 'master' of ssh://cremersc@buckleburg.inf.ethz.ch/home/cremersc/repos/scyther 2008-01-28 15:25:46 +01:00
Cas Cremers
a7c1d8c696 Improved handling of cases with untyped variables.
When untyped variables occur, the encryption level depth pruning is for
now unjustified. Maybe we can get a proof later.  Previously this was
hidden, which was a bad design decision.  Now the output is much
clearer.
2008-01-28 15:23:40 +01:00
Cas Cremers
03522b7108 Try to not draw duplicate arrows.
This cleans up some graphs rather nicely. There is only one potential
drawback (not observed in practive):
If two bindings have the same from/to, but different interpretations,
we might lose information. In particular the 'select' intermediate nodes might
pose a problem and we would be better off by not having any interpretation on
what is selected.
2008-01-16 11:55:15 +01:00
Cas Cremers
bf24312fb1 Disabled intruder knowledge computation.
Isolated problem causing segfault identified by Simon Meier.
2008-01-10 16:50:02 +01:00
Cas Cremers
ce9891d351 Disabled well-formedness temporarily.
Simon Meier found some problems with the draft implementation, so it is disabled
for now.
2008-01-10 16:09:24 +01:00
Cas Cremers
2d45daa8ee Introduced '-c,--characterize' switches for complete characterization.
This switch was previously known as '--state-space', but the new name is
much better.

Backwards compatibility:

'-c' was previously used by '--check', so check is now abbreviated to
'-C'.

'-s,--state-space' still works but is from now on considered to be
deprecated.
2007-11-15 21:49:56 +01:00
Cas Cremers
08bbdded3c Minor cleanup. 2007-10-22 21:42:43 +02:00
Cas Cremers
a6370726ef Cleanup. 2007-10-22 21:14:06 +02:00
Cas Cremers
b013440c8b Merge branch 'Todo' 2007-09-18 16:09:05 +02:00
Cas Cremers
2107d76532 Proof output improved for occurrences of the Athena problem. 2007-09-18 15:36:11 +02:00
Cas Cremers
59bcb18fec Caught Athena problem case.
I've added a marked for the Athena problem case, and now no more false 'complete proof' results are produced.
However, the tool reports, 'no attack within bounds', which is slightly inaccurate
depending on the interpretatio of 'bounds'.
2007-09-18 15:27:41 +02:00
Cas Cremers
8a2ae84f35 Added incompleteness marker for the untyped variables and MGDU set problem. 2007-09-17 16:54:17 +02:00
Cas Cremers
a93b555b1a Added cast to solve long-standing compilation warning.
Note that the cast does not seem to be needed after manual inspection, but
the compiler insists.
2007-09-17 16:53:37 +02:00