andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,445 Commits 1 Branch 0 Tags 21 MiB
ab324fcea8
Commit Graph

100 Commits

Author SHA1 Message Date
Cas Cremers
ab324fcea8 Added syntax check for usage of agreement. 2012-04-25 15:30:15 +02:00
Cas Cremers
2242a5fcbd Fixing read->recv conventions. 2012-04-25 09:53:07 +02:00
Cas Cremers
1cbe9826ac Updated dates. 2012-04-24 13:56:51 +02:00
Cas Cremers
4ec5ea4232 Added helper protocol support. 
This is not a full copy from the compromise branch. In particular,
some counts (in arachne.c) are missing, as well as the modified dot output (dotout.c).
 2011-04-01 15:23:20 +02:00
Cas Cremers
a03f06ea41 BUGFIX: Auto-claim naming scheme was context dependent. 
The automatic mechanism to assign labels to claims was dependent on the
context. In practice, a claim could get a different label when analyzed in
isolation compared to when analyzed in parallel with some other protocols. This
caused problems for the multi-protocol analysis.
 2011-01-27 14:12:51 +01:00
Cas Cremers
1814a2d7b3 BUGFIX: Removed obsolete code that was destroying commit/agreement functionality when filtering. 
This is now (and has been for a while) handled by other code.
 2011-01-25 17:30:59 +01:00
Cas Cremers
c25f6efd6a SPDL: Introduced 'hashfunction f;' construct to input language. 2010-11-11 00:01:31 +01:00
Cas Cremers
6d9d89eca2 Introduced 'fresh' for fresh value generation and added deprecation warning for 'const' usage. 2010-11-10 10:37:57 +01:00
Cas Cremers
3e3c2d7b07 Rewrote some code for humans to read, i.e. strcmp wrapper. 2008-08-21 16:59:05 +02:00
Cas Cremers
c729d13a00 Reindent of the code revealed that some was not indented nicely yet. Silly. 2008-03-23 15:56:09 +09:00
Cas Cremers
0709539737 Merge branch 'master' of ssh://cremersc@buckleburg.inf.ethz.ch/home/cremersc/repos/scyther 2008-01-28 15:25:46 +01:00
Cas Cremers
a7c1d8c696 Improved handling of cases with untyped variables. 
When untyped variables occur, the encryption level depth pruning is for
now unjustified. Maybe we can get a proof later.  Previously this was
hidden, which was a bad design decision.  Now the output is much
clearer.
 2008-01-28 15:23:40 +01:00
Cas Cremers
ce9891d351 Disabled well-formedness temporarily. 
Simon Meier found some problems with the draft implementation, so it is disabled
for now.
 2008-01-10 16:09:24 +01:00
Cas Cremers
7d584cca1e Added GPL 2 License to the C sources. 
A first step towards releasing Scyther completely to the public.
 2007-06-11 14:01:04 +02:00
Cas Cremers
1542d65def - Big catchup commit to make sure we are up to beta7. 
This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features.
 2007-05-18 14:06:29 +02:00
ccremers
9882651f4a - Fixed role comparison bug. 2007-02-01 12:18:38 +00:00
ccremers
41d811a49a - Improved error output with line number syntax. 2007-01-29 17:20:45 +00:00
ccremers
df62d65d5c - Fixes to error output 2007-01-29 15:17:11 +00:00
ccremers
cf84e83f9f - Scanned protocols for new obligatory check. 2007-01-29 15:05:15 +00:00
ccremers
9ca722e3cc - Added automatic checking of label correspondence. This will break [BREAK ALERT] some protocol files, e.g. those with weird roles. Fix them by prefixing the bang 'make' for ignoring labels. 2007-01-29 13:15:35 +00:00
ccremers
eaa6ef1345 - Added feature for multi-party protocols (weaker precondition on Reachable) 2007-01-16 17:22:51 +00:00
ccremers
0fddd9f566 - Some fixes after pedantic tests. What remains: (a) C++ style comments (//) and (b) nested functions. 2007-01-06 18:01:36 +00:00
ccremers
89c3a20acf - Many cleanups to make -Wall happy. Next up is pedantic... 2007-01-06 14:45:29 +00:00
ccremers
e2aca6f3ce - Better filter. 2006-08-08 13:00:16 +00:00
ccremers
36ccfd776a - Even less warnings. 2006-08-08 12:40:04 +00:00
ccremers
d9a37b62b3 - Some warnings are only interesting when checking. 2006-08-08 12:35:43 +00:00
ccremers
29f0756f0a - Generating a label should not cause a warning. 2006-08-08 12:34:11 +00:00
ccremers
ec3be3d55b - Implemented --claim=ns3,I switch to filter certain claims. 2006-08-08 12:30:29 +00:00
ccremers
2ef343ba6e - Order of claim processing now corresponds to the order in which they 
occur in the file.
 2006-08-07 09:56:55 +00:00
ccremers
180d00ff41 - Fully removed substitutions.h artefacts. 2006-08-02 09:50:21 +00:00
ccremers
cc358c5df3 - Misc fixes, some reporting with --check. 2006-07-31 11:30:08 +00:00
ccremers
e902aaa260 - Added well-formedness checks. This will only be enabled if a role uses 
the 'knows' keyword.
 2006-07-31 11:08:51 +00:00
ccremers
df1a56c780 - Iteration seems to work nicely, thank you. 2006-07-27 11:55:24 +00:00
ccremers
4e085f0eb8 - Initial knowledge displayed when running --check. 2006-07-27 10:45:26 +00:00
ccremers
f00392ac3e - Added functional 'knows' keyword. 2006-07-27 10:44:12 +00:00
ccremers
2b9246bb64 - Bug report: this should be fixed. 2006-03-15 08:33:09 +00:00
ccremers
16a59624fe - Revised dot output. 
- Reintroduced intruder events.
  - Added colors.
 2006-03-14 11:37:28 +00:00
ccremers
5487d3ae90 - From this version onwards, Scyther no longer supports the modelchecker 
method. A big cleanup has been started, but is not finished yet, so
  minor artefacts might still remain. These are to be cleaned up later.
 2006-03-08 13:58:46 +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
0ce88af6ac - [[[ Broken commit ]]] 
Committing partial new Warshall work because it is getting too big.
 2006-02-26 15:00:58 +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
5d2d836d07 - Much work for the skeleton of the Hidelevel lemma. 2006-02-21 20:29:05 +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
724faa8949 - Cleaned up some printf's and warnings in compiler.c 
- Added warning for unspecified roles.
 2006-01-02 15:29:41 +00:00
ccremers
bceaca28f0 - Improved some type of warnings for e.g. empty prec sets andsoforth. 2005-12-28 14:25:06 +00:00
ccremers
39adf85c6a - Reverted previous version: Tickets can possibly be secret as well 
(although this is dubious, as the claiming role will not know the
  contents in many cases)
 2005-12-28 12:04:00 +00:00
ccremers
dce2befd50 - Don't add secrecy claims for ticket types. 2005-12-28 11:59:39 +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
ccc4c34823 - Added '--remove-claims' switch to cut off all existing claims. 2005-12-27 13:53:49 +00:00