src/regression-tests: Consistent regression testing.
There is now a script src/regression-tests/regression-test.py that should in the future be the default for running regression tests instead of the ad-hoc approach we are currently using. The goal is to ultimately have more reliable and consistent regression testing. The script takes as input "tests.txt" and tries to perform tests from that. This is effectively a collection of inputs to the scyther-linux binary. The results are writting to the 'results' directory, as test-X.out and test-X.err, where those correspond to stdout and stderr, respectively. Additionally, a measurement of wall-clock time in seconds is written to test-X.time. For now, we are using the timer to ensure all tests terminate. It would be nicer to use a less environment-dependent way of enforcing termination.
This commit is contained in:
Cas Cremers
parent
b92c097b38
commit
4a1898db92
5
src/regression-tests/Makefile
Normal file
5
src/regression-tests/Makefile
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
|
||||
results:
|
||||
./regression-test.py
|
||||
|
||||
.PHONY: results
|
||||
140
src/regression-tests/regression-test.py
Executable file
140
src/regression-tests/regression-test.py
Executable file
|
|
@ -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()
|
||||
|
||||
|
||||
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
4
|
||||
|
|
@ -0,0 +1 @@
|
|||
warning: protocol @keysymm26 has empty role definitions for the roles: [B, P]
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
35
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -0,0 +1 @@
|
|||
warning: protocol @keysymm25 has empty role definitions for the roles: [B, P]
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
60
|
||||
|
|
@ -0,0 +1 @@
|
|||
warning: protocol @keysymm26 has empty role definitions for the roles: [B, P]
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
60
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
60
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
9
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
60
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
7
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -0,0 +1 @@
|
|||
warning: protocol @keysymm-41 has empty role definitions for the roles: [B]
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -0,0 +1 @@
|
|||
warning: protocol @keysymm-42 has empty role definitions for the roles: [B]
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -0,0 +1 @@
|
|||
warning: protocol @keysymm-43 has empty role definitions for the roles: [B]
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
Passed wall time in seconds:
|
||||
0
|
||||
|
|
@ -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]
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user