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
ccremers
164e325659
- New attack attribute.
2005-07-01 13:25:54 +00:00
ccremers
b6e9841c0f
- Moved special terms into their own (very) special file.
2005-06-16 14:10:07 +00:00
ccremers
db18b203a9
- Added "Empty" claim type, which is ignored.
...
Syntax example: claim_x(I, Empty);
2005-06-16 11:59:44 +00:00
ccremers
1bdaf7b5d9
- Large rewrite of switch code. Instead of having switch parameters in
...
the (monstrously large) system structure, there is now a global
'switchdata' structure originating in switches.c. This makes it much
easier to see what's happening.
* Note: although this code has been tested, there might be some
hiccups, because doing multiple search&replace actions over all
files is bound to cause some problems.
2005-06-07 15:02:27 +00:00
ccremers
1331f5e7a3
- Added a global attack id, starting at one. Currently only shown in
...
XML and Dot output. For Dot, it is included in the label. For XML, it
is an added attribute of the 'attack' tag.
2005-06-07 13:40:56 +00:00
ccremers
4a42604cb6
- Added Ticket basic term type. Note that this only has consequences for
...
the Arachne type checking. The net result is that a variable of type
'Ticket' can always contain any term, even with -m0 or -m1 matching.
2005-06-02 12:14:28 +00:00
ccremers
0540b744e2
- Repaired a pruning method that still needed a lemma. It was a bit
...
overzealous and killed a woolam-mutual attack.
2005-05-19 14:43:32 +00:00
ccremers
f22ce0dcb9
- Big change in the Arachne algorithm: decryptor sequences now get
...
expanded explicitly. This solves a long-standing issue with {k}k
decryption to yield k. Needs some testing to ensure that it did not
introduce any new errors.
2005-05-17 18:45:01 +00:00
ccremers
71558706a6
- XML output should be workable now.
2005-05-02 13:38:45 +00:00
ccremers
924abc065d
- Added xml output switch (-x, check scyther --help). It's not complete
...
yet, to be finished tomorrow.
2005-05-01 13:32:50 +00:00
ccremers
8e1041b567
- Minor output fixes.
2005-04-21 12:04:45 +00:00
ccremers
9271cc7624
- Matching method propagation was wrong in new switch code.
...
- Some fixes for protocols that do not include matching send/read
combo's. In particular, the max encryption level method ranged over
the sends; now over all events. Maybe it can range over read events
only?
2005-04-18 05:51:25 +00:00
ccremers
88e2f3d26c
- Added a better reverse-engineered variation of the Athena goal
...
selector.
- Added an idea that might make searches somewhat faster.
2005-03-11 20:41:59 +00:00
ccremers
c8df32c7a2
- Minor improvements.
...
* Old bindings detections (immediately binds them to older binding)
* Know_only derivation for keylevel lemmas.
2005-03-08 13:02:16 +00:00
ccremers
291353a14f
- Improved version of the latex renderer of arachne attacks. Still not
...
usable, however.
2005-03-07 19:02:08 +00:00
ccremers
197117f2fe
- Made a start with the arachne latex output. It's a mess currently.
2005-03-07 15:38:01 +00:00
ccremers
5c90a5af29
- Improved the .dot output format quite a bit.
2005-02-21 15:12:59 +00:00
ccremers
820c2caed8
- Revisited type matching conditions.
...
- Introduced tuple unfolding stuff for Arachne. -m2 should work now.
2005-01-14 18:18:40 +00:00