Added regression test script.

This commit is contained in:
Cas Cremers 2012-06-12 22:30:23 +02:00
parent 588ae30bef
commit 163a915a6d
2 changed files with 155 additions and 0 deletions

91
gui/Scripts/regression-test.py Executable file
View File

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

View File

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