58f3aafc65- Much improved.
ccremers
2005-11-16 18:19:50 +0000
5c065a7bba- Started generator.
ccremers
2005-11-16 16:49:47 +0000
9e5a076d7d- Added test file. - Created main file.
ccremers
2005-11-16 16:44:56 +0000
2fe91a2eb1- Made a start with if2spdl parser.
ccremers
2005-11-16 16:24:18 +0000
e51b54af23- FIX: Instantiation of variables is now the default. - NEW: -C --class switch to reset this. - NEW: max runs is now 6 by default for usability. For unbounded search, use -r 0 or --maxruns=0
ccremers
2005-11-12 21:26:50 +0000
41132afea3- Finally fixed the 'IV', 'RV' nuissance for global variables such as the role names.
ccremers
2005-11-12 21:16:02 +0000
76666404b0- Added '--concrete' switch to fill in to pick readable names for variables.
ccremers
2005-11-12 21:13:00 +0000
1527773ae2- Added Boyd's NSL fix, which is broken.
ccremers
2005-11-09 11:51:38 +0000
c1c0b856deCHG: Changed default behaviour to Arachne engine. NEW: Added 'S' switch for --summary things.
ccremers
2005-11-04 13:23:30 +0000
5e1ca56f87- Added experimental feature: explicit unique origination. This has to be investigated further, because it seems to reduce just a few states. Note to Gijs: stay away from this, you should be writing your thesis.
ccremers
2005-10-08 20:57:39 +0000
9f8f04c41c- Switched to the new consistency checking base.
ccremers
2005-10-08 20:47:31 +0000
2ead7ab2ff- Improved code for new preferred order swapping of substitutions. Also included more comments.
ccremers
2005-10-08 20:22:24 +0000
2452a34671- Added 'termlistMinusTermlist' function. - Added TERMLISTERROR constant, and corresponding tests. Note that this will not work in many contexts, because only NULL is usually considered to be a special value. It is purely intended for the new type evaluation functions in type.c.
ccremers
2005-10-08 19:56:04 +0000
a3b009f119- The state of sys->variables was not maintained correctly, because terms were destroyed before it could be tested whether they were in sys->variables. Thus, garbage was left in sys->variables. This has gone undetected because it was never really used. Hmpf.
ccremers
2005-10-08 19:53:10 +0000
ea5bc6893f- Slightly smarter substitution in the symmetric case, when we make Var1 equivalent to Var2.
ccremers
2005-10-07 20:38:41 +0000
8d9891fee0- Added some todo stuff.
ccremers
2005-10-03 08:19:58 +0000
cb0f72a23d- Use I and R as role names instead of A and B in ksl
gijs
2005-09-19 10:13:17 +0000
5b73d707a0- Rewrite of actor/agent type consitency code: now more aware of initiator/responder difference.
ccremers
2005-09-09 10:05:29 +0000
5c0c5d3333- Better XML output for variables section.
ccremers
2005-09-08 13:30:00 +0000
01a45f87d2- Rewrote variables section, integrated typeflaw info. Note that for variables that are not instantiated, only the variable and the type info is shown. For instantiated variables, both are shown. In this output the attribute 'free' should be ignored, as its output is not accurate here.
ccremers
2005-09-08 12:55:32 +0000
48574de13e- Minor improvement to type flaw output: now also shows the type of the substituted term.
ccremers
2005-09-07 07:21:13 +0000
053a76e5fb- oops forgot to update 1 message, we really need some option to check input files for correctness (i.e. will it finish without an intruder)
gijs
2005-08-31 13:17:54 +0000
a4c9303781- Fix a modelling error in wmf-lowe
gijs
2005-08-31 13:08:10 +0000
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.
ccremers
2005-08-21 21:38:32 +0000
c330a5b719- Added some thoughts.
ccremers
2005-08-21 21:36:00 +0000
fb2c0f1d7a- Whoops, too readable (i.e. wrong)
ccremers
2005-08-19 15:25:35 +0000
0a9c0fbfac- Implemented a much beter naming convention for the roles, which should make hand proofs much easier.
ccremers
2005-08-18 14:00:51 +0000
95d33810ce- Added some heuristics testing.
ccremers
2005-08-15 14:01:01 +0000
0f54f2ed23- Update modeling of needham schroeder to better reflect the modelling in SPORE: - pk is not known to all agents, only pk(Simon) is known - Use new naming convention: - Protocol name starting with an @ means internal protocol - For non internal protocols naming is as follows: protocolname-variant^subprotocol For example: yahalom-Lowe^KeyCompromise meaning the key compromise sub protocol of the Lowe variant of the Yahalom protocol.
gijs
2005-08-15 13:31:48 +0000
998e4852ba- Allow ^ and - in identifies which will be used in protocol names in future naming conventions
gijs
2005-08-15 11:27:46 +0000
7e246cf4f3- Added some agreement/synchronisation claims.
ccremers
2005-08-12 13:56:37 +0000
6f900f1d47- More narrowing down.
ccremers
2005-08-12 13:52:38 +0000
5a027cc00a- Forgot to update wmf to the ExpiredTimeStamp
gijs
2005-08-12 13:24:00 +0000
2e9e43742e- Added more fine-grained control for the associativity of tupling: --tupling=n * 0: right-associative; 1: left-associative; others are reserved for future use. --ra-tupling * Sets the default, but is there for symmetry.
ccremers
2005-08-12 12:59:25 +0000
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.
ccremers
2005-08-12 12:13:50 +0000
44bc36edc5- Add @ to swapkey, to disable it in classification - Modify key Compromise for protocols that contain a timestamp to make the key compromise disclose a timestamp with a different type, namely ExpiredTimeStamp so that they will not be accepted as timestamps in a new session, thereby simulating that they are expired.
gijs
2005-08-12 11:55:24 +0000
56f7cf5df2- Added switch '--la-tupling' to enforce left-associative tupling instead of the default right-associative tupling. Note that this only matters for full typeflaw matching. - Adapted multi-nsl test script to test for both association variants.
ccremers
2005-08-12 07:28:44 +0000
cee11bc0af- Extra checks: * For incomplete protocols, better handling of dangling labels. * For termSubTerm better handling of NULL cases.
ccremers
2005-08-11 12:56:36 +0000
c8d2222c58- Allow identifiers to start with @ so that internal protocols such as key compromise and swapkey can be prefixed with @ to indicate that they should be ignored by the classification tool.
gijs
2005-08-11 12:24:36 +0000
2cd9cf4148- Added random goal picker. Untested.
ccremers
2005-08-01 12:59:30 +0000
eb948b8009- Fix a small modelling error in wmf-lowe
gijs
2005-07-07 14:03:48 +0000
f7f2bf27bb- Added type flaw information (just after the variables section) In pseudo-xml: <typeflaws><run id="1"><typeflaw><term variable /><termlist type(s) /><term value of variable /></typeflaw></run></typeflaws>
ccremers
2005-07-06 14:33:05 +0000
b7f82212c0- Some improvements.
ccremers
2005-07-05 09:54:00 +0000
53e7a7c55d- Fixed a modelling error in the key compromise part of WMF-Lowe - Included agent names in WMF-Lowe messages
gijs
2005-07-04 13:40:09 +0000
92356a2d43- Add names to WMF messages so that the system property described in SPORE (agents will not accepted messages they have created them selves) can be modelled.
gijs
2005-07-04 13:29:49 +0000
12b5d96ddb- Added script to test all variants of something.
ccremers
2005-07-04 11:52:36 +0000
cf52f34dab- Working version.
ccremers
2005-07-04 11:12:27 +0000
a1fdbe119f- Incorporated untrusted agents list (<untrusted> element in attack, containing a <termlist>) - <commandline><arg>./scyther</arg> <arg>-x</arg>... is now available.
ccremers
2005-07-01 13:46:18 +0000
6a3e57913c- Quick addition of Gijs' suggestions.
ccremers
2005-07-01 13:27:38 +0000
164e325659- New attack attribute.
ccremers
2005-07-01 13:25:54 +0000
0cf19b98a3- Added the BuNaVa protocol 1.
ccremers
2005-07-01 08:59:05 +0000
49cd9b1271- Use variable type SessionKey every where instead of a combination between Key and SessionKey - Make KSL working again
gijs
2005-06-29 12:42:25 +0000
eef9072324- Started to work on multiparty protocol generator.
ccremers
2005-06-28 13:41:55 +0000
c2b3f6492f- Remove some small modelling errors - New way to model Neumann Stub (it should be 2 distinct protocols)
gijs
2005-06-27 11:50:24 +0000
6fb6aa33dd- Add session compromise to all protocols that establish a session key
gijs
2005-06-24 10:53:15 +0000
658f4f392a- Add Compromised claim to test my new definition of freshness in combination with key compromise (appears to be working pretty well)
gijs
2005-06-23 12:49:34 +0000
4c224dc6f4- Add freshness claims to the protocols that should guarantee freshness
gijs
2005-06-23 12:45:32 +0000
464920907b- Added '--extend-nonreads' switch. It is totally untested, and I hope Gijs will have a look at it and tell me whether it actually works.
ccremers
2005-06-21 11:04:34 +0000
b6e9841c0f- Moved special terms into their own (very) special file.
ccremers
2005-06-16 14:10:07 +0000
db18b203a9- Added "Empty" claim type, which is ignored. Syntax example: claim_x(I, Empty);
ccremers
2005-06-16 11:59:44 +0000
f8a91d744dLittle tweak to the key compromise modelling, model key compromise agent as a responder instead of an initiator, remove empty roles from key compromise protocol.
gijs
2005-06-15 09:17:15 +0000
ba47af0c42- Test out a possible way to model key compromise: Add a role that sends out all messages that would occur in a legit run of the protocol including the session key (simulating a previously recorded run with its compromised session key)
gijs
2005-06-14 13:51:51 +0000
b212e0b1ec- Add a dummy role in andrew-ban-concrete to work around the key symmetry issue (k(I,R) != k(R,I)) - Fix a typo in splice-as-cj
gijs
2005-06-14 12:24:42 +0000
013afc99aa- Fixed a newly introduced bug. When the decryptor sequence unfolding code was added (two weeks ago), bindings were changed without changing the state of the graph closure buffer. This resulted in possible missed loops: thus, reports of broken claims could be found in the output, in inconsistent states. (Reported bij Gijs Hollestelle.) Note that this only influences the current development release, and not any previous results.
ccremers
2005-06-08 13:51:40 +0000
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.
ccremers
2005-06-07 15:02:27 +0000
eb36abee75- Indent any changed .c / .h files. Intended to be used just before a commit.
ccremers
2005-06-07 14:56:17 +0000
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.
ccremers
2005-06-07 13:40:56 +0000
22a0d2adfb- Some cleanup.
ccremers
2005-06-02 12:42:10 +0000
56c032f4a5Update SPORE protocols to use new ticket mechanism:
gijs
2005-06-02 12:41:24 +0000
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.
ccremers
2005-06-02 12:14:28 +0000
cd2ef14e4e- [Syntactical changes only] Fixed the indentation of some files.
ccremers
2005-06-02 09:40:05 +0000
01124e2104- Modified a number of things related to the attack analysis tools. * removed <term> wrappers * added <const> wrappers * removed <role><term> construct, now <rolename>R</rolename> constructs. * added <variables> section. * variable substitutions are followed through in runs. Thus, only unbound variables occur in the semitrace. * added the untested claims back in, so that all events in a role/semitrace are now shown. Note that they can be disabled again by using the new '-H' switch.
ccremers
2005-06-02 08:25:45 +0000
f8bafdcd60- Fixed type flaw problem.
ccremers
2005-05-24 14:31:55 +0000
ccremers
gijs