Updated changelogs and readme's.
This commit is contained in:
Cas Cremers
parent
091ce01f60
commit
408a88807f
@ -55,7 +55,7 @@ Manual
|
|||||||
We are currently rewriting the manual. The current (incomplete) snapshot
|
We are currently rewriting the manual. The current (incomplete) snapshot
|
||||||
of the manual can be found here:
|
of the manual can be found here:
|
||||||
|
|
||||||
* `./doc/scyther-manual.pdf
|
* `./doc/manual/scyther-manual.pdf`
|
||||||
|
|
||||||
|
|
||||||
Protocol Models
|
Protocol Models
|
||||||
|
|||||||
@ -1,67 +1,120 @@
|
|||||||
---------------------
|
Scyther changelog
|
||||||
- Scyther changelog -
|
===============================
|
||||||
---------------------
|
|
||||||
|
|
||||||
Next release:
|
Scyther 1.1
|
||||||
|
-------------------------------
|
||||||
|
|
||||||
Bugfixes:
|
Major new features:
|
||||||
|
|
||||||
* Python 2.5 has integrated (c)elementtree into the core.
|
* [Language] Added support for `macro Term1 = Term2;` definitions, which greatly
|
||||||
Unfortunaly, this broke our previous import attempts.
|
simplifies many specifications.
|
||||||
|
* [Language] Added support for `match(T1,T2);` events in roles, which
|
||||||
|
can be used for e.g. a straightforward modeling of delayed decryption.
|
||||||
|
* [Language] Added support for `not match(T1,T2);` events in roles.
|
||||||
|
This can be useful for, e.g., modeling protocol restrictions (such as
|
||||||
|
`A != B`).
|
||||||
|
* [Language] Added support for `option "COMMANDLINE_OPTIONS";` in
|
||||||
|
specifications. This provides full access to the command-line options
|
||||||
|
of the Scyther backend to the protocol specifications. An example of
|
||||||
|
its use is `option "--one-role-per-agent";`.
|
||||||
|
* [Mac OS X] Dropped support for PPC in Scyther distributions, only
|
||||||
|
supporting Intel for now. Note that installing from source may still
|
||||||
|
work fine with a minor tweak to the build script.
|
||||||
|
|
||||||
|
Additional protocol models:
|
||||||
|
|
||||||
|
See <http://people.inf.ethz.ch/cremersc/tools/protocols.html> for a
|
||||||
|
more high-level overview of selected protocol models.
|
||||||
|
|
||||||
|
* IEEE 802.16e/WIMAX: PKMv2rsa and variants
|
||||||
|
* IKEv1 and IKEv2 protocol suites
|
||||||
|
|
||||||
|
Other new features:
|
||||||
|
|
||||||
|
* `SCYTHERCACHEDIR` environment variable can be set to override the
|
||||||
|
internal cache path.
|
||||||
|
* [Backend] The command-line tool now supports the option
|
||||||
|
`--one-role-per-agent`. This disallows agents from performing more than
|
||||||
|
one role in a single trace. This effectively partitions the agents into
|
||||||
|
role sets, i.e., each role can only be performed by agents from one of
|
||||||
|
these sets.
|
||||||
|
* [Documentation] Added the first incomplete version of the new manual.
|
||||||
|
|
||||||
|
There are also various minor bugfixes and installation improvements.
|
||||||
|
|
||||||
|
Scyther 1.0
|
||||||
|
-------------------------------
|
||||||
|
|
||||||
|
Major new features:
|
||||||
|
|
||||||
|
* [Language] Support for weak agreement
|
||||||
|
* [Language] Support for non-injective data agreement through `Commit`
|
||||||
|
and `Running` signals.
|
||||||
|
|
||||||
|
Bugfixes:
|
||||||
|
|
||||||
|
* Python 2.5 has integrated (c)elementtree into the core.
|
||||||
|
Unfortunaly, this broke our previous import attempts. This has now
|
||||||
|
been fixed.
|
||||||
|
|
||||||
Scyther 1.0-beta7.1
|
Scyther 1.0-beta7.1
|
||||||
|
-------------------------------
|
||||||
|
|
||||||
Bugfixes:
|
Bugfixes:
|
||||||
|
|
||||||
* Windows Vista fix broke Windows XP support.
|
* Windows Vista fix broke Windows XP support.
|
||||||
|
|
||||||
Scyther 1.0-beta7
|
Scyther 1.0-beta7
|
||||||
|
-------------------------------
|
||||||
|
|
||||||
Bugfixes:
|
Bugfixes:
|
||||||
|
|
||||||
* Windows Vista causes a number of problems. The biggest problem
|
* Windows Vista causes a number of problems. The biggest problem
|
||||||
is now fixed, which is the bad implementation of the tmpfile() C
|
is now fixed, which is the bad implementation of the tmpfile() C
|
||||||
function, causing no attack output, for which there is a
|
function, causing no attack output, for which there is a
|
||||||
workaround now.
|
workaround now.
|
||||||
|
|
||||||
Scyther 1.0-beta6
|
Scyther 1.0-beta6
|
||||||
|
-------------------------------
|
||||||
Big new features:
|
|
||||||
|
Major new features:
|
||||||
|
|
||||||
* [Gui] Added Mac support (added universal binary)
|
* [Gui] Added Mac support (added universal binary)
|
||||||
* [Gui] Switched to Scintilla editor component, providing undo
|
* [Gui] Switched to Scintilla editor component, providing undo
|
||||||
and line numbering, and highlighting of error lines.
|
and line numbering, and highlighting of error lines.
|
||||||
|
|
||||||
Other new features:
|
Other new features:
|
||||||
|
|
||||||
* [Backend] Scyther now detects when a recv event cannot match
|
* [Backend] Scyther now detects when a recv event cannot match
|
||||||
with a send event. This significantly helps in reducing errors
|
with a send event. This significantly helps in reducing errors
|
||||||
in the protocol descriptions.
|
in the protocol descriptions.
|
||||||
* [Language] Added claim parameter for Reachable claim;
|
* [Language] Added claim parameter for Reachable claim;
|
||||||
Reachable,R means that role R should be trusted (as well as the
|
Reachable,R means that role R should be trusted (as well as the
|
||||||
actor), but not any other role. This can be useful for showing
|
actor), but not any other role. This can be useful for showing
|
||||||
stronger authentication properties of protocols with more than
|
stronger authentication properties of protocols with more than
|
||||||
two parties.
|
two parties.
|
||||||
* [Backend] Added '--max-of-role=N' switch (to narrow scenarios)
|
* [Backend] Added '--max-of-role=N' switch (to narrow scenarios)
|
||||||
* [Backend] Added '--scan-claims' switch (allows for retrieving
|
* [Backend] Added '--scan-claims' switch (allows for retrieving
|
||||||
a list of claims)
|
a list of claims)
|
||||||
* [Scripting] Added 'verifyOne' and 'scanClaims' methods to
|
* [Scripting] Added 'verifyOne' and 'scanClaims' methods to
|
||||||
Scyther object, to help with singular claim testing.
|
Scyther object, to help with singular claim testing.
|
||||||
|
|
||||||
Bugfixes:
|
Bugfixes:
|
||||||
|
|
||||||
* [Scripting] Fixed bug in python interface backend (e.g. with mpa.py)
|
* [Scripting] Fixed bug in python interface backend (e.g. with mpa.py)
|
||||||
|
|
||||||
Scyther 1.0-beta5
|
Scyther 1.0-beta5
|
||||||
|
-------------------------------
|
||||||
|
|
||||||
* Change of switch semantics. '--max-attacks=N' now defines the
|
* Change of switch semantics. '--max-attacks=N' now defines the
|
||||||
maximum number of attacks per claim. Previously this was a
|
maximum number of attacks per claim. Previously this was a
|
||||||
global maximum for all claims combined.
|
global maximum for all claims combined.
|
||||||
* Improved attack graph output.
|
* Improved attack graph output.
|
||||||
* added switch '--errors=FILE' to redirect standard error output
|
* added switch '--errors=FILE' to redirect standard error output
|
||||||
to a file.
|
to a file.
|
||||||
* Rewrote parts of the gui code for improved stability.
|
* Rewrote parts of the gui code for improved stability.
|
||||||
|
|
||||||
Scyther 1.0-beta4
|
Scyther 1.0-beta4
|
||||||
|
-------------------------------
|
||||||
|
|
||||||
* (Changelog starts after the release of Scyther 1.0-beta4)
|
* (Changelog starts after the release of Scyther 1.0-beta4)
|
||||||
|
|||||||
66
gui/README.md
Normal file
66
gui/README.md
Normal file
@ -0,0 +1,66 @@
|
|||||||
|
The Scyther tool
|
||||||
|
================
|
||||||
|
|
||||||
|
Scyther is a tool for the symbolic analysis of security protocols. It is
|
||||||
|
developed by Cas Cremers, and is available from
|
||||||
|
<http://people.inf.ethz.ch/cremersc/scyther/index.html>.
|
||||||
|
|
||||||
|
The below instructions apply only to the *distribution version* of
|
||||||
|
the Scyther tool. If you are working from the source files, some paths may be
|
||||||
|
slightly different, and it is recommended to follow the instructions in '../README.md'.
|
||||||
|
|
||||||
|
Running the scyther tool
|
||||||
|
------------------------
|
||||||
|
|
||||||
|
### Graphical user interface ###
|
||||||
|
|
||||||
|
The graphical user interface can be started by running `scyther-gui.py`,
|
||||||
|
e.g., enter the following in a terminal and press return
|
||||||
|
|
||||||
|
python ./scyther-gui.py
|
||||||
|
|
||||||
|
### Command-line usage ###
|
||||||
|
|
||||||
|
In the directory `./Scyther` there should be an executable for the
|
||||||
|
Scyther backend. Its name depends on the platform:
|
||||||
|
|
||||||
|
* `scyther-linux` (Linux)
|
||||||
|
* `scyther-w32` (Windows)
|
||||||
|
* `scyther-mac` (Mac OS X)
|
||||||
|
|
||||||
|
If this executable does not exist, you probably downloaded the source
|
||||||
|
files, and will need to compile it first. See `../README.md` for further
|
||||||
|
details.
|
||||||
|
|
||||||
|
There are also various test scripts (for usage in Linux) in this
|
||||||
|
directory.
|
||||||
|
|
||||||
|
Obtaining the sources
|
||||||
|
----------------------
|
||||||
|
|
||||||
|
Scyther is being developed on *Github*, and its complete source files are
|
||||||
|
availabe from
|
||||||
|
<https://github.com/cascremers/scyther>.
|
||||||
|
|
||||||
|
Manual
|
||||||
|
------
|
||||||
|
|
||||||
|
We are currently rewriting the manual. The current (incomplete)
|
||||||
|
distribution version of the manual can be found here:
|
||||||
|
|
||||||
|
* `./scyther-manual.pdf`
|
||||||
|
|
||||||
|
|
||||||
|
Protocol Models
|
||||||
|
---------------
|
||||||
|
|
||||||
|
The protocol models have the extension `.spdl` and can be found in the following directories:
|
||||||
|
|
||||||
|
* `./Protocols` and its subdirectories.
|
||||||
|
|
||||||
|
License
|
||||||
|
-------
|
||||||
|
|
||||||
|
Currently the Scyther tool is licensed under the GPL 2, as indicated in
|
||||||
|
the source code. Contact Cas Cremers if you have any questions.
|
||||||
|
|
||||||
@ -1,35 +0,0 @@
|
|||||||
------------------------------------------------------------------------
|
|
||||||
|
|
||||||
Scyther
|
|
||||||
|
|
||||||
an automatic verification tool for security protocols
|
|
||||||
by Cas Cremers
|
|
||||||
|
|
||||||
------------------------------------------------------------------------
|
|
||||||
|
|
||||||
|
|
||||||
Note: This is a BETA release, and therefore the usual warnings apply.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
1. More information
|
|
||||||
========================================================================
|
|
||||||
|
|
||||||
For more information, see:
|
|
||||||
|
|
||||||
http://people.inf.ethz.ch/cremersc/scyther/index.html
|
|
||||||
|
|
||||||
|
|
||||||
2. Starting out
|
|
||||||
========================================================================
|
|
||||||
|
|
||||||
Start the graphical user interface by starting
|
|
||||||
|
|
||||||
scyther-gui.py
|
|
||||||
|
|
||||||
Some protocol description files (with extension .spdl) can be found in
|
|
||||||
the base directory. Many other protocol input files can be found in the
|
|
||||||
'Protocols' directory.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Loading…
Reference in New Issue
Block a user