andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Adding missing scripts.

Browse Source
This commit is contained in:
Cas Cremers 2011-03-31 15:00:56 +02:00
parent a03f06ea41
commit da616c1198
6 changed files with 116 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
gui/combos-ike.sh Executable file
View File

@ -0,0 +1,8 @@
#!/bin/sh
# Individual data
./combos-ikev1.sh
./combos-ikev2.sh
# And combine
./combos-ikev0.sh

12
gui/combos-ikev0.sh Executable file
View File

@ -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

12
gui/combos-ikev1.sh Executable file
View File

@ -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

13
gui/combos-ikev2.sh Executable file
View File

@ -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

66
gui/json-scyther.py Executable file
View File

@ -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:]))

5
gui/precompute-ike.sh Executable file
View File

@ -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