Commit Graph

184 Commits

Author SHA1 Message Date
ccremers
8d66dc48fd - Fixed intruder generated value displays. 2006-12-05 10:10:17 +00:00
ccremers
31f1753e4e - Added malloc wrappers for OSX builds. 2006-09-12 16:17:49 +00:00
ccremers
341bbfeb0c - Minor refactoring. 2006-08-08 14:50:28 +00:00
ccremers
ec3be3d55b - Implemented --claim=ns3,I switch to filter certain claims. 2006-08-08 12:30:29 +00:00
ccremers
5e10206df1 - Added encapsulated dot output and claim reporting to the XML output. 2006-08-01 07:31:40 +00:00
ccremers
9a98e66671 - Claim status is now reported after each claim. 2006-08-01 06:10:12 +00:00
ccremers
92a98a85cc - Single claim check branched. 2006-08-01 06:04:01 +00:00
ccremers
f31b5bfe9c - Started rewrite of main algorithm, by removing dynamic addition of M_0
nodes, and simply restricting it to a single M_0 send node.
2006-07-09 15:08:42 +00:00
ccremers
a8dee79504 - Added support for different attack heuristics. Disable with --prune=2. 2006-07-06 15:52:13 +00:00
ccremers
d2058d937b - Revised cost heuristic. Trace length is no longer the real
optimization.
2006-04-02 12:29:02 +00:00
ccremers
52708d09b4 - MakeTraceConcrete now yields nicer choices, e.g. "Agent1" or "Nonce2". 2006-04-02 11:56:22 +00:00
ccremers
8c03bba02a - Fixed a bug in output overwrite for de-class code. 2006-03-31 12:24:32 +00:00
ccremers
881eccd6be - Fixed --disable-intruder: it now also uses no tupling shortcuts. 2006-03-19 12:59:26 +00:00
ccremers
5624f7e7b6 - Added some comments. 2006-03-15 08:56:23 +00:00
ccremers
25244c5b23 - Fixed bug in new tuple expansion code (again, caused by the intricate
"realX" versus "isX" distinction.)
- Added structures for rho, sigma, constants, but did not activate them
  yet.
2006-03-15 08:51:08 +00:00
ccremers
16a59624fe - Revised dot output.
- Reintroduced intruder events.
  - Added colors.
2006-03-14 11:37:28 +00:00
ccremers
5487d3ae90 - From this version onwards, Scyther no longer supports the modelchecker
method. A big cleanup has been started, but is not finished yet, so
  minor artefacts might still remain. These are to be cleaned up later.
2006-03-08 13:58:46 +00:00
ccremers
1678577ce0 - Improved proof reports.
- Minor (epsilon type) efficiency improvement.
2006-03-05 15:18:39 +00:00
ccremers
f3d94b8e0d - Removed old hack lemmas by clean ones. 2006-02-28 15:01:58 +00:00
ccremers
00616e45ed - Bit masking was incorrect: & binds less strong than == !
This caused many of the --experimental switches not to work.
2006-02-28 13:41:36 +00:00
ccremers
cf832ca1b1 - Seems to work again, but further testing is needed. 2006-02-27 22:27:09 +00:00
ccremers
b49d13b6ee - [[[ Broken commit. ]]]
Stuff seems to be working again, slightly less efficient though (count
  states).
2006-02-27 16:08:17 +00:00
ccremers
c22173e5ee - [[[ Broken commit ]]]
More work on the arachne multiple-decryptor. Horrific.
2006-02-26 20:01:22 +00:00
ccremers
95df010a54 - [[[ Broken commit ]]]
More intermediate work.
2006-02-26 17:18:59 +00:00
ccremers
0ce88af6ac - [[[ Broken commit ]]]
Committing partial new Warshall work because it is getting too big.
2006-02-26 15:00:58 +00:00
ccremers
b16023bf0e - Cleaned up heuristic code. Note that there is a "hidden" heuristic:
implicitly, older goals are resolved first, if some goals have equal
  weights. This is encoded in the "w <=" comparison; if this is set to
  "w <", the heuristic becomes much less effective.
2006-02-23 15:03:43 +00:00
ccremers
921c82876d - experimental=4 now disables some things. Weirdly enough, they don't
seem to make much difference.
2006-02-22 09:53:50 +00:00
ccremers
b2e40e07f3 - Some more work on hidelevel backbone.
- Added '--count-states' switch for the Arachne engine.
2006-02-22 08:24:29 +00:00
ccremers
bb7259a1ad - Removed some too interesting pruning methods that really need theorems
first. Revealed by the certified e-mail protocol by Abadi and
  Blanchet.
2006-01-17 16:18:26 +00:00
ccremers
da75862d82 - Huge code documentation effort. 2006-01-02 21:06:08 +00:00
ccremers
6676266f4a - More refactoring to improve the code. 2006-01-02 20:18:47 +00:00
ccremers
e6505a72a3 - Further refactoring.
- Some cleanup.
2006-01-02 19:55:34 +00:00
ccremers
a5acc4984a - More refactoring for Arachne. Slowly we're getting somewhere. 2006-01-02 19:19:23 +00:00
ccremers
e592a0a432 - Refactoring code: splitting stuff out of arachne.c 2006-01-02 18:43:25 +00:00
ccremers
e21627442a - Added 'singular' directive for roles. Syntax:
protocol ns3 (I,R)
  {
    singular role I:
    {
    }
  }
2006-01-02 16:05:53 +00:00
ccremers
3b897c3872 - Added '--check' switch, to see whether your protocol terminates at all
if there is no intruder.
- Restructered many switches.
2005-12-29 12:52:51 +00:00
ccremers
a50245734d - Fixed the broken '--no-intruder' switch. 2005-12-29 12:14:21 +00:00
ccremers
ca4c5674ac - Added check for non-used variables. 2005-12-27 13:44:12 +00:00
ccremers
28774cb94c - Moved dot output (finally) into a separate file, and made some minor
improvements.
2005-12-27 11:50:46 +00:00
ccremers
c4628e8be6 - Added support for more intelligent bounding. Fairly untested at the
moment.
2005-12-27 11:19:45 +00:00
ccremers
c20810def5 - Added preliminary support for singular attack output. 2005-12-27 10:49:22 +00:00
ccremers
e82ce8b962 - Added --no-intruder switch, but it is currently broken. 2005-12-21 19:02:41 +00:00
ccremers
6543a8f659 - Added '--extravert' switch, which avoids initiator Alice to talk to
Alice.
2005-11-29 09:15:16 +00:00
ccremers
76666404b0 - Added '--concrete' switch to fill in to pick readable names for
variables.
2005-11-12 21:13:00 +00:00
ccremers
9f8f04c41c - Switched to the new consistency checking base. 2005-10-08 20:47:31 +00:00
ccremers
5b73d707a0 - Rewrite of actor/agent type consitency code: now more aware of
initiator/responder difference.
2005-09-09 10:05:29 +00:00
ccremers
e104dddbfb - Added a switch to number the limit of intruder actions.
Initial testing suggests it does not influence the number of states
  much for values of 2 and higher.
2005-08-21 21:38:32 +00:00
ccremers
1ee77472a0 - --max-attacks=AnyGijsNumber. 2005-08-15 12:49:32 +00:00
ccremers
cb315aafc8 - Added '--extend-trivial' switch. This is not a complete '--extend'
algorithm, as it is pretty dumb, but it works in most cases. Use with
  care.
2005-08-12 12:13:50 +00:00
ccremers
2cd9cf4148 - Added random goal picker. Untested. 2005-08-01 12:59:30 +00:00