Cas Cremers
266e5fb26b
BRUTUS: Added special build script.
...
Originates in newCompromise branch.
2010-11-11 12:14:49 +01:00
Cas Cremers
8ddd955415
MPA: Better test setup.
2010-11-11 12:08:53 +01:00
Cas Cremers
65074352c3
MPA: Improving the summaries given by the test script.
2010-11-11 11:16:59 +01:00
Cas Cremers
01eb5854cf
EFFICIENCY: If a new dependency overlaps with an old one, we don't have to recompute the closure.
2010-11-11 10:37:18 +01:00
Cas Cremers
6cd8007ab0
EFFICIENCY: New (default) heuristic.
...
Given that sk/pk/k are now hardcoded, we can exploit their occurrences with this
new heuristic.
The heuristic can now scan for the lowest term depth at which either sk or k occur.
This will cause the heuristic to favor looking for sk, then sk(x), and only later
other terms. In a small test this was twice as fast. For protocols based on pk only
the performance loss should be negligible.
The old heuristic was 162, now it is 162+512 = 674.
2010-11-11 10:37:18 +01:00
Cas Cremers
e42aa1215e
Scyther.py: Added Caching to Scyther's Python interface.
...
Cached data is stored in:
Cache/XX/YYYYY.out (stdout)
Cache/XX/YYYYY.err (stderr)
Where XX^YYYYY is the sha256 hexdigest of the concatenation of the input spdl and
the arguments.
2010-11-11 10:37:18 +01:00
Cas Cremers
cbb66ea794
Scyther.py: Improving Scyther python interface by giving options and filenames when reporting an error.
2010-11-11 10:37:18 +01:00
Cas Cremers
fac14fc950
Added a new subdirectory with protocols for MPA experiments.
2010-11-11 10:37:18 +01:00
Cas Cremers
96e52a3724
Expanding test script for full MPA analysis.
2010-11-11 10:37:18 +01:00
Cas Cremers
fcf694dbd9
CLEANUP: Reindenting code.
2010-11-11 00:09:16 +01:00
Cas Cremers
619ecf7673
Added commented-out code to use llvm as a compiler instead of gcc when needed.
2010-11-11 00:02:36 +01:00
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
a7f68bcb40
Removed Eve from one demo file.
2010-06-03 22:47:29 +02:00
Cas Cremers
e5fc05a379
Correctly escaping program file name.
2010-05-16 00:36:06 +02:00
Cas Cremers
dc4dc34624
String commands require shell=True.
2010-05-16 00:33:53 +02:00
Cas Cremers
d1b334765b
Updated image construction code to also use subprocess.Popen.
2010-05-16 00:13:33 +02:00
Cas Cremers
1f75f73cb0
Added realistic check for graphviz/dot.
2010-05-15 23:27:11 +02:00
Cas Cremers
7d03f22b24
Added new 'safeCommandOutput' command to Scyther/Misc and force use of Python 2.4 or later.
2010-05-15 23:26:44 +02:00
Cas Cremers
feb400c610
Added GUI error message if wxPython is not present.
...
If wxPython is not present, there would be a command-line message only.
Some users may not notice that. We now fall back to Tkinter to report
such messages.
2010-05-15 22:56:48 +02:00
Cas Cremers
f8ad858d87
Removed huge file; unclear why this was in here anyway.
2010-05-11 10:58:38 +02:00
Cas Cremers
a45172583f
Removed obsolete bibliography data from README.
2010-05-02 23:37:07 +02:00
Cas Cremers
2a2a087cf6
GUI BUGFIX: On some file systems, problems with case-insensitivity and name clash between sys module and local.
2009-04-30 15:06:28 +02:00
Cas Cremers
cd33fb3e14
BUGFIX: Paths with control characters (e.g. $) were causing trouble.
2009-04-30 13:40:06 +02: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
97991116bd
Fixed release scripts to work with new git conventions.
2008-09-10 11:20:50 +02:00
Cas Cremers
e3268bb8e5
GUI: Added a large set of possible output formats to the right-click menu.
...
To do: We still need better error handling.
- File exists: overwrite?
- Write failed popup.
- Check for empty file at the end (what if dot does not support this particular
output format?)
2008-08-29 12:05:06 +02:00
Cas Cremers
63471c5053
Code cleanup for GUI code.
2008-08-29 12:05:06 +02:00
Cas Cremers
8471f13da3
Added 'prune' switch support in GUI.
...
Allows to use the 'stop at first attack' feature of the backend.
2008-08-29 12:05:00 +02:00
Cas Cremers
b352044f92
BUGFIX: PIL is tested at the start of the program.
...
Previously, one would get one void verification result before Scyther detected
PIL was not working. Now nothing is wasted.
2008-08-26 21:52:00 +02:00
Cas Cremers
a020cffec7
GUI: Added popup menu to save graphviz (.dot) data.
...
A long requested feature was the option to print graphs more nicely.
This is a solution for knowledgeable users: the dot data is more basic
and can be converted in various ways.
TODO: Simple image export.
2008-08-26 17:35:38 +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
76bf6328b6
Nicer crash handling for PIL problem with a warning etc.
2008-08-21 21:57:22 +02:00
Cas Cremers
eb64f68968
Added loop script which I had always wanted before.
2008-08-21 21:55:55 +02:00
Cas Cremers
630f6e9459
Added large delta-test script.
...
The script runs over all protocol files it can find, and runs it using two different
command-line parameters to scyther. If the results differ, the script reports it.
The code can use some cleanup, removing e.g. global variables, but it works.
2008-08-21 21:20:16 +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
feb3827ba1
BUGFIX: Fixed crash on some include file cases.
...
Reported by ETH students last year: if you include a file, where the file has an
error in a line with a number higher than the original, the Python code crashes.
This is a *patch* only because the real underlying problem is that error reporting
does not take include commands into account, and does not propagate any
file names.
2008-07-31 17:37:20 +02:00