From 408a88807f1861db3be2c1b376956d042e93300f Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Mon, 17 Dec 2012 11:26:04 +0100 Subject: [PATCH] Updated changelogs and readme's. --- README.md | 2 +- gui/Changelog.txt | 139 ++++++++++++++++++++++++++++++++-------------- gui/README.md | 66 ++++++++++++++++++++++ gui/README.txt | 35 ------------ 4 files changed, 163 insertions(+), 79 deletions(-) create mode 100644 gui/README.md delete mode 100644 gui/README.txt diff --git a/README.md b/README.md index da224e8..339ccdd 100644 --- a/README.md +++ b/README.md @@ -55,7 +55,7 @@ Manual We are currently rewriting the manual. The current (incomplete) snapshot of the manual can be found here: - * `./doc/scyther-manual.pdf + * `./doc/manual/scyther-manual.pdf` Protocol Models diff --git a/gui/Changelog.txt b/gui/Changelog.txt index a72997e..99b7416 100644 --- a/gui/Changelog.txt +++ b/gui/Changelog.txt @@ -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. - Unfortunaly, this broke our previous import attempts. + * [Language] Added support for `macro Term1 = Term2;` definitions, which greatly + 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 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 +------------------------------- - Bugfixes: +Bugfixes: - * Windows Vista fix broke Windows XP support. + * Windows Vista fix broke Windows XP support. Scyther 1.0-beta7 +------------------------------- - Bugfixes: +Bugfixes: - * Windows Vista causes a number of problems. The biggest problem - is now fixed, which is the bad implementation of the tmpfile() C - function, causing no attack output, for which there is a - workaround now. + * Windows Vista causes a number of problems. The biggest problem + is now fixed, which is the bad implementation of the tmpfile() C + function, causing no attack output, for which there is a + workaround now. Scyther 1.0-beta6 - - Big new features: +------------------------------- + +Major new features: - * [Gui] Added Mac support (added universal binary) - * [Gui] Switched to Scintilla editor component, providing undo - and line numbering, and highlighting of error lines. + * [Gui] Added Mac support (added universal binary) + * [Gui] Switched to Scintilla editor component, providing undo + and line numbering, and highlighting of error lines. - Other new features: +Other new features: - * [Backend] Scyther now detects when a recv event cannot match - with a send event. This significantly helps in reducing errors - in the protocol descriptions. - * [Language] Added claim parameter for Reachable claim; - 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 - stronger authentication properties of protocols with more than - two parties. - * [Backend] Added '--max-of-role=N' switch (to narrow scenarios) - * [Backend] Added '--scan-claims' switch (allows for retrieving - a list of claims) - * [Scripting] Added 'verifyOne' and 'scanClaims' methods to - Scyther object, to help with singular claim testing. + * [Backend] Scyther now detects when a recv event cannot match + with a send event. This significantly helps in reducing errors + in the protocol descriptions. + * [Language] Added claim parameter for Reachable claim; + 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 + stronger authentication properties of protocols with more than + two parties. + * [Backend] Added '--max-of-role=N' switch (to narrow scenarios) + * [Backend] Added '--scan-claims' switch (allows for retrieving + a list of claims) + * [Scripting] Added 'verifyOne' and 'scanClaims' methods to + 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 +------------------------------- - * Change of switch semantics. '--max-attacks=N' now defines the - maximum number of attacks per claim. Previously this was a - global maximum for all claims combined. - * Improved attack graph output. - * added switch '--errors=FILE' to redirect standard error output - to a file. - * Rewrote parts of the gui code for improved stability. + * Change of switch semantics. '--max-attacks=N' now defines the + maximum number of attacks per claim. Previously this was a + global maximum for all claims combined. + * Improved attack graph output. + * added switch '--errors=FILE' to redirect standard error output + to a file. + * Rewrote parts of the gui code for improved stability. Scyther 1.0-beta4 +------------------------------- - * (Changelog starts after the release of Scyther 1.0-beta4) + * (Changelog starts after the release of Scyther 1.0-beta4) diff --git a/gui/README.md b/gui/README.md new file mode 100644 index 0000000..8813c5e --- /dev/null +++ b/gui/README.md @@ -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 +. + +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 +. + +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. + diff --git a/gui/README.txt b/gui/README.txt deleted file mode 100644 index 68cc720..0000000 --- a/gui/README.txt +++ /dev/null @@ -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. - - -