diff --git a/src/regression-tests/Makefile b/src/regression-tests/Makefile new file mode 100644 index 0000000..c2bd104 --- /dev/null +++ b/src/regression-tests/Makefile @@ -0,0 +1,5 @@ + +results: + ./regression-test.py + +.PHONY: results diff --git a/src/regression-tests/regression-test.py b/src/regression-tests/regression-test.py new file mode 100755 index 0000000..a27e5df --- /dev/null +++ b/src/regression-tests/regression-test.py @@ -0,0 +1,140 @@ +#!/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. +""" + +""" +regression-test.py + +Regression tests for changes to the Scyther executable. +""" + +""" +For each file, we run a test with some parameters, and check the result. + +We do this for a large set of protocols, but also for some subset with 'special' parameters. +The tests are described in "tests.txt" + +Each line is considered a sequence of arguments. +The output is written to test-X.out, where X is a sanitized version of the argument line. +""" + +def sanitize(arg): + """ + Take an argument line and sanitize it. + + Return argument may well be empty, which causes an error + """ + from string import printable + + l = "" + for c in arg: + if c in printable: + l = l + c + l = l.strip() + + removes = "\\\"'`{}$" + for x in removes: + l = l.replace(x,"") + + l = l.replace("\t"," ") + #ol = l + #l = ol + "x" + #while l != ol: + # l = ol.replace(" "," ") + + #l = l.replace(" ","_") + l = l.replace("/","-") + + l = l.strip() + assert(len(l) > 0) + return l + + +def runTest(arg,destdir="."): + """ + Run a test and store the result. + + Time measurement is super coarse and depends, among other things, on me + browsing in the background during the tests. + """ + import subprocess + import time + from os.path import join + + nm = sanitize(arg) + outfile = join(destdir,"test-%s.out" % (nm)) + errfile = join(destdir,"test-%s.err" % (nm)) + clkfile = join(destdir,"test-%s.time" % (nm)) + + starttime = time.time() # Time in seconds + + cmd = "../scyther-linux ../../%s --output=\"%s\" --errors=\"%s\"" % (arg,outfile,errfile) + subprocess.call(cmd,shell=True) + + delta = time.time() - starttime # Duration in seconds + + fp = open(clkfile,'w') + fp.write("Passed wall time in seconds:\n%i\n" % (delta)) + fp.close() + + +def runTests(fn,destdir="."): + + fp = open(fn,'r') + tests = [] + clen = 0 + for l in fp.xreadlines(): + if l.startswith("#") or l.startswith("%"): + continue + d = l.strip() + if len(d) > 0: + tests.append(d) + if not d.startswith("="): + # We skip the 'global' settings + clen = clen + 1 + fp.close() + + print "Running %i tests." % (clen) + print "Destination: %s" % (destdir) + cnt = 1 + setting = "" + for l in tests: + if l.startswith("="): + + setting = l[1:] + if len(setting.strip()) == 0: + setting = "" + + print "Changing global setting to \"%s\"" % (setting) + + else: + print "%i/%i: Evaluating %s" % (cnt,clen,l+setting) + runTest(l+setting,destdir) + cnt = cnt + 1 + + +def main(): + runTests("tests.txt","results") + + +if __name__ == "__main__": + main() + + + diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..91b2ee0 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.out @@ -0,0 +1,8 @@ +claim ns3,I Secret_i1 ni Ok [proof of correctness] +claim ns3,I Secret_i2 nr Ok [proof of correctness] +claim ns3,I Niagree_i3 - Ok [proof of correctness] +claim ns3,I Nisynch_i4 - Ok [proof of correctness] +claim ns3,R Secret_r1 ni Fail [at least 1 attack] +claim ns3,R Secret_r2 nr Fail [at least 1 attack] +claim ns3,R Niagree_r3 - Fail [at least 1 attack] +claim ns3,R Nisynch_r4 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-ns3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out new file mode 100644 index 0000000..39d339c --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.out @@ -0,0 +1,8 @@ +claim nsl3-broken,I Secret_i1 ni Fail [at least 1 attack] +claim nsl3-broken,I Secret_i2 nr Fail [at least 1 attack] +claim nsl3-broken,I Niagree_i3 - Fail [at least 1 attack] +claim nsl3-broken,I Nisynch_i4 - Fail [at least 1 attack] +claim nsl3-broken,R Secret_r1 ni Fail [at least 1 attack] +claim nsl3-broken,R Secret_r2 nr Ok [proof of correctness] +claim nsl3-broken,R Niagree_r3 - Ok [proof of correctness] +claim nsl3-broken,R Nisynch_r4 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-broken.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out new file mode 100644 index 0000000..d76f35e --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.out @@ -0,0 +1,16 @@ +claim nsl3-broken,I Secret_i1 ni Fail [at least 3 attacks] +claim nsl3-broken,I Secret_i2 nr Fail [at least 1 attack] +claim nsl3-broken,I Niagree_i3 - Fail [at least 1 attack] +claim nsl3-broken,I Nisynch_i4 - Fail [at least 1 attack] +claim nsl3-broken,R Secret_r1 ni Fail [at least 2 attacks] +claim nsl3-broken,R Secret_r2 nr Ok [proof of correctness] +claim nsl3-broken,R Niagree_r3 - Fail [at least 1 attack] +claim nsl3-broken,R Nisynch_r4 - Fail [at least 1 attack] +claim nsl3,I Secret_i1 ni Fail [at least 2 attacks] +claim nsl3,I Secret_i2 nr Fail [at least 1 attack] +claim nsl3,I Niagree_i3 - Fail [at least 1 attack] +claim nsl3,I Nisynch_i4 - Fail [at least 1 attack] +claim nsl3,R Secret_r1 ni Fail [at least 2 attacks] +claim nsl3,R Secret_r2 nr Ok [proof of correctness] +claim nsl3,R Niagree_r3 - Fail [at least 1 attack] +claim nsl3,R Nisynch_r4 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3-updated-both.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..b0c4054 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.out @@ -0,0 +1,8 @@ +claim nsl3,I Secret_i1 ni Ok [proof of correctness] +claim nsl3,I Secret_i2 nr Ok [proof of correctness] +claim nsl3,I Niagree_i3 - Ok [proof of correctness] +claim nsl3,I Nisynch_i4 - Ok [proof of correctness] +claim nsl3,R Secret_r1 ni Ok [proof of correctness] +claim nsl3,R Secret_r2 nr Ok [proof of correctness] +claim nsl3,R Niagree_r3 - Ok [proof of correctness] +claim nsl3,R Nisynch_r4 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-Demo-nsl3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out new file mode 100644 index 0000000..8254692 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.out @@ -0,0 +1,12 @@ +claim isoiec-9798-2-5,A Commit_A2 (B,Kab,Text5,Text7) Ok [no attack within bounds] +claim isoiec-9798-2-5,A Secret_A3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-5,A Secret_A4 Text5 Ok [no attack within bounds] +claim isoiec-9798-2-5,A Secret_A5 Text7 Ok [no attack within bounds] +claim isoiec-9798-2-5,A Alive_A6 - Ok [no attack within bounds] +claim isoiec-9798-2-5,A Weakagree_A7 - Ok [no attack within bounds] +claim isoiec-9798-2-5,B Commit_B2 (A,Kab,Text5) Ok [no attack within bounds] +claim isoiec-9798-2-5,B Secret_B3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-5,B Secret_B4 Text5 Ok [no attack within bounds] +claim isoiec-9798-2-5,B Secret_B5 Text7 Ok [no attack within bounds] +claim isoiec-9798-2-5,B Alive_B6 - Ok [no attack within bounds] +claim isoiec-9798-2-5,B Weakagree_B7 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time new file mode 100644 index 0000000..711e64e --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso25-tag.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +4 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err new file mode 100644 index 0000000..d3b1ed1 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +warning: protocol @keysymm26 has empty role definitions for the roles: [B, P] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out new file mode 100644 index 0000000..843770a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.out @@ -0,0 +1,12 @@ +claim isoiec-9798-2-6-tag,A Commit_A2 (B,Kab,Text6,Text8) Fail [at least 2 attacks] +claim isoiec-9798-2-6-tag,A Secret_A3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-6-tag,A Secret_A4 Text6 Ok [no attack within bounds] +claim isoiec-9798-2-6-tag,A Secret_A5 Text8 Ok [no attack within bounds] +claim isoiec-9798-2-6-tag,A Alive_A6 - Fail [at least 2 attacks] +claim isoiec-9798-2-6-tag,A Weakagree_A7 - Fail [at least 2 attacks] +claim isoiec-9798-2-6-tag,B Commit_B2 (A,Kab,Text6) Fail [at least 2 attacks] +claim isoiec-9798-2-6-tag,B Secret_B3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-6-tag,B Secret_B4 Text6 Ok [no attack within bounds] +claim isoiec-9798-2-6-tag,B Secret_B5 Text8 Ok [no attack within bounds] +claim isoiec-9798-2-6-tag,B Alive_B6 - Fail [at least 2 attacks] +claim isoiec-9798-2-6-tag,B Weakagree_B7 - Fail [at least 2 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df42412 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-iso26-tag.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +35 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..c581d3a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-2-1-udkey,B Commit_B1 (A,TNA,Text1) Ok [no attack within bounds] +claim isoiec-9798-2-1-udkey,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-2-1-udkey,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..0c647d4 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-2-1,B Commit_B1 (A,TNA,Text1) Ok [no attack within bounds] +claim isoiec-9798-2-1,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-2-1,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..99a8dcd --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-2-2-udkey,B Commit_B1 (A,RB,Text2) Ok [no attack within bounds] +claim isoiec-9798-2-2-udkey,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-2-2-udkey,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..86a6e87 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-2-2,B Commit_B1 (A,RB,Text2) Ok [no attack within bounds] +claim isoiec-9798-2-2,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-2-2,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..1dd1c33 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-2-3-udkey,A Commit_A2 (B,TNB,Text3) Fail [at least 1 attack] +claim isoiec-9798-2-3-udkey,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-2-3-udkey,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-2-3-udkey,B Commit_B2 (A,TNA,Text1) Fail [at least 3 attacks] +claim isoiec-9798-2-3-udkey,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-2-3-udkey,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..a3905d1 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-2-3,A Commit_A2 (B,TNB,Text3) Fail [at least 1 attack] +claim isoiec-9798-2-3,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-2-3,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-2-3,B Commit_B2 (A,TNA,Text1) Fail [at least 4 attacks] +claim isoiec-9798-2-3,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-2-3,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..68d5a72 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-2-4-udkey,A Commit_A2 (B,RA,RB,Text2,Text4) Ok [no attack within bounds] +claim isoiec-9798-2-4-udkey,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-2-4-udkey,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-2-4-udkey,B Commit_B2 (A,RA,RB,Text2) Ok [no attack within bounds] +claim isoiec-9798-2-4-udkey,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-2-4-udkey,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out new file mode 100644 index 0000000..7b19e80 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-2-4,A Commit_A2 (B,RA,RB,Text2,Text4) Ok [no attack within bounds] +claim isoiec-9798-2-4,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-2-4,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-2-4,B Commit_B2 (A,RA,RB,Text2) Ok [no attack within bounds] +claim isoiec-9798-2-4,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-2-4,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-4.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e45b99d --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +warning: protocol @keysymm25 has empty role definitions for the roles: [B, P] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out new file mode 100644 index 0000000..69b82f2 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.out @@ -0,0 +1,12 @@ +claim isoiec-9798-2-5,A Commit_A2 (B,Kab,Text5,Text7) Fail [at least 3 attacks] +claim isoiec-9798-2-5,A Secret_A3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-5,A Secret_A4 Text5 Ok [no attack within bounds] +claim isoiec-9798-2-5,A Secret_A5 Text7 Ok [no attack within bounds] +claim isoiec-9798-2-5,A Alive_A6 - Fail [at least 3 attacks] +claim isoiec-9798-2-5,A Weakagree_A7 - Fail [at least 3 attacks] +claim isoiec-9798-2-5,B Commit_B2 (A,Kab,Text5) Fail [at least 5 attacks] +claim isoiec-9798-2-5,B Secret_B3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-5,B Secret_B4 Text5 Ok [no attack within bounds] time=60 +claim isoiec-9798-2-5,B Secret_B5 Text7 Ok [no attack within bounds] time=60 +claim isoiec-9798-2-5,B Alive_B6 - Ok [does not occur] time=60 +claim isoiec-9798-2-5,B Weakagree_B7 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-5.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err new file mode 100644 index 0000000..d3b1ed1 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +warning: protocol @keysymm26 has empty role definitions for the roles: [B, P] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out new file mode 100644 index 0000000..76e99d2 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.out @@ -0,0 +1,12 @@ +claim isoiec-9798-2-6,A Commit_A2 (B,Kab,Text6,Text8) Fail [at least 2 attacks] +claim isoiec-9798-2-6,A Secret_A3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-6,A Secret_A4 Text6 Ok [no attack within bounds] +claim isoiec-9798-2-6,A Secret_A5 Text8 Ok [no attack within bounds] +claim isoiec-9798-2-6,A Alive_A6 - Fail [at least 2 attacks] +claim isoiec-9798-2-6,A Weakagree_A7 - Fail [at least 2 attacks] +claim isoiec-9798-2-6,B Commit_B2 (A,Kab,Text6) Fail [at least 2 attacks] +claim isoiec-9798-2-6,B Secret_B3 Kab Ok [no attack within bounds] +claim isoiec-9798-2-6,B Secret_B4 Text6 Ok [no attack within bounds] +claim isoiec-9798-2-6,B Secret_B5 Text8 Ok [no attack within bounds] time=60 +claim isoiec-9798-2-6,B Alive_B6 - Ok [does not occur] time=60 +claim isoiec-9798-2-6,B Weakagree_B7 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-2-6.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..d2e10db --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-3-1,B Commit_B1 (A,TNA,Text1) Ok [no attack within bounds] +claim isoiec-9798-3-1,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-3-1,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..b8a62d4 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-3-2,B Commit_B1 (A,Ra,Rb,Text2) Ok [no attack within bounds] +claim isoiec-9798-3-2,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-3-2,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..b9573d2 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-3-3,A Commit_A2 (B,TNB,Text3) Fail [at least 6 attacks] +claim isoiec-9798-3-3,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-3-3,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-3-3,B Commit_B2 (A,TNA,Text1) Fail [at least 3 attacks] +claim isoiec-9798-3-3,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-3-3,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out new file mode 100644 index 0000000..058730e --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-3-4,A Commit_A2 (B,RA,RB,Text2,Text4) Ok [no attack within bounds] +claim isoiec-9798-3-4,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-3-4,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-3-4,B Commit_B2 (A,RA,RB,Text2) Ok [no attack within bounds] +claim isoiec-9798-3-4,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-3-4,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-4.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out new file mode 100644 index 0000000..4d2a79b --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-3-5,A Commit_A2 (B,RA,RB,Text5) Ok [no attack within bounds] +claim isoiec-9798-3-5,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-3-5,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-3-5,B Commit_B2 (A,RA,RB,Text3,Text5) Ok [no attack within bounds] +claim isoiec-9798-3-5,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-3-5,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-5.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..571c456 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim isoiec-9798-3-6-1,A Commit_A2 (B,Ra,Rb,Text2) Ok [no attack within bounds] time=60 +claim isoiec-9798-3-6-1,A Alive_A3 - Ok [does not occur] time=60 +claim isoiec-9798-3-6-1,B Commit_B2 (A,Ra,Rb,Text8) Ok [does not occur] time=60 +claim isoiec-9798-3-6-1,B Alive_B3 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..3ff3b13 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim isoiec-9798-3-6-2,A Commit_A2 (B,Ra,Rb,Text2) Ok [no attack within bounds] +claim isoiec-9798-3-6-2,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-3-6-2,B Commit_B2 (A,Ra,Rb,Text8) Ok [no attack within bounds] +claim isoiec-9798-3-6-2,B Alive_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..7fda290 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-6-2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +9 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..3802f29 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim isoiec-9798-3-7-1,A Commit_A2 (B,Ra,Rb,Text8) Ok [no attack within bounds] time=60 +claim isoiec-9798-3-7-1,A Alive_A3 - Ok [does not occur] time=60 +claim isoiec-9798-3-7-1,B Commit_B2 (A,Ra,Rb,Text6) Ok [does not occur] time=60 +claim isoiec-9798-3-7-1,B Alive_B3 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..59c72eb --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim isoiec-9798-3-7-2,A Commit_A2 (B,Ra,Rb,Text8) Ok [no attack within bounds] +claim isoiec-9798-3-7-2,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-3-7-2,B Commit_B2 (A,Ra,Rb,Text6) Ok [no attack within bounds] +claim isoiec-9798-3-7-2,B Alive_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..20932a6 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-3-7-2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +7 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..103d248 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-4-1-udkey,B Commit_B1 (A,TNA,Text1) Ok [no attack within bounds] +claim isoiec-9798-4-1-udkey,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-4-1-udkey,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..a1acda1 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +warning: protocol @keysymm-41 has empty role definitions for the roles: [B] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..235bc6b --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-4-1,B Commit_B1 (A,TNA,Text1) Ok [no attack within bounds] +claim isoiec-9798-4-1,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-4-1,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..1d8fc28 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-4-2-udkey,B Commit_B1 (A,Rb,Text2) Ok [no attack within bounds] +claim isoiec-9798-4-2-udkey,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-4-2-udkey,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..7d6a765 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +warning: protocol @keysymm-42 has empty role definitions for the roles: [B] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..242ec1a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim isoiec-9798-4-2,B Commit_B1 (A,Rb,Text2) Ok [no attack within bounds] +claim isoiec-9798-4-2,B Alive_B2 - Ok [no attack within bounds] +claim isoiec-9798-4-2,B Weakagree_B3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..9680050 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-4-3-udkey,A Commit_A2 (B,TNb,Text3) Fail [at least 1 attack] +claim isoiec-9798-4-3-udkey,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-4-3-udkey,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-4-3-udkey,B Commit_B2 (A,TNa,Text1) Fail [at least 3 attacks] +claim isoiec-9798-4-3-udkey,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-4-3-udkey,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..bf87b0b --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +warning: protocol @keysymm-43 has empty role definitions for the roles: [B] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..3e2a2f7 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-4-3,A Commit_A2 (B,TNb,Text3) Fail [at least 1 attack] +claim isoiec-9798-4-3,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-4-3,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-4-3,B Commit_B2 (A,TNa,Text1) Fail [at least 4 attacks] +claim isoiec-9798-4-3,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-4-3,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out new file mode 100644 index 0000000..e131a97 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-4-4-udkey,A Commit_A2 (B,Ra,Rb,Text2,Text4) Ok [no attack within bounds] +claim isoiec-9798-4-4-udkey,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-4-4-udkey,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-4-4-udkey,B Commit_B2 (A,Ra,Rb,Text2) Ok [no attack within bounds] +claim isoiec-9798-4-4-udkey,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-4-4-udkey,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4-udkey.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out new file mode 100644 index 0000000..4dd3a5a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim isoiec-9798-4-4,A Commit_A2 (B,Ra,Rb,Text2,Text4) Ok [no attack within bounds] +claim isoiec-9798-4-4,A Alive_A3 - Ok [no attack within bounds] +claim isoiec-9798-4-4,A Weakagree_A4 - Ok [no attack within bounds] +claim isoiec-9798-4-4,B Commit_B2 (A,Ra,Rb,Text2) Ok [no attack within bounds] +claim isoiec-9798-4-4,B Alive_B3 - Ok [no attack within bounds] +claim isoiec-9798-4-4,B Weakagree_B4 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-isoiec-9798-4-4.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ISO-9798-sasl.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out new file mode 100644 index 0000000..32a0a19 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim andrew-Concrete,I Secret_I1 kir Ok [no attack within bounds] +claim andrew-Concrete,I Nisynch_I2 - Fail [at least 1 attack] +claim andrew-Concrete,R Secret_R1 kir Ok [no attack within bounds] +claim andrew-Concrete,R Nisynch_R2 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban-concrete.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out new file mode 100644 index 0000000..2011c4f --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.out @@ -0,0 +1,8 @@ +claim andrew-Ban,I Nisynch_I1 - Ok [proof of correctness] +claim andrew-Ban,I Niagree_I2 - Ok [proof of correctness] +claim andrew-Ban,I Secret_I3 kir Ok [proof of correctness] +claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness] +claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness] +claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness] +claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness] +claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew-ban.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out new file mode 100644 index 0000000..91fc492 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness] +claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness] +claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness] +claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew-lowe-ban.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out new file mode 100644 index 0000000..ec24c37 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim andrew,I Secret_I1 kir Ok [no attack within bounds] +claim andrew,I Nisynch_I2 - Fail [at least 1 attack] +claim andrew,I Niagree_I3 - Fail [at least 1 attack] +claim andrew,R Secret_R1 kir Ok [no attack within bounds] +claim andrew,R Nisynch_R2 - Ok [no attack within bounds] +claim andrew,R Niagree_R3 - Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time new file mode 100644 index 0000000..97d01d7 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-andrew.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +14 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..0fddf90 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out new file mode 100644 index 0000000..710d27e --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-1c.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..bf351ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness] +claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness] +claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness] +claim ccitt509-3,R Nisynch_R1 - Fail [at least 3 attacks] +claim ccitt509-3,R Secret_R2 Ya Ok [no attack within bounds] +claim ccitt509-3,R Secret_R3 Yb Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..c711226 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.out @@ -0,0 +1,2 @@ +claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness] +claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-ccitt509-ban3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out new file mode 100644 index 0000000..3ea7e70 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim denningSacco-Lowe,I Niagree_I1 - Ok [no attack within bounds] +claim denningSacco-Lowe,I Nisynch_I2 - Fail [at least 1 attack] +claim denningSacco-Lowe,I SKR_I3 Kir Ok [no attack within bounds] +claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds] +claim denningSacco-Lowe,R Nisynch_R2 - Fail [at least 1 attack] +claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco-lowe.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out new file mode 100644 index 0000000..5f53683 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim denningSacco,I Niagree_I1 - Ok [no attack within bounds] +claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack] +claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds] +claim denningSacco,R Niagree_R1 - Ok [no attack within bounds] +claim denningSacco,R Nisynch_R2 - Fail [at least 1 attack] +claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-denning-sacco.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..f42247a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim kaochow-2,I Nisynch_I1 - Fail [at least 2 attacks] +claim kaochow-2,I Niagree_I2 - Fail [at least 2 attacks] +claim kaochow-2,I Secret_I3 kir Ok [no attack within bounds] +claim kaochow-2,R Nisynch_R1 - Fail [at least 2 attacks] +claim kaochow-2,R Niagree_R2 - Fail [at least 2 attacks] +claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..4674dbd --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +5 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..f3cf440 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim kaochow-3,I Nisynch_I1 - Fail [at least 2 attacks] +claim kaochow-3,I Niagree_I2 - Fail [at least 2 attacks] +claim kaochow-3,I Secret_I3 kir Ok [no attack within bounds] +claim kaochow-3,R Nisynch_R1 - Fail [at least 2 attacks] +claim kaochow-3,R Niagree_R2 - Fail [at least 2 attacks] +claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-kaochow-v3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out new file mode 100644 index 0000000..5e05c55 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim kaochow,I Nisynch_I1 - Fail [at least 2 attacks] +claim kaochow,I Niagree_I2 - Fail [at least 2 attacks] +claim kaochow,I Secret_I3 kir Ok [no attack within bounds] +claim kaochow,R Nisynch_R1 - Fail [at least 2 attacks] +claim kaochow,R Niagree_R2 - Fail [at least 2 attacks] +claim kaochow,R Secret_R3 kir Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time new file mode 100644 index 0000000..a4bc84c --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-kaochow.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +2 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out new file mode 100644 index 0000000..81a7e6f --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [no attack within bounds] +claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [no attack within bounds] +claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks] +claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [no attack within bounds] +claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [no attack within bounds] +claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time new file mode 100644 index 0000000..37da462 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-lowe.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +23 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out new file mode 100644 index 0000000..38f78d0 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds] +claim needhamschroedersk-amend,I Nisynch_I3 - Fail [at least 1 attack] +claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds] +claim needhamschroedersk-amend,R Nisynch_R3 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time new file mode 100644 index 0000000..a4bc84c --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder-sk-amend.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +2 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out new file mode 100644 index 0000000..d8d506e --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim needhamschroederpk,I Secret_I1 Ni Ok [no attack within bounds] +claim needhamschroederpk,I Secret_I2 Nr Ok [no attack within bounds] +claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks] +claim needhamschroederpk,R Secret_R1 Nr Fail [at least 7 attacks] +claim needhamschroederpk,R Secret_R2 Ni Fail [at least 7 attacks] +claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time new file mode 100644 index 0000000..27fb100 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-needham-schroeder.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +28 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err new file mode 100644 index 0000000..89b9ed9 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +error: fresh terms [Kir] should be declared inside roles, on line 19. diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.out new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman-hwang.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err new file mode 100644 index 0000000..89b9ed9 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +error: fresh terms [Kir] should be declared inside roles, on line 19. diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.out new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-guttman.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out new file mode 100644 index 0000000..153113f --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim neustub-Hwang,I Secret_I1 Kir Ok [no attack within bounds] time=60 +claim neustub-Hwang,I Niagree_I2 - Ok [does not occur] time=60 +claim neustub-Hwang,I Nisynch_I3 - Ok [does not occur] time=60 +claim neustub-Hwang,R Secret_R1 Kir Ok [no attack within bounds] time=60 +claim neustub-Hwang,R Niagree_R2 - Ok [does not occur] time=60 +claim neustub-Hwang,R Nisynch_R3 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-hwang.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err new file mode 100644 index 0000000..89b9ed9 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +error: fresh terms [Kir] should be declared inside roles, on line 19. diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.out new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub-keycompromise.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e52a51e --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.err @@ -0,0 +1 @@ +error: fresh terms [Kir] should be declared inside roles, on line 16. diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.out new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-neumannstub.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out new file mode 100644 index 0000000..15e3371 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim smartright,R Nisynch_R1 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-smartright.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out new file mode 100644 index 0000000..cdd6305 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim spliceAS-HC,I Secret_7 N2 Ok [no attack within bounds] time=60 +claim spliceAS-HC,I Niagree_9 - Ok [does not occur] time=60 +claim spliceAS-HC,I Nisynch_10 - Ok [does not occur] time=60 +claim spliceAS-HC,R Secret_8 N2 Ok [no attack within bounds] time=60 +claim spliceAS-HC,R Niagree_11 - Ok [does not occur] time=60 +claim spliceAS-HC,R Nisynch_12 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-splice-as-hc.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out new file mode 100644 index 0000000..a8474fb --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.out @@ -0,0 +1,6 @@ +claim spliceAS,I Secret_7 N2 Ok [no attack within bounds] time=60 +claim spliceAS,I Niagree_9 - Ok [does not occur] time=60 +claim spliceAS,I Nisynch_10 - Ok [does not occur] time=60 +claim spliceAS,R Secret_8 N2 Ok [no attack within bounds] time=60 +claim spliceAS,R Niagree_11 - Ok [does not occur] time=60 +claim spliceAS,R Nisynch_12 - Ok [does not occur] time=60 diff --git a/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time new file mode 100644 index 0000000..df21598 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-splice-as.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +60 diff --git a/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out new file mode 100644 index 0000000..a6a11dd --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim tmn,I Secret_I1 Kr Fail [at least 4 attacks] +claim tmn,I Nisynch_I2 - Fail [at least 2 attacks] +claim tmn,R Secret_R1 Kr Fail [at least 2 attacks] +claim tmn,R Nisynch_R2 - Fail [exactly 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-tmn.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out new file mode 100644 index 0000000..1fb959d --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds] +claim wmf-Lowe,I Nisynch_I2 - Fail [at least 3 attacks] +claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds] +claim wmf-Lowe,R Nisynch_R2 - Fail [at least 3 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-wmf-lowe.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out new file mode 100644 index 0000000..039a65a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.out @@ -0,0 +1,3 @@ +claim wmf,I Secret_I1 Kir Ok [no attack within bounds] +claim wmf,R Secret_R1 Kir Ok [no attack within bounds] +claim wmf,R Nisynch_R2 - Fail [at least 3 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-wmf.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out new file mode 100644 index 0000000..3ac7ab5 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-1.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out new file mode 100644 index 0000000..63b6634 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-2.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..756742c --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out new file mode 100644 index 0000000..eb93f90 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi-f.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out new file mode 100644 index 0000000..233b5fc --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.out @@ -0,0 +1 @@ +claim woolamPi,R Nisynch_R1 - Fail [at least 4 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam-pi.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out new file mode 100644 index 0000000..f34f204 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim woolam,I Secret_I1 Kir Ok [no attack within bounds] +claim woolam,I Nisynch_I2 - Fail [at least 2 attacks] +claim woolam,R Secret_R1 Kir Ok [no attack within bounds] +claim woolam,R Nisynch_R2 - Fail [at least 2 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time new file mode 100644 index 0000000..b449a72 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-woo-lam.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +36 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-ban-paulson-modified.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out new file mode 100644 index 0000000..d2006f0 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim yahalom-BAN,I Secret_I1 Kir Ok [no attack within bounds] +claim yahalom-BAN,I Nisynch_I2 - Fail [at least 1 attack] +claim yahalom-BAN,R Secret_R1 Kir Ok [no attack within bounds] +claim yahalom-BAN,R Nisynch_R2 - Fail [at least 2 attacks] diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-ban.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out new file mode 100644 index 0000000..1d1be5a --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness] +claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness] +claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness] +claim yahalom-Lowe,R Nisynch_R2 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-lowe.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out new file mode 100644 index 0000000..ea12ec0 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim yahalom-Paulson,I Secret_I1 Kir Ok [no attack within bounds] +claim yahalom-Paulson,I Nisynch_I2 - Fail [at least 1 attack] +claim yahalom-Paulson,R Secret_R1 Kir Ok [no attack within bounds] +claim yahalom-Paulson,R Nisynch_R2 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom-paulson.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out new file mode 100644 index 0000000..5606f67 --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.out @@ -0,0 +1,4 @@ +claim yahalom,I Secret_I1 Kir Ok [no attack within bounds] +claim yahalom,R Secret_R1 Kir Ok [no attack within bounds] +claim yahalom,S Secret_S1 Ni Fail [at least 1 attack] +claim yahalom,S Secret_S2 Nr Ok [no attack within bounds] diff --git a/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-Protocols-yahalom.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out new file mode 100644 index 0000000..fa4ead8 --- /dev/null +++ b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.out @@ -0,0 +1,16 @@ +claim nsl3,I Secret_i1 ni Fail [at least 2 attacks] +claim nsl3,I Secret_i2 nr Fail [at least 1 attack] +claim nsl3,I Niagree_i3 - Fail [at least 1 attack] +claim nsl3,I Nisynch_i4 - Fail [at least 1 attack] +claim nsl3,R Secret_r1 ni Fail [at least 2 attacks] +claim nsl3,R Secret_r2 nr Ok [proof of correctness] +claim nsl3,R Niagree_r3 - Fail [at least 1 attack] +claim nsl3,R Nisynch_r4 - Fail [at least 1 attack] +claim nsl3-broken,I Secret_i1 ni Fail [at least 1 attack] +claim nsl3-broken,I Secret_i2 nr Fail [at least 1 attack] +claim nsl3-broken,I Niagree_i3 - Fail [at least 1 attack] +claim nsl3-broken,I Nisynch_i4 - Fail [at least 1 attack] +claim nsl3-broken,R Secret_r1 ni Fail [at least 1 attack] +claim nsl3-broken,R Secret_r2 nr Ok [proof of correctness] +claim nsl3-broken,R Niagree_r3 - Fail [at least 1 attack] +claim nsl3-broken,R Nisynch_r4 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-mpa.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out new file mode 100644 index 0000000..39d339c --- /dev/null +++ b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.out @@ -0,0 +1,8 @@ +claim nsl3-broken,I Secret_i1 ni Fail [at least 1 attack] +claim nsl3-broken,I Secret_i2 nr Fail [at least 1 attack] +claim nsl3-broken,I Niagree_i3 - Fail [at least 1 attack] +claim nsl3-broken,I Nisynch_i4 - Fail [at least 1 attack] +claim nsl3-broken,R Secret_r1 ni Fail [at least 1 attack] +claim nsl3-broken,R Secret_r2 nr Ok [proof of correctness] +claim nsl3-broken,R Niagree_r3 - Ok [proof of correctness] +claim nsl3-broken,R Nisynch_r4 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-nsl3-broken.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..b61e892 --- /dev/null +++ b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.out @@ -0,0 +1,14 @@ +claim nsl3,I Secret_I2 ni Ok [proof of correctness] +claim nsl3,I Secret_I3 nr Ok [proof of correctness] +claim nsl3,I Alive_I4 - Ok [proof of correctness] +claim nsl3,I Weakagree_I5 - Ok [proof of correctness] +claim nsl3,I Commit_I6 (R,ni,nr) Ok [proof of correctness] +claim nsl3,I Niagree_I7 - Ok [proof of correctness] +claim nsl3,I Nisynch_I8 - Ok [proof of correctness] +claim nsl3,R Secret_R2 ni Ok [proof of correctness] +claim nsl3,R Secret_R3 nr Ok [proof of correctness] +claim nsl3,R Alive_R4 - Ok [proof of correctness] +claim nsl3,R Weakagree_R5 - Ok [proof of correctness] +claim nsl3,R Commit_R6 (I,ni,nr) Ok [proof of correctness] +claim nsl3,R Niagree_R7 - Ok [proof of correctness] +claim nsl3,R Nisynch_R8 - Ok [proof of correctness] diff --git a/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-gui-nsl3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.err b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.err new file mode 100644 index 0000000..e69de29 diff --git a/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out new file mode 100644 index 0000000..f4d4594 --- /dev/null +++ b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.out @@ -0,0 +1,14 @@ +claim ns3,I Secret_I2 ni Ok [proof of correctness] +claim ns3,I Secret_I3 nr Ok [proof of correctness] +claim ns3,I Alive_I4 - Ok [proof of correctness] +claim ns3,I Weakagree_I5 - Ok [proof of correctness] +claim ns3,I Commit_I6 (R,ni,nr) Ok [proof of correctness] +claim ns3,I Niagree_I7 - Ok [proof of correctness] +claim ns3,I Nisynch_I8 - Ok [proof of correctness] +claim ns3,R Secret_R2 ni Fail [at least 1 attack] +claim ns3,R Secret_R3 nr Fail [at least 1 attack] +claim ns3,R Alive_R4 - Ok [proof of correctness] +claim ns3,R Weakagree_R5 - Fail [at least 1 attack] +claim ns3,R Commit_R6 (I,ni,nr) Fail [at least 1 attack] +claim ns3,R Niagree_R7 - Fail [at least 1 attack] +claim ns3,R Nisynch_R8 - Fail [at least 1 attack] diff --git a/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time new file mode 100644 index 0000000..80f32ca --- /dev/null +++ b/src/regression-tests/results/test-src-ns3.spdl --timer=60 --plain.time @@ -0,0 +1,2 @@ +Passed wall time in seconds: +0 diff --git a/src/regression-tests/tests.txt b/src/regression-tests/tests.txt new file mode 100644 index 0000000..65ed360 --- /dev/null +++ b/src/regression-tests/tests.txt @@ -0,0 +1,316 @@ +# Test file for scyther +# +# Essentially contains argument lines for the tool, where the first +# argument is the file name, relative to the base directory of the +# repository. +# +# For each, we then record the output. +# +# Empty lines or lines starting with '%' or '#' are not considered. +# Lines with '=' set the "global" concatenation. +# += --timer=60 --plain +# testing/bke.spdl +# testing/bke-one.spdl +# testing/ibe.spdl +# testing/otwayrees.spdl +# testing/ns-symmetric.spdl +# testing/bkepk-ce.spdl +# testing/unknown2.spdl +# testing/splice-as.spdl +# testing/nst2.spdl +# testing/boyd.spdl +testing/ksl.spdl -r3 +# testing/andrew-ban.spdl +# testing/tmn.spdl +# testing/carkey-broken-limited.spdl +# testing/bunava-1-4.spdl +# testing/soph.spdl +# testing/kaochow-v2.spdl +# testing/2r890-ex3-a.spdl +# testing/tmn-Gijs.spdl +# testing/nsl3-nisynch-rep.spdl +# testing/ns3.spdl +# testing/yahalom-paulson.spdl +# testing/localclaims-seq1.spdl +# testing/bke-variation.spdl +# testing/localclaims.spdl +# testing/carkey-ni2.spdl +# testing/broken1.spdl +# testing/gong-nonce-b.spdl +# testing/isoiec11770-2-13.spdl +# testing/ccitt509-ban.spdl +# testing/bunava-2-3.spdl +# testing/wmf-brutus.spdl +# testing/five-run-bound.spdl +# testing/tls/tls-BM-1.spdl +# testing/tls/tls-HSDDM05-2.spdl +# testing/tls/tls-HSDDM05-fix.spdl +# testing/tls/tls-HSDDM05.spdl +# testing/tls/tls-paulson.spdl +# testing/tls/tls-paulson-avispa.spdl +# testing/ns-symmetric-amended.spdl +# testing/bunava-2-4.spdl +# testing/soph-keyexch.spdl +# testing/gong-nonce.spdl +# testing/splice-as-hc.spdl +# testing/onetrace.spdl +# testing/woolam-pi-f.spdl +# testing/nst1.spdl +# testing/nsl3.spdl +# testing/andrew-lowe-ban.spdl +# testing/kaochow-palm.spdl +# testing/yahalom-lowe.spdl +# testing/speedtest.spdl +# testing/carkey-ni.spdl +# testing/woolam-cmv.spdl +# testing/compositionality-examples/th-1.spdl +# testing/compositionality-examples/th-1seq2-rename-ni.spdl +# testing/compositionality-examples/th-1seq2-rename-nr.spdl +# testing/compositionality-examples/th-2.spdl +# testing/compositionality-examples/th-1seq2.spdl +# testing/compositionality-examples/th-1par2.spdl +# testing/samasc-broken.spdl +# testing/kaochow.spdl +# testing/splice-as-hc-cj.spdl +# testing/2r890-ex3-b.spdl +# testing/carkey-broken.spdl +# testing/denning-sacco-shared.spdl +# testing/kaochow-v3.spdl +# testing/fourway-HSDDM05.spdl +# testing/bke-broken.spdl +# testing/simplest.spdl +# testing/kerberos-rddm.spdl +# testing/f5.spdl +# testing/yahalom-ban.spdl +# testing/ns3-brutus.spdl +# testing/ibe-ns.spdl +# testing/boyd-nsl-fix.spdl +# testing/localclaims-breaker.spdl +# testing/helloworld.spdl +# testing/bkepk-ce2.spdl +# testing/bunava-1-3.spdl +# testing/athena-breaker.spdl +# testing/f4.spdl +# gui/yhl.spdl +# gui/Protocols-reachable/reach_yahalom-lowe.spdl +# gui/Protocols-reachable/reach_woo-lam-pi-f.spdl +# gui/Protocols-reachable/reach_splice-as.spdl +# gui/Protocols-reachable/reach_kaochow-v2.spdl +# gui/Protocols-reachable/reach_wmf-lowe.spdl +# gui/Protocols-reachable/reach_woo-lam-pi-1.spdl +# gui/Protocols-reachable/reach_needham-schroeder-sk.spdl +# gui/Protocols-reachable/reach_neumannstub-guttman.spdl +# gui/Protocols-reachable/reach_splice-as-hc.spdl +# gui/Protocols-reachable/reach_tmn.spdl +# gui/Protocols-reachable/reach_needham-schroeder-lowe.spdl +# gui/Protocols-reachable/reach_woo-lam-pi.spdl +# gui/Protocols-reachable/reach_yahalom-ban-paulson.spdl +# gui/Protocols-reachable/reach_ccitt509-3.spdl +# gui/Protocols-reachable/reach_woo-lam-pi-2.spdl +# gui/Protocols-reachable/reach_kaochow-v3.spdl +# gui/Protocols-reachable/reach_neumannstub-guttman-hwang.spdl +# gui/Protocols-reachable/reach_denning-sacco.spdl +# gui/Protocols-reachable/reach_yahalom.spdl +# gui/Protocols-reachable/reach_kaochow.spdl +# gui/Protocols-reachable/reach_andrew-lowe-ban.spdl +# gui/Protocols-reachable/reach_woo-lam.spdl +# gui/Protocols-reachable/reach_neumannstub-keycompromise.spdl +# gui/Protocols-reachable/reach_wmf.spdl +# gui/Protocols-reachable/reach_ccitt509-1c.spdl +# gui/Protocols-reachable/reach_ccitt509-ban3.spdl +# gui/Protocols-reachable/reach_neumannstub-hwang.spdl +# gui/Protocols-reachable/reach_needham-schroeder-sk-amend.spdl +# gui/Protocols-reachable/reach_splice-as-cj.spdl +# gui/Protocols-reachable/reach_BKE.spdl +# gui/Protocols-reachable/reach_andrew-ban-concrete.spdl +# gui/Protocols-reachable/reach_andrew-ban.spdl +# gui/Protocols-reachable/reach_otwayrees.spdl +# gui/Protocols-reachable/reach_andrew.spdl +# gui/Protocols-reachable/reach_denning-sacco-lowe.spdl +# gui/Protocols-reachable/reach_yahalom-paulson.spdl +# gui/Protocols-reachable/reach_neumannstub.spdl +# gui/Protocols-reachable/reach_TLS-Paulson.spdl +# gui/Protocols-reachable/reach_yahalom-ban.spdl +# gui/Protocols-reachable/reach_ccitt509-1.spdl +# gui/Protocols-reachable/reach_needham-schroeder.spdl +# gui/Protocols-reachable/reach_smartright.spdl +# gui/Protocols-reachable/reach_woo-lam-pi-3.spdl +# gui/ns3.spdl +# gui/nsl3-ibake.spdl +# gui/Protocols/otwayrees.spdl +# gui/Protocols/splice-as-cj.spdl +# gui/Protocols/MultiProtocolAttacks/otwayrees.spdl +# gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl +# gui/Protocols/MultiProtocolAttacks/splice-as.spdl +# gui/Protocols/MultiProtocolAttacks/boyd.spdl +# gui/Protocols/MultiProtocolAttacks/ksl.spdl +# gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl +# gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl +# gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl +# gui/Protocols/MultiProtocolAttacks/tmn.spdl +# gui/Protocols/MultiProtocolAttacks/soph.spdl +# gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl +# gui/Protocols/MultiProtocolAttacks/ns3.spdl +# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl +# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl +# gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl +# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl +# gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl +# gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl +# gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl +# gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl +# gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl +# gui/Protocols/MultiProtocolAttacks/wmf.spdl +# gui/Protocols/MultiProtocolAttacks/yahalom.spdl +# gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl +# gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl +# gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl +# gui/Protocols/MultiProtocolAttacks/BKE.spdl +# gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl +# gui/Protocols/MultiProtocolAttacks/woo-lam.spdl +# gui/Protocols/MultiProtocolAttacks/nsl3.spdl +# gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl +# gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl +# gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl +# gui/Protocols/MultiProtocolAttacks/kaochow.spdl +# gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl +# gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl +# gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl +gui/Protocols/splice-as.spdl +gui/Protocols/ksl.spdl -r3 +gui/Protocols/andrew-ban.spdl +gui/Protocols/denning-sacco-lowe.spdl +gui/Protocols/needham-schroeder-sk-amend.spdl +gui/Protocols/tmn.spdl +gui/Protocols/andrew.spdl +gui/Protocols/neumannstub-guttman.spdl +gui/Protocols/kaochow-v2.spdl +gui/Protocols/ccitt509-1.spdl +gui/Protocols/ccitt509-1c.spdl +gui/Protocols/yahalom-paulson.spdl +gui/Protocols/woo-lam-pi-2.spdl +gui/Protocols/Demo/ns3.spdl +gui/Protocols/Demo/nsl3-updated-both.spdl +gui/Protocols/Demo/nsl3.spdl +gui/Protocols/Demo/nsl3-broken.spdl +gui/Protocols/woo-lam-pi-3.spdl +gui/Protocols/woo-lam-pi.spdl +gui/Protocols/needham-schroeder-lowe.spdl +gui/Protocols/woo-lam-pi-1.spdl +gui/Protocols/ccitt509-ban3.spdl +gui/Protocols/denning-sacco.spdl +gui/Protocols/wmf-lowe.spdl +gui/Protocols/wmf.spdl +# gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl +# gui/Protocols/IEEE-WIMAX/pkmv2rsa-noid.spdl +# gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl +# gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl +# gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl +# gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl +# gui/Protocols/IEEE-WIMAX/pqr.spdl +gui/Protocols/neumannstub-hwang.spdl +gui/Protocols/yahalom.spdl +gui/Protocols/splice-as-hc.spdl +# gui/Protocols/needham-schroeder-sk.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl +gui/Protocols/ISO-9798/iso26-tag.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl +gui/Protocols/ISO-9798/iso25-tag.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl +gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl +gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl +gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl +gui/Protocols/neumannstub.spdl +gui/Protocols/neumannstub-guttman-hwang.spdl +gui/Protocols/woo-lam.spdl +gui/Protocols/andrew-lowe-ban.spdl +gui/Protocols/andrew-ban-concrete.spdl +gui/Protocols/yahalom-lowe.spdl +gui/Protocols/needham-schroeder.spdl +gui/Protocols/kaochow.spdl +gui/Protocols/ccitt509-3.spdl +gui/Protocols/ksl-lowe.spdl -r3 +gui/Protocols/woo-lam-pi-f.spdl +gui/Protocols/smartright.spdl +gui/Protocols/kaochow-v3.spdl +gui/Protocols/yahalom-ban.spdl +gui/Protocols/neumannstub-keycompromise.spdl +# gui/Protocols/IKE/ikev1-pk2-m.spdl +# gui/Protocols/IKE/ikev1-quick-nopfs.spdl +# gui/Protocols/IKE/ikev2-sig-child2-composed.spdl +# gui/Protocols/IKE/ikev1-pk2-a2.spdl +# gui/Protocols/IKE/ikev1-psk-a.spdl +# gui/Protocols/IKE/sts-mac.spdl +# gui/Protocols/IKE/ikev2-eap2.spdl +# gui/Protocols/IKE/oakley-a.spdl +# gui/Protocols/IKE/jfkr.spdl +# gui/Protocols/IKE/jfki-core.spdl +# gui/Protocols/IKE/ikev2-child-nopfs.spdl +# gui/Protocols/IKE/ikev1-psk-m-perlman.spdl +# gui/Protocols/IKE/ikev2-sig-child-composed.spdl +# gui/Protocols/IKE/ikev2-sig-child2.spdl +# gui/Protocols/IKE/ikev2-mac2.spdl +# gui/Protocols/IKE/oakley-c.spdl +# gui/Protocols/IKE/ikev1-pk-a12.spdl +# gui/Protocols/IKE/ikev1-quick.spdl +# gui/Protocols/IKE/sts-main.spdl +# gui/Protocols/IKE/ikev1-quick-noid.spdl +# gui/Protocols/IKE/ikev1-pk-a1.spdl +# gui/Protocols/IKE/ikev2-sigtomac.spdl +# gui/Protocols/IKE/ikev1-pk2-a.spdl +# gui/Protocols/IKE/jfkr-core.spdl +# gui/Protocols/IKE/oakley-alt.spdl +# gui/Protocols/IKE/ikev1-pk-m.spdl +# gui/Protocols/IKE/ikev1-sig-m-perlman.spdl +# gui/Protocols/IKE/ikev1-sig-a-perlman2.spdl +# gui/Protocols/IKE/ikev1-sig-m.spdl +# gui/Protocols/IKE/jfki.spdl +# gui/Protocols/IKE/ikev1-sig-a1.spdl +# gui/Protocols/IKE/skeme-rekey.spdl +# gui/Protocols/IKE/skeme-basic.spdl +# gui/Protocols/IKE/ikev2-sig-child.spdl +# gui/Protocols/IKE/skeme-psk.spdl +# gui/Protocols/IKE/ikev1-pk-a22.spdl +# gui/Protocols/IKE/ikev2-child.spdl +# gui/Protocols/IKE/ikev2-mac.spdl +# gui/Protocols/IKE/ikev2-eap.spdl +# gui/Protocols/IKE/sts-modified.spdl +# gui/Protocols/IKE/ikev1-sig-a-perlman1.spdl +# gui/Protocols/IKE/ikev2-mactosig.spdl +# gui/Protocols/IKE/ikev1-psk-m.spdl +# gui/Protocols/IKE/ikev1-pk-a2.spdl +# gui/Protocols/IKE/ikev2-sig.spdl +# gui/Protocols/IKE/ikev2-sigtomac2.spdl +# gui/Protocols/IKE/ikev1-pk2-m2.spdl +# gui/Protocols/IKE/ikev1-sig-a2.spdl +# gui/Protocols/IKE/ikev2-sig2.spdl +# gui/Protocols/IKE/ikev2-mactosig2.spdl +# gui/Protocols/IKE/ikev1-pk-m2.spdl +gui/nsl3.spdl +gui/mpa.spdl +gui/nsl3-broken.spdl +src/ns3.spdl + +