ccremers
91b52f6b4a
- Removed more dead code, improved scantags.py
2007-01-27 11:07:45 +00:00
ccremers
8d66dc48fd
- Fixed intruder generated value displays.
2006-12-05 10:10:17 +00:00
ccremers
1ce03104c5
Major:
...
- Added rho/sigma/constants fields to the runs, on which the new code is
based. Over time, .locals should be deprecated in favour of these
better variants.
- Untyped variant is out of grace for the time being (cf. Athena interm
problems)
- Improved graph output further.
Minor:
- Added TERMLISTADD and APPEND macros for more concise code.
2006-03-15 21:30:19 +00:00
ccremers
2280187b32
- Improved dot class output.
2006-03-08 15:12:58 +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
5d2d836d07
- Much work for the skeleton of the Hidelevel lemma.
2006-02-21 20:29:05 +00:00
ccremers
da75862d82
- Huge code documentation effort.
2006-01-02 21:06:08 +00:00
ccremers
e6505a72a3
- Further refactoring.
...
- Some cleanup.
2006-01-02 19:55:34 +00:00
ccremers
0505aaacd6
- New claim: CLAIM_Reachable
...
- Added new switches:
-G,--generate-statespace
-C,--generate-claims
- Claims are now allowed to have no label (they will be generated
automatically)
- Output summary shows parameter of claims
- Internally, new symbols can now be generated by
symbolNextFree(prefixsymbol)
2005-12-28 11:50:17 +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
8b51593cf5
- Each attack now includes
...
* Initial knowledge
* Role definitions for protocols involved
2005-05-12 14:52:50 +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
ccremers
54ccd5179e
- Added a new selector that picks goals that are local variables.
2004-12-29 16:05:32 +00:00
ccremers
a38925c9c2
- Added some useful macros to term.h to address subparts (e.g.
...
TermOp1(t)). Renamed all uses.
2004-11-16 12:06:36 +00:00
ccremers
b6af2f9dac
- First try for diff function.
2004-11-01 14:06:26 +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
d58fc5ab43
- Made the label naming unique, by adding tuple info with the protocol
...
name. Now, we can simply test multiple protocol names by
concatenation.
- Removed the pointer equality leaf hypothesis, as it didn't hold
anymore.
2004-08-27 10:08:03 +00:00
ccremers
0fc008fe33
- Added keylevels to symbols. This is to help pruning the proofs, for
...
terms and patterns that do not originate on regular nodes.
2004-08-20 19:16:56 +00:00
ccremers
f25f0abd4e
- Fixed a memory error.
2004-08-19 14:49:03 +00:00
ccremers
b2d21f0a8a
BROKEN
...
- Working on new algorithm. Some memory error can occur.
2004-08-18 14:06:14 +00:00
ccremers
c5695d6fe8
- Added more generic term iterators.
2004-08-18 12:12:29 +00:00
ccremers
bb78c71c90
- Introduced termInTerm (bigterm, smallterm)
2004-08-17 14:11:25 +00:00
ccremers
74851e0393
- Consistency improvements.
2004-08-14 14:27:46 +00:00
ccremers
f219461c8d
- After some trouble, nonce binding is working nicely.
2004-08-14 14:23:21 +00:00
ccremers
0f470cf6a2
- Rewrote roleInstance to cope with Arachne needs.
...
- Introduced some iterators for e.g. term leaves and roledefs. These are
not used everywhere yet.
2004-08-12 09:14:31 +00:00
ccremers
71c658051e
- Reindented everything, so the layout is up to date again.
2004-08-09 10:05:58 +00:00
ccremers
b22667a791
- Fixed termlist printing.
2004-07-29 11:15:07 +00:00
ccremers
60b02eea0e
- Renamed nearly all files. Now, we try to use singular terms.
...
Exception: states.h is the plural form.
2004-07-24 19:07:29 +00:00