diff --git a/gui/Scripts/regression-test.py b/gui/Scripts/regression-test.py new file mode 100755 index 0000000..de9ab63 --- /dev/null +++ b/gui/Scripts/regression-test.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python + +""" + Scyther : An automatic verifier for security protocols. + Copyright (C) 2007-2012 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. +""" + +def testSet(blacklist=[]): + import os + + prefix = "../Protocols/" + dl = os.listdir(prefix) + fl = [] + for fn in dl: + if fn.endswith(".spdl"): + okay = True + for fb in blacklist: + if fn.startswith(fb): + okay = False + break + if okay: + fl.append((prefix,fn)) + return fl + +def evaluate(fn,prefix=""): + import subprocess + import tempfile + + cmd = "../Scyther/scyther-linux" + args = [cmd,"--max-runs=4","--plain",fn] + + fstdout = tempfile.TemporaryFile() + fstderr = tempfile.TemporaryFile() + + subprocess.call(args,stdout=fstdout,stderr=fstderr) + + fstdout.seek(0) + fstderr.seek(0) + + res = "" + for l in fstdout.xreadlines(): + res += prefix + l.strip() + "\n" + #for l in fstderr.xreadlines(): + # print l + + fstdout.close() + fstderr.close() + return res + + +def main(): + dest = "regression-test.txt" + output = "regression-test.txt.tmp" + + fp = open(output, 'w') + + fl = testSet(blacklist=['ksl']) + cnt = 1 + tres = "" + for (prefix,fn) in sorted(fl): + print "Evaluating %s (%i/%i)" % (fn,cnt,len(fl)) + res = evaluate(prefix+fn, "%s\t" % (fn)) + fp.write(res) + tres += res + cnt += 1 + fp.close() + + fp = open(dest, 'w') + fp.write(tres) + fp.close() + + print res + + + +if __name__ == '__main__': + main() diff --git a/gui/Scripts/regression-test.txt b/gui/Scripts/regression-test.txt new file mode 100644 index 0000000..3fa247f --- /dev/null +++ b/gui/Scripts/regression-test.txt @@ -0,0 +1,64 @@ +BKE.spdl claim bke,I SKR_4 kir Ok [no attack within bounds] +BKE.spdl claim bke,R SKR_7 kir Ok [no attack within bounds] +TLS-Paulson.spdl claim tlspaulson,a SKR_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [no attack within bounds] +TLS-Paulson.spdl claim tlspaulson,a SKR_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [no attack within bounds] +TLS-Paulson.spdl claim tlspaulson,b SKR_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [no attack within bounds] +TLS-Paulson.spdl claim tlspaulson,b SKR_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [no attack within bounds] +ccitt509-1.spdl claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness] +ccitt509-1c.spdl claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness] +ccitt509-3.spdl claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness] +ccitt509-3.spdl claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness] +ccitt509-3.spdl claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness] +ccitt509-3.spdl claim ccitt509-3,R Nisynch_R1 - Fail [at least 3 attacks] +ccitt509-3.spdl claim ccitt509-3,R Secret_R2 Ya Ok [no attack within bounds] +ccitt509-3.spdl claim ccitt509-3,R Secret_R3 Yb Ok [no attack within bounds] +ccitt509-ban3.spdl claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness] +ccitt509-ban3.spdl claim ccitt509-ban3,R Nisynch_5 - Ok [no attack within bounds] +needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [no attack within bounds] +needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [no attack within bounds] +needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks] +needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [no attack within bounds] +needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [no attack within bounds] +needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks] +needham-schroeder.spdl claim needhamschroederpk,I Secret_I1 Ni Ok [no attack within bounds] +needham-schroeder.spdl claim needhamschroederpk,I Secret_I2 Nr Ok [no attack within bounds] +needham-schroeder.spdl claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks] +needham-schroeder.spdl claim needhamschroederpk,R Secret_R1 Nr Fail [at least 5 attacks] +needham-schroeder.spdl claim needhamschroederpk,R Secret_R2 Ni Fail [at least 5 attacks] +needham-schroeder.spdl claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks] +smartright.spdl claim smartright,R Nisynch_R1 - Fail [at least 1 attack] +splice-as-cj.spdl claim spliceAS-CJ,I Secret_7 N2 Ok [no attack within bounds] +splice-as-cj.spdl claim spliceAS-CJ,I Niagree_9 - Fail [at least 1 attack] +splice-as-cj.spdl claim spliceAS-CJ,I Nisynch_10 - Fail [at least 1 attack] +splice-as-cj.spdl claim spliceAS-CJ,R Secret_8 N2 Ok [no attack within bounds] +splice-as-cj.spdl claim spliceAS-CJ,R Niagree_11 - Fail [at least 1 attack] +splice-as-cj.spdl claim spliceAS-CJ,R Nisynch_12 - Fail [at least 1 attack] +splice-as-hc.spdl claim spliceAS-HC,I Secret_7 N2 Ok [no attack within bounds] +splice-as-hc.spdl claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack] +splice-as-hc.spdl claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack] +splice-as-hc.spdl claim spliceAS-HC,R Secret_8 N2 Ok [no attack within bounds] +splice-as-hc.spdl claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack] +splice-as-hc.spdl claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack] +splice-as.spdl claim spliceAS,I Secret_7 N2 Ok [no attack within bounds] +splice-as.spdl claim spliceAS,I Niagree_9 - Fail [at least 1 attack] +splice-as.spdl claim spliceAS,I Nisynch_10 - Fail [at least 1 attack] +splice-as.spdl claim spliceAS,R Secret_8 N2 Ok [no attack within bounds] +splice-as.spdl claim spliceAS,R Niagree_11 - Fail [at least 1 attack] +splice-as.spdl claim spliceAS,R Nisynch_12 - Fail [at least 1 attack] +woo-lam-pi-1.spdl claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks] +woo-lam-pi-2.spdl claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks] +woo-lam-pi-3.spdl claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks] +woo-lam-pi-f.spdl claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack] +woo-lam-pi.spdl claim woolamPi,R Nisynch_R1 - Fail [at least 2 attacks] +yahalom-ban-paulson-modified.spdl claim yahalom-BAN-Paulson-modified,A Secret_5 kab Ok [no attack within bounds] +yahalom-ban-paulson-modified.spdl claim yahalom-BAN-Paulson-modified,B Secret_6 kab Ok [no attack within bounds] +yahalom-ban-paulson.spdl claim yahalom-BAN-Paulson,A SKR_5 kab Ok [no attack within bounds] +yahalom-ban-paulson.spdl claim yahalom-BAN-Paulson,B SKR_6 kab Ok [no attack within bounds] +yahalom-lowe.spdl claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness] +yahalom-lowe.spdl claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness] +yahalom-lowe.spdl claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness] +yahalom-lowe.spdl claim yahalom-Lowe,R Nisynch_R2 - Ok [no attack within bounds] +yahalom.spdl claim yahalom,I Secret_I1 Kir Ok [no attack within bounds] +yahalom.spdl claim yahalom,R Secret_R1 Kir Ok [no attack within bounds] +yahalom.spdl claim yahalom,S Secret_S1 Ni Fail [at least 1 attack] +yahalom.spdl claim yahalom,S Secret_S2 Nr Ok [no attack within bounds]