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

760 Commits

Author SHA1 Message Date
Cas Cremers
c25f6efd6a SPDL: Introduced 'hashfunction f;' construct to input language. 2010-11-11 00:01:31 +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
03a8a1b6e7 BUGFIX: Redundant parameter to eprint. 2010-11-11 00:01:17 +01:00
Cas Cremers
2557d308bb CLEANUP: Add timing output to proof output. 2010-11-11 00:01:12 +01:00
Cas Cremers
6b3d572e3b BUGFIX: Fixed long-standing bug with timer values, wrongly using CLOCKS_PER_SEC. 2010-11-10 23:55:57 +01:00
Cas Cremers
5c53d4bb9e Better reindent script (from newCompromise branch) 2010-11-10 23:55:21 +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
519a9d0a81 Added factored-out 'warning_pre' function. 2010-11-10 10:37:57 +01:00
Cas Cremers
d633a62f0d BUGFIX: C-minimality was tripping over claims. 2009-01-28 20:45:58 +01:00
Cas Cremers
f21c02e772 BUGFIX: Build scripts did not always build unix version correctly. 2008-09-15 16:48:39 +02:00
Cas Cremers
6ffdda4a3c BUGFIX: Graph output correct removal of function applications. 
The graph output edge remover was incorrect, and would also
remove applications that were not completely triggered by M_0 alone.
 2008-08-26 13:25:43 +02:00
Cas Cremers
77cc97c03b Added a note for code cleanup. 2008-08-21 22:32:19 +02:00
Cas Cremers
0c06cb7a30 Added debug build script. 2008-08-21 21:57:42 +02: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
8f01637528 Output should also yield 'recv' instead of 'read'. 2008-08-21 16:58:57 +02:00
Cas Cremers
aaf27779a3 Allow for use of RECV instead of READ. 
Read will become deprecated later on.
 2008-08-21 16:58:53 +02:00
Cas Cremers
739f59174f Removed unused functions. 2008-08-21 16:58:12 +02:00
Cas Cremers
1a7aa73b26 Created a small program that can find unused functions. 2008-08-21 16:56:12 +02:00
Cas Cremers
a0a377a84f Added switch to disable verbose exit codes. 
In the near future, the default exit code behavior should be made obsolete anyway,
as the exit codes are not a nice way to report status.
It used to be convenient for shell scripting in early times,
when the parallel tests were run using the forward model
checker, but no modern script should be relying on it.
 2008-06-16 18:57:28 +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
27521d0e87 Added notes. 2008-03-13 10:24:13 +01: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
03522b7108 Try to not draw duplicate arrows. 
This cleans up some graphs rather nicely. There is only one potential
drawback (not observed in practive):
If two bindings have the same from/to, but different interpretations,
we might lose information. In particular the 'select' intermediate nodes might
pose a problem and we would be better off by not having any interpretation on
what is selected.
 2008-01-16 11:55:15 +01:00
Cas Cremers
bf24312fb1 Disabled intruder knowledge computation. 
Isolated problem causing segfault identified by Simon Meier.
 2008-01-10 16:50:02 +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
2d45daa8ee Introduced '-c,--characterize' switches for complete characterization. 
This switch was previously known as '--state-space', but the new name is
much better.

Backwards compatibility:

'-c' was previously used by '--check', so check is now abbreviated to
'-C'.

'-s,--state-space' still works but is from now on considered to be
deprecated.
 2007-11-15 21:49:56 +01:00
Cas Cremers
08bbdded3c Minor cleanup. 2007-10-22 21:42:43 +02:00
Cas Cremers
a6370726ef Cleanup. 2007-10-22 21:14:06 +02:00
Cas Cremers
b013440c8b Merge branch 'Todo' 2007-09-18 16:09:05 +02:00
Cas Cremers
2107d76532 Proof output improved for occurrences of the Athena problem. 2007-09-18 15:36:11 +02:00
Cas Cremers
59bcb18fec Caught Athena problem case. 
I've added a marked for the Athena problem case, and now no more false 'complete proof' results are produced.
However, the tool reports, 'no attack within bounds', which is slightly inaccurate
depending on the interpretatio of 'bounds'.
 2007-09-18 15:27:41 +02:00
Cas Cremers
8a2ae84f35 Added incompleteness marker for the untyped variables and MGDU set problem. 2007-09-17 16:54:17 +02:00
Cas Cremers
a93b555b1a Added cast to solve long-standing compilation warning. 
Note that the cast does not seem to be needed after manual inspection, but
the compiler insists.
 2007-09-17 16:53:37 +02:00
Cas Cremers
52e23f5c86 Merge branch 'manual' into 'master'. 2007-06-12 14:43:58 +02:00
Cas Cremers
4d1e62fac9 Removed a large number of obsolete files. 2007-06-12 14:39:08 +02:00
Cas Cremers
34ff7e28c6 Added GPL 2 notice to command-line usage of the Scyther backend. 
Modified '--version' to report the Scyther license briefly, and
added '--license' to display the full license.
 2007-06-11 15:05:49 +02: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
9f97e1e5d7 Moved todo text into a more sensible place. 2007-05-25 11:18:45 +02:00
Cas Cremers
76c516dee0 Merge branch 'reverting-b7' into release 2007-05-21 16:41:19 +02:00
Cas Cremers
742cbcda60 - Added some ignore patterns. 2007-05-21 13:56:00 +02:00
Cas Cremers
b80de55289 Merge branch 'testing' of cas@roivas.shape9.nl:/export/git/scyther into reverting-b7 2007-05-21 13:48:56 +02:00
Cas Cremers
461895555b - Removed Bin subdirectory and updates scripts. 2007-05-21 13:34:43 +02:00
Cas Cremers
f56a10646f Got rid of obsolete version number encoding. 
The old version numbers were retrieved from SVN; of course this no longer works. Now no versions are retrieved on normal building. Instead, this is covered by the dist building script.
 2007-05-20 16:08:56 +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
Cas Cremers
5882548643 - Forgot the bool file. 2007-05-18 13:57:33 +02:00
Cas Cremers
46636014c0 - Forgotten tempfile code. 2007-05-18 13:56:43 +02:00
Cas Cremers
7c8ca527b2 - Updates (fast forwarding to latest Scyther from svn) 2007-05-18 13:55:11 +02:00
Cas Cremers
814fbf31cd - Some obsolete bugs removed. 2007-05-18 08:11:54 +02:00
Cas Cremers
04b6ab4b36 - Added ignore patterns 
- Removed some obsolete bug reports (but more pruning is needed in the future)
 2007-05-18 00:34:02 +02:00