58f3aafc65
- Much improved.
ccremers
2005-11-16 18:19:50 +00:00
5c065a7bba
- Started generator.
ccremers
2005-11-16 16:49:47 +00:00
9e5a076d7d
- Added test file. - Created main file.
ccremers
2005-11-16 16:44:56 +00:00
2fe91a2eb1
- Made a start with if2spdl parser.
ccremers
2005-11-16 16:24:18 +00:00
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 +00:00
41132afea3
- Finally fixed the 'IV', 'RV' nuissance for global variables such as the role names.
ccremers
2005-11-12 21:16:02 +00:00
76666404b0
- Added '--concrete' switch to fill in to pick readable names for variables.
ccremers
2005-11-12 21:13:00 +00:00
1527773ae2
- Added Boyd's NSL fix, which is broken.
ccremers
2005-11-09 11:51:38 +00:00
c1c0b856de
CHG: Changed default behaviour to Arachne engine. NEW: Added 'S' switch for --summary things.
ccremers
2005-11-04 13:23:30 +00:00
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 +00:00
9f8f04c41c
- Switched to the new consistency checking base.
ccremers
2005-10-08 20:47:31 +00:00
2ead7ab2ff
- Improved code for new preferred order swapping of substitutions. Also included more comments.
ccremers
2005-10-08 20:22:24 +00:00
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 +00:00
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 +00:00
ea5bc6893f
- Slightly smarter substitution in the symmetric case, when we make Var1 equivalent to Var2.
ccremers
2005-10-07 20:38:41 +00:00
8d9891fee0
- Added some todo stuff.
ccremers
2005-10-03 08:19:58 +00:00
cb0f72a23d
- Use I and R as role names instead of A and B in ksl
gijs
2005-09-19 10:13:17 +00:00
5b73d707a0
- Rewrite of actor/agent type consitency code: now more aware of initiator/responder difference.
ccremers
2005-09-09 10:05:29 +00:00
5c0c5d3333
- Better XML output for variables section.
ccremers
2005-09-08 13:30:00 +00:00
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 +00:00
48574de13e
- Minor improvement to type flaw output: now also shows the type of the substituted term.
ccremers
2005-09-07 07:21:13 +00:00
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 +00:00
a4c9303781
- Fix a modelling error in wmf-lowe
gijs
2005-08-31 13:08:10 +00:00
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 +00:00
c330a5b719
- Added some thoughts.
ccremers
2005-08-21 21:36:00 +00:00
0a9c0fbfac
- Implemented a much beter naming convention for the roles, which should make hand proofs much easier.
ccremers
2005-08-18 14:00:51 +00:00
95d33810ce
- Added some heuristics testing.
ccremers
2005-08-15 14:01:01 +00:00
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 +00:00
998e4852ba
- Allow ^ and - in identifies which will be used in protocol names in future naming conventions
gijs
2005-08-15 11:27:46 +00:00
7e246cf4f3
- Added some agreement/synchronisation claims.
ccremers
2005-08-12 13:56:37 +00:00
6f900f1d47
- More narrowing down.
ccremers
2005-08-12 13:52:38 +00:00
5a027cc00a
- Forgot to update wmf to the ExpiredTimeStamp
gijs
2005-08-12 13:24:00 +00:00
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 +00:00
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 +00:00
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 +00:00
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 +00:00
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 +00:00
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 +00:00
eb948b8009
- Fix a small modelling error in wmf-lowe
gijs
2005-07-07 14:03:48 +00:00
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 +00:00
b7f82212c0
- Some improvements.
ccremers
2005-07-05 09:54:00 +00:00
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 +00:00
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 +00:00
12b5d96ddb
- Added script to test all variants of something.
ccremers
2005-07-04 11:52:36 +00:00
cf52f34dab
- Working version.
ccremers
2005-07-04 11:12:27 +00:00
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 +00:00
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 +00:00
eef9072324
- Started to work on multiparty protocol generator.
ccremers
2005-06-28 13:41:55 +00:00
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 +00:00
6fb6aa33dd
- Add session compromise to all protocols that establish a session key
gijs
2005-06-24 10:53:15 +00:00
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 +00:00
4c224dc6f4
- Add freshness claims to the protocols that should guarantee freshness
gijs
2005-06-23 12:45:32 +00:00
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 +00:00
b6e9841c0f
- Moved special terms into their own (very) special file.
ccremers
2005-06-16 14:10:07 +00:00
db18b203a9
- Added "Empty" claim type, which is ignored. Syntax example: claim_x(I, Empty);
ccremers
2005-06-16 11:59:44 +00:00
f8a91d744d
Little 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 +00:00
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 +00:00
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 +00:00
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 +00:00
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 +00:00
eb36abee75
- Indent any changed .c / .h files. Intended to be used just before a commit.
ccremers
2005-06-07 14:56:17 +00:00
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 +00:00
22a0d2adfb
- Some cleanup.
ccremers
2005-06-02 12:42:10 +00:00
56c032f4a5
Update SPORE protocols to use new ticket mechanism:
gijs
2005-06-02 12:41:24 +00:00
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 +00:00
cd2ef14e4e
- [Syntactical changes only] Fixed the indentation of some files.
ccremers
2005-06-02 09:40:05 +00:00
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 +00:00
f8bafdcd60
- Fixed type flaw problem.
ccremers
2005-05-24 14:31:55 +00:00
ccremers
gijs