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

14 Commits

Author SHA1 Message Date
Cas Cremers
1bbd2f1ab7 Introduced markers in proof output for consistency with book description. 2012-10-02 13:43:30 +02:00
Cas Cremers
1cbe9826ac Updated dates. 2012-04-24 13:56:51 +02:00
Cas Cremers
66e18deb3f NEW: Added claims: Commit and Running. 
There are two new claims:

  claim(X,Commit,t)  : check for agreement on data
  claim(X,Running,t) : signaling claim

The property checked is that each claim Commit needs to be preceded by a Running
with an identical term t.

Cherry-picked from commit 99a6be00e9d3d219ec73665607e8a3a7d65d04d1
 2011-01-04 15:50:25 +01:00
Cas Cremers
2fb0ecde97 NEW: Added Aliveness and Weak Agreement claims. 2011-01-04 15:50:25 +01:00
Cas Cremers
6afcfe1d10 NEW: Added SID & SKR dummy claims. 
This allows for input file reuse among branches (i.e. compromise).
 2011-01-04 15:50:25 +01:00
Cas Cremers
4ac74f321f SPDL: Introduced preconstructed PKI with pk/sk/k. 
Introduced K(A1...AN) constant function for symmetric pre-shared keys.
Added inverses (pk,sk) as default constructs.
 2010-11-11 00:01:31 +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
89c3a20acf - Many cleanups to make -Wall happy. Next up is pedantic... 2007-01-06 14:45:29 +00:00
ccremers
bb7259a1ad - Removed some too interesting pruning methods that really need theorems 
first. Revealed by the certified e-mail protocol by Abadi and
  Blanchet.
 2006-01-17 16:18:26 +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
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
b6e9841c0f - Moved special terms into their own (very) special file. 2005-06-16 14:10:07 +00:00