From da616c119846c58605c5426660045cbeca99187d Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 31 Mar 2011 15:00:56 +0200 Subject: [PATCH] Adding missing scripts. --- gui/combos-ike.sh | 8 ++++++ gui/combos-ikev0.sh | 12 ++++++++ gui/combos-ikev1.sh | 12 ++++++++ gui/combos-ikev2.sh | 13 +++++++++ gui/json-scyther.py | 66 +++++++++++++++++++++++++++++++++++++++++++ gui/precompute-ike.sh | 5 ++++ 6 files changed, 116 insertions(+) create mode 100755 gui/combos-ike.sh create mode 100755 gui/combos-ikev0.sh create mode 100755 gui/combos-ikev1.sh create mode 100755 gui/combos-ikev2.sh create mode 100755 gui/json-scyther.py create mode 100755 gui/precompute-ike.sh diff --git a/gui/combos-ike.sh b/gui/combos-ike.sh new file mode 100755 index 0000000..515b20e --- /dev/null +++ b/gui/combos-ike.sh @@ -0,0 +1,8 @@ +#!/bin/sh + +# Individual data +./combos-ikev1.sh +./combos-ikev2.sh + +# And combine +./combos-ikev0.sh diff --git a/gui/combos-ikev0.sh b/gui/combos-ikev0.sh new file mode 100755 index 0000000..389835b --- /dev/null +++ b/gui/combos-ikev0.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +bsub -W 8:00 -Jd "ike0-aa-t" -N ./test-mpa.py -m 2 --plain --latex ike0-aa-t ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-aa-b" -N ./test-mpa.py -m 2 --plain -b --latex ike0-aa-b ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-aa-u" -N ./test-mpa.py -m 2 --plain -u --latex ike0-aa-u ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-ex-t" -N ./test-mpa.py -m 2 --plain --extravert --latex ike0-ex-t ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-ex-b" -N ./test-mpa.py -m 2 --plain -b --extravert --latex ike0-ex-b ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-ex-u" -N ./test-mpa.py -m 2 --plain -u --extravert --latex ike0-ex-u ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-iu-t" -N ./test-mpa.py -m 2 --plain --init-unique --latex ike0-iu-t ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-iu-b" -N ./test-mpa.py -m 2 --plain -b --init-unique --latex ike0-iu-b ~/src/ikev2/pp-results/mpa/ikev*.spdl +bsub -W 8:00 -Jd "ike0-iu-u" -N ./test-mpa.py -m 2 --plain -u --init-unique --latex ike0-iu-u ~/src/ikev2/pp-results/mpa/ikev*.spdl + diff --git a/gui/combos-ikev1.sh b/gui/combos-ikev1.sh new file mode 100755 index 0000000..a5743b9 --- /dev/null +++ b/gui/combos-ikev1.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +bsub -W 8:00 -Jd "ike1-aa-t" -N ./test-mpa.py -m 2 --plain --latex ike1-aa-t ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-aa-b" -N ./test-mpa.py -m 2 --plain -b --latex ike1-aa-b ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-aa-u" -N ./test-mpa.py -m 2 --plain -u --latex ike1-aa-u ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-ex-t" -N ./test-mpa.py -m 2 --plain --extravert --latex ike1-ex-t ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-ex-b" -N ./test-mpa.py -m 2 --plain -b --extravert --latex ike1-ex-b ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-ex-u" -N ./test-mpa.py -m 2 --plain -u --extravert --latex ike1-ex-u ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-iu-t" -N ./test-mpa.py -m 2 --plain --init-unique --latex ike1-iu-t ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-iu-b" -N ./test-mpa.py -m 2 --plain -b --init-unique --latex ike1-iu-b ~/src/ikev2/pp-results/mpa/ikev1*.spdl +bsub -W 8:00 -Jd "ike1-iu-u" -N ./test-mpa.py -m 2 --plain -u --init-unique --latex ike1-iu-u ~/src/ikev2/pp-results/mpa/ikev1*.spdl + diff --git a/gui/combos-ikev2.sh b/gui/combos-ikev2.sh new file mode 100755 index 0000000..1da0bb1 --- /dev/null +++ b/gui/combos-ikev2.sh @@ -0,0 +1,13 @@ +#!/bin/sh + +bsub -W 8:00 -Jd "ike2-aa-t" -N ./test-mpa.py -m 2 --plain --latex ike2-aa-t ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-aa-b" -N ./test-mpa.py -m 2 --plain -b --latex ike2-aa-b ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-aa-u" -N ./test-mpa.py -m 2 --plain -u --latex ike2-aa-u ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-ex-t" -N ./test-mpa.py -m 2 --plain --extravert --latex ike2-ex-t ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-ex-b" -N ./test-mpa.py -m 2 --plain -b --extravert --latex ike2-ex-b ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-ex-u" -N ./test-mpa.py -m 2 --plain -u --extravert --latex ike2-ex-u ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-iu-t" -N ./test-mpa.py -m 2 --plain --init-unique --latex ike2-iu-t ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-iu-b" -N ./test-mpa.py -m 2 --plain -b --init-unique --latex ike2-iu-b ~/src/ikev2/pp-results/mpa/ikev2*.spdl +bsub -W 8:00 -Jd "ike2-iu-u" -N ./test-mpa.py -m 2 --plain -u --init-unique --latex ike2-iu-u ~/src/ikev2/pp-results/mpa/ikev2*.spdl + + diff --git a/gui/json-scyther.py b/gui/json-scyther.py new file mode 100755 index 0000000..51d8531 --- /dev/null +++ b/gui/json-scyther.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python +""" + Scyther : An automatic verifier for security protocols. + Copyright (C) 2007 Cas Cremers + + This program is free software; you can redistribute it and/or + modify it under the terms of the GNU General Public License + as published by the Free Software Foundation; either version 2 + of the License, or (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program; if not, write to the Free Software + Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. +""" + + +""" + +Author: Cas Cremers + +""" + +import sys +import json +from Scyther import Scyther + + +def scyther_json(jsondata): + """ + Decode json data into (protocollist,options,filter) and run scyther + """ + s = Scyther.Scyther() + + (protocollist,options,filter) = json.loads(jsondata) + + s.options = str(options) + for protocol in sorted(protocollist): + s.addFile(protocol) + s.verifyOne(str(filter)) + +def fileandline(fn,linenos): + fp = open(fn,"r") + ln = 1 + done = 0 + sz = len(linenos) + for l in fp.xreadlines(): + if str(ln) in linenos: + print l + scyther_json(l) + done = done + 1 + if done >= sz: + fp.close() + return + ln = ln + 1 + fp.close() + return + +if __name__ == '__main__': + fileandline(sys.argv[1],set(sys.argv[2:])) + + diff --git a/gui/precompute-ike.sh b/gui/precompute-ike.sh new file mode 100755 index 0000000..7b7652f --- /dev/null +++ b/gui/precompute-ike.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +./batcher.sh -m 2 --all-types --self-communication ~/src/ikev2/pp-results/mpa/ikev1*.spdl +./batcher.sh -m 2 --all-types --self-communication ~/src/ikev2/pp-results/mpa/ikev2*.spdl +