Commit Graph

1604 Commits

Author SHA1 Message Date
ccremers
dfe16fa306 - First skeleton for tuple printer. 2004-10-14 18:18:01 +00:00
ccremers
d33ec486ce - Modified -l switch to also serve as proof depth limit. 2004-10-14 15:25:28 +00:00
ccremers
ba832159b1 - Added a new prioritylevel for seemingly public keys, but the splice-as
problem remains.
2004-10-14 15:09:48 +00:00
ccremers
29445bbd5f - Added two (SPORE) splice-AS variants. 2004-10-14 14:50:49 +00:00
ccremers
15ed7a99fa - Prevent stupid clashes. 2004-10-14 14:41:54 +00:00
ccremers
884db51a4b - Added (false) Nisynch, Niagree claims.
- Shortened the names.
2004-10-14 14:41:27 +00:00
ccremers
c717262e20 - Fixed the types. 2004-10-14 14:35:01 +00:00
ccremers
09ffaad340 - Fixed a claim role. 2004-10-14 14:34:47 +00:00
ccremers
9ac12f9198 - More serious problem found. 2004-10-14 14:33:22 +00:00
ccremers
123b12a1c0 - Problems with Splice/AS suggest heuristic improvements. 2004-10-14 14:30:27 +00:00
ccremers
dbb35a3ec9 - Added the splice-AS protocol. The modelchecker finds an attack, but
the arachne methods causes some problems.
2004-10-14 14:22:59 +00:00
ccremers
87a75106d1 - Printing the protocol tab-separated from the role is more useful for
script-based parsing.
2004-10-14 13:29:28 +00:00
ccremers
2bc1df6135 - Improved readability of printed claims.
- Fixed comment.
2004-10-14 13:19:36 +00:00
ccremers
0efd39e028 - This script now only outputs summary to stdout. 2004-10-14 11:52:13 +00:00
ccremers
c7b06fc0f1 - Added Nisynch claims. 2004-10-14 11:51:49 +00:00
ccremers
6eecef9806 - I can't remember why I needed this protocol, but here goes. 2004-10-13 13:29:38 +00:00
ccremers
1effb2ca99 - Added original Kao-Chow protocol. There is something strange with the
Arachne method though, that needs investigating.
2004-10-13 12:55:23 +00:00
ccremers
46e46abb84 - Added andrew-ban and made the naming more consistent. 2004-10-13 12:25:01 +00:00
ccremers
0df4662a4a - Fixed claim labelling. 2004-10-13 12:24:34 +00:00
ccremers
decf9f36c2 - Added test script. 2004-10-13 12:24:18 +00:00
ccremers
1387fd1d50 - Fixed claim labelling. 2004-10-13 12:23:55 +00:00
ccremers
0db90f4243 - Fixed some agent issue. 2004-10-13 12:23:35 +00:00
ccremers
d7bcd18fb0 - Fixed a claim label. 2004-10-13 12:23:05 +00:00
ccremers
40584ba6bd - Noted some stuff about graph computations, so that I won't forget
this.
2004-10-12 18:08:01 +00:00
ccremers
487212a9f9 - The TMN protocol was wrongly reporting an error in the protocol. This
turned out to be caused by an over-protective first-read detection.
2004-10-12 16:58:29 +00:00
ccremers
d64badefdc - Found a problem with type flaw attacks. 2004-10-12 15:23:03 +00:00
ccremers
0de3320009 - Fixed a memory leak in termLocal. This did not cause any problems for
the modelchecker, as it calls it only once, but it caused major
  problems for the arachne engine, which creates and destroys semiruns
  all the time.
2004-10-12 15:12:20 +00:00
ccremers
ef34e0080e - Counterexample for Bart's logic. 2004-10-06 09:10:04 +00:00
ccremers
3b4b367a4a - Minor correction. Probably redundant for a good compiler ;) 2004-09-20 17:41:53 +00:00
ccremers
02e99761ae - Split roleInstance into two more managable parts. 2004-09-20 12:40:01 +00:00
ccremers
500710519e - Added protocols for Bertinoro VODCA talk. 2004-09-10 07:46:00 +00:00
ccremers
f771d3ef4c - Testing to see what the gains are of using one regular agent. Turns
out to be half of the states, thus twice as fast.
2004-09-07 10:20:20 +00:00
ccremers
be366afa0e - A good reduction idea for secrecy added to the todo list. 2004-09-07 09:56:06 +00:00
ccremers
c293c3bac8 - Added a new counter ref version. 2004-09-02 13:50:45 +00:00
ccremers
947fe654f1 - Testing with this protocol didn't yet reveal the desired behaviour, as
Arachne -m2 strategies aren't working fully yet.
2004-09-01 20:24:39 +00:00
ccremers
8570465e48 - More todo. 2004-09-01 19:11:06 +00:00
ccremers
78e68f3c17 - Added claim label. 2004-08-31 14:35:47 +00:00
ccremers
5ed9fefa7e - Improved these scenarios. 2004-08-31 14:32:31 +00:00
ccremers
8b48aade68 - Huge effort to make match type 2 (typeflaw generic) matching work.
Problem with goals that turn into tuples, will have to be solved.
2004-08-31 14:31:06 +00:00
ccremers
0e9b7dcf11 - Some added error/bounds detection all around. 2004-08-31 12:35:05 +00:00
ccremers
a673ea4ad1 - Write down, so that we don't forget. 2004-08-31 08:58:50 +00:00
ccremers
3687bff185 - Fixed kaochow - Niek Palm version. 2004-08-30 22:12:18 +00:00
ccremers
f5ab30995c - Removed the debugging output. 2004-08-30 22:09:44 +00:00
ccremers
5c90522c55 - Fixed a bug in the pruning algorithm, where intruder runs were also
checked for agent lists, which is false.
2004-08-30 22:08:44 +00:00
ccremers
b04bc86185 - Some minor cleanups. 2004-08-30 21:49:51 +00:00
ccremers
4832e9116c - Added pruning theorem for untrusted actors. 2004-08-30 21:07:45 +00:00
ccremers
d43e3d432f - Ignoring singular variables seems to be a smart choice, although it
implies that the intruder can generate any type. That is not conform
  the usual semantics. So we either change the usual semantics (wise) or
  we make this choice optional.
2004-08-30 20:48:11 +00:00
ccremers
8f441ac913 - Fixed some minor issues.
- Fixed type flaw in labellist type.
2004-08-30 20:08:11 +00:00
ccremers
20a38f79c5 BROKEN
- Protocol is not done yet.
2004-08-30 14:40:12 +00:00
ccremers
44f394d098 - Improvement. 2004-08-30 14:39:52 +00:00