- Added preliminary results, which will be used in the thesis.

- Modified heuristics test for stuff in the thesis.
This commit is contained in:
ccremers 2006-07-01 10:11:08 +00:00
parent b85d2e2270
commit 3b330d40de
17 changed files with 3866 additions and 36 deletions

View File

@ -60,11 +60,15 @@ def timed(file):
print file, " no time found"
def all():
print "prot\t\t\tclaims\tattacks\tcorrect\tdecided"
for i in range(1,8):
analyze("boundruns%i.txt" % (i),i)
print
for i in range(1,8):
timed("boundtime%i.txt" % (i))
print
for i in range(1,8):
l = []
for k in firstbroken.keys():

32
test/boundanalyze.txt Normal file
View File

@ -0,0 +1,32 @@
prot claims attacks correct decided
[boundruns1.txt] 518 9 15 4.6332046332%
[boundruns2.txt] 518 80 95 33.7837837838%
[boundruns3.txt] 518 220 176 76.4478764479%
[boundruns4.txt] 518 234 214 86.4864864865%
[boundruns5.txt] 518 236 228 89.5752895753%
[boundruns6.txt] 518 236 234 90.7335907336%
[boundruns7.txt] 518 236 234 90.7335907336%
time
boundtime1.txt 0.44
boundtime2.txt 2.26
boundtime3.txt 10.08
boundtime4.txt 37.98
boundtime5.txt 149.73
boundtime6.txt 591.45
boundtime7.txt 590.43
Attack with 1 runs:
['simplest,I,Secret_3', 'woolamPi-1,R,Nisynch_R1', 'tmn,S,Secret_7', 'carkeybrokenlim,R,Nisynch_2', 'localclaims,R,Secret_r1', 'onetrace,I,Secret_4', 'tmn,R,Nisynch_R2', 'woolamPi-2,R,Nisynch_R1', 'woolamPi-3,R,Nisynch_R1']
Attack with 2 runs:
['otwayrees,B,Nisynch_6b', 'wmf-Lowe,R,Nisynch_R2', 'gongnonce,I,Nisynch_8', 'gongnonceb,R,Niagree_13', 'needhamschroedersk,R,Secret_R1', 'ns3,R,Nisynch_r4', 'boydNS,I,Niagree_i3', 'gongnonce,R,Niagree_13', 'bkebroken,R,Secret_5', 'otwayrees,R,Nisynch_R2', 'woolampif,B,Nisynch_7', 'wmf-Lowe,I,Nisynch_I2', 'denningsaccosh,A,Nisynch_5', 'ns3,R,Secret_r1', 'ns3,R,Secret_r2', 'woolampif,B,Niagree_6', 'wmf,R,Nisynch_R2', 'ns3speedtest,R,Secret_5', 'boydNS,I,Nisynch_i4', 'yahalomBan,B,Secret_6', 'boydNS,I,Secret_i2', 'tmn,I,Nisynch_I2', 'bkevariation,R,Niagree_8', 'nsl3rep,I,Nisynch_7', 'gongnonceb,I,Niagree_9', 'tmn,I,Secret_I1', 'andrewLoweBan,I,Niagree_5b', 'carkeybroken,R,Nisynch_2', 'needhamschroedersk,R,Nisynch_R3', 'nsl3rep,R,Nisynch_8', 'kaochow,R,Niagree_R2', 'gongnonce,R,Nisynch_12', 'otwayrees,I,Nisynch_I2', 'tlspaulson-avispa,a,Niagree_9c', 'ns3brutus,R,Secret_5', 'otwayrees,B,Niagree_6a', 'nsl3th3nr,R,Nisynch_r2', 'woolamPi-f,R,Nisynch_R1', 'otwayrees,A,Niagree_5b', 'neustub^Repeat,I,Niagree_I2', 'bkevariation,R,Nisynch_9', 'gongnonceb,I,Nisynch_8', 'tmn,A,Secret_8', 'tmn,A,Secret_5', 'woolamPi,R,Nisynch_R1', 'gongnonce,I,Niagree_9', 'tmn,R,Secret_R1', 'andrewLoweBan,I,Nisynch_5', 'nsl3th3nr,I,Nisynch_i2', 'gongnonceb,R,Nisynch_12', 'tmn,B,Secret_6', 'lcbreakerS1,R,Secret_r0', 'ns3,R,Niagree_r3', 'kaochow,R,Nisynch_R1', 'carkeyni2,R,Nisynch_4', 'yahalomBan,A,Secret_5', 'smartright,R,Nisynch_R1', 'otwayrees,A,Nisynch_5c', 'neustub^Repeat,I,Nisynch_I3', 'ibe,R,Secret_r1', 'kaochow,R,Secret_R3', 'denningSacco,I,Nisynch_I2']
Attack with 3 runs:
['spliceAS,C,Secret_7', 'spliceAS,S,Niagree_11', 'neustub,R,Niagree_R2', 'neustub-Hwang,R,Nisynch_R3', 'kaochowPalm,I,Nisynch_5', 'neustub,I,Niagree_I2', 'ksl,B,Nisynch_B3', 'spliceAS-HC,R,Niagree_11', 'andrew-Concrete,R,Nisynch_R2', 'kaochow,I,Nisynch_5', 'neustub,R,Nisynch_R3', 'spliceAShcCJ,S,Nisynch_12', 'kaochow,I,Niagree_6', 'ksl,I,Nisynch_I3', 'kaochow-2,R,Niagree_R2', 'boyd,R,Niagree_11', 'andrew,I,Secret_I1', 'kaochow-3,I,Nisynch_I1', 'boydNS,R,Nisynch_r4', 'spliceAShc,C,Niagree_9', 'kaochow2,R,Niagree_9', 'woolamcmv,A,Nisynch_10', 'spliceAShcCJ,S,Niagree_11', 'yahalom-Paulson,R,Nisynch_R2', 'yahalom,I,Nisynch_I2', 'ksl,A,Nisynch_A3', 'kaochow2,R,Nisynch_8', 'lcbreakerS1,I,Secret_i0', 'kaochow2,I,Niagree_6', 'spliceAS-HC,R,Nisynch_12', 'denningSacco-Lowe,R,Nisynch_R2', 'yahalom,R,Nisynch_R2', 'bunava13,R1,Niagree_B1', 'kaochow-3,R,Niagree_R2', 'neustub,I,Nisynch_I3', 'ksl,A,Niagree_A2', 'yahalom-BAN,I,Nisynch_I2', 'neustub^Repeat,R,Nisynch_R3', 'ksl,I,Niagree_I2', 'bunava23,R0,Niagree_A1', 'needhamschroederpk,I,Nisynch_I3', 'unknown2,I,Nisynch_i1', 'spliceAS,I,Niagree_9', 'spliceAShc,C,Nisynch_10', 'kaochow,I,Niagree_I2', 'bunava23,R2,Niagree_C1', 'bunava23,R0,Nisynch_A2', 'ksl-Lowe,R,Niagree_R2', 'needhamschroedersk-amend,R,Nisynch_R3', 'bunava23,R1,Niagree_B1', 'spliceAS,R,Nisynch_12', 'yahalom-BAN,R,Nisynch_R2', 'ksl,B,Niagree_B2', 'boydNS,R,Secret_r1', 'kaochow,R,Niagree_9', 'neustub-Hwang,I,Nisynch_I3', 'unknown2,R,Niagree_r2', 'kaochow-3,I,Niagree_I2', 'bunava13,R1,Nisynch_B2', 'spliceAShcCJ,C,Niagree_9', 'kaochow-2,I,Niagree_I2', 'nssymmetricamended,A,Nisynch_8b', 'neustub-Hwang,I,Niagree_I2', 'spliceAS-CJ,I,Niagree_9', 'spliceAS,C,Nisynch_10', 'woolam,I,Nisynch_I2', 'bunava13,R0,Nisynch_A2', 'spliceAS,C,Niagree_9', 'kaochow3,I,Nisynch_5', 'unknown2,I,Niagree_i2', 'course2r890year0405ex3,I,Nisynch_i2', 'spliceAS-HC,I,Nisynch_10', 'andrew,I,Nisynch_I2', 'spliceAS-CJ,R,Nisynch_12', 'spliceAS-CJ,I,Nisynch_10', 'bunava13,R0,Niagree_A1', 'boydNS,R,Niagree_r3', 'woolam,R,Nisynch_R2', 'boyd,R,Nisynch_12', 'spliceAS-CJ,R,Niagree_11', 'yahalom-Paulson,I,Nisynch_I2', 'denningsaccosh,B,Nisynch_8', 'kaochow,I,Nisynch_I1', 'needhamschroedersk-amend,I,Nisynch_I3', 'kaochowPalm,I,Niagree_6', 'ksl,R,Niagree_R2', 'spliceAShcCJ,C,Nisynch_10', 'denningSacco,R,Nisynch_R2', 'spliceAShc,S,Nisynch_12', 'yahalompaulson,R,Niagree_13', 'nssymmetricamended,A,Niagree_8a', 'needhamschroederpk-Lowe,I,Nisynch_I3', 'woolamcmv,B,Niagree_12', 'spliceAShc,C,Secret_7', 'spliceAS-HC,I,Niagree_9', 'yahalompaulson,I,Nisynch_9', 'kaochow-2,R,Nisynch_R1', 'neustub^Repeat,R,Niagree_R2', 'bunava23,R2,Nisynch_C2', 'needhamschroederpk,R,Secret_R1', 'andrew,I,Niagree_I3', 'needhamschroederpk,R,Secret_R2', 'ccitt509-3,R,Nisynch_R1', 'kaochow-2,I,Nisynch_I1', 'ksl-Lowe,I,Niagree_I2', 'kaochow3,R,Niagree_9', 'kaochow-3,R,Nisynch_R1', 'yahalompaulson,I,Niagree_10', 'kaochow3,R,Nisynch_8', 'neustub-Hwang,R,Niagree_R2', 'denningSacco-Lowe,I,Nisynch_I2', 'kaochow,R,Nisynch_8', 'spliceAS,S,Nisynch_12', 'kaochow3,I,Niagree_6', 'spliceAShc,S,Niagree_11', 'spliceAS,R,Niagree_11', 'yahalompaulson,R,Nisynch_12', 'ksl-Lowe,I,Nisynch_I3', 'needhamschroederpk,R,Nisynch_R3', 'woolamcmv,B,Nisynch_13', 'broken1,R,Secret_4', 'andrew-Concrete,I,Nisynch_I2', 'needhamschroederpk-Lowe,R,Nisynch_R3', 'ksl-Lowe,R,Nisynch_R3', 'boyd,I,Niagree_7', 'nssymmetricamended,B,Nisynch_9b', 'nssymmetricamended,B,Niagree_9a', 'woolamcmv,A,Niagree_9', 'ksl,R,Nisynch_R3', 'kaochow2,I,Nisynch_5', 'bunava23,R1,Nisynch_B2', 'unknown2,R,Nisynch_r1', 'boyd,I,Nisynch_8', 'spliceAS,I,Nisynch_10']
Attack with 4 runs:
['bunava13,R2,Nisynch_C2', 'bunava14,B,Nisynch_B2', 'spliceAShc,S,Secret_8', 'bunava14,A,Niagree_A1', 'bunava14,C,Nisynch_C2', 'bunava13,R2,Niagree_C1', 'bunava14,C,Niagree_C1', 'bunava14,A,Nisynch_A2', 'nsl3th3,I,Nisynch_i2', 'nsl3th3,R,Nisynch_r2', 'bunava24,A,Nisynch_A2', 'bunava24,A,Niagree_A1', 'spliceAS,S,Secret_8', 'bunava14,B,Niagree_B1']
Attack with 5 runs:
['bunava14,D,Niagree_D1', 'bunava14,D,Nisynch_D2']
Attack with 6 runs:
[]
Attack with 7 runs:
[]

518
test/boundruns1.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Ok [does not occur]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [no attack within bounds]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Ok [does not occur]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [no attack within bounds]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [no attack within bounds]
claim spliceAS,R Nisynch_12 - Ok [does not occur]
claim spliceAS,R Niagree_11 - Ok [does not occur]
claim spliceAS,R Secret_8 N2 Ok [no attack within bounds]
claim spliceAS,I Nisynch_10 - Ok [does not occur]
claim spliceAS,I Niagree_9 - Ok [does not occur]
claim spliceAS,I Secret_7 N2 Ok [no attack within bounds]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Ok [does not occur]
claim kaochow-2,R Nisynch_R1 - Ok [does not occur]
claim kaochow-2,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-2,I Niagree_I2 - Ok [does not occur]
claim kaochow-2,I Nisynch_I1 - Ok [does not occur]
claim yahalom-Lowe,R Nisynch_R2 - Ok [does not occur]
claim yahalom-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-Lowe,I Nisynch_I2 - Ok [does not occur]
claim yahalom-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim otwayrees,R Nisynch_R2 - Ok [does not occur]
claim otwayrees,R Secret_R1 Kir Ok [no attack within bounds]
claim otwayrees,I Nisynch_I2 - Ok [does not occur]
claim otwayrees,I Secret_I1 Kir Ok [no attack within bounds]
claim smartright,R Nisynch_R1 - Ok [does not occur]
claim needhamschroedersk,R Nisynch_R3 - Ok [does not occur]
claim needhamschroedersk,R Secret_R1 Kir Ok [no attack within bounds]
claim needhamschroedersk,I Nisynch_I3 - Ok [does not occur]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow,R Niagree_R2 - Ok [does not occur]
claim kaochow,R Nisynch_R1 - Ok [does not occur]
claim kaochow,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow,I Niagree_I2 - Ok [does not occur]
claim kaochow,I Nisynch_I1 - Ok [does not occur]
claim spliceAS-HC,R Nisynch_12 - Ok [does not occur]
claim spliceAS-HC,R Niagree_11 - Ok [does not occur]
claim spliceAS-HC,R Secret_8 N2 Ok [no attack within bounds]
claim spliceAS-HC,I Nisynch_10 - Ok [does not occur]
claim spliceAS-HC,I Niagree_9 - Ok [does not occur]
claim spliceAS-HC,I Secret_7 N2 Ok [no attack within bounds]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [no attack within bounds]
claim ccitt509-3,R Secret_R2 Ya Ok [no attack within bounds]
claim ccitt509-3,R Nisynch_R1 - Ok [does not occur]
claim ccitt509-3,I Secret_I3 Yb Ok [no attack within bounds]
claim ccitt509-3,I Secret_I2 Ya Ok [no attack within bounds]
claim ccitt509-3,I Nisynch_I1 - Ok [does not occur]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Ok [does not occur]
claim denningSacco-Lowe,R Niagree_R1 - Ok [does not occur]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Ok [does not occur]
claim denningSacco-Lowe,I Niagree_I1 - Ok [does not occur]
claim yahalom-Paulson,R Nisynch_R2 - Ok [does not occur]
claim yahalom-Paulson,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-Paulson,I Nisynch_I2 - Ok [does not occur]
claim yahalom-Paulson,I Secret_I1 Kir Ok [no attack within bounds]
claim woolam,R Nisynch_R2 - Ok [does not occur]
claim woolam,R Secret_R1 Kir Ok [no attack within bounds]
claim woolam,I Nisynch_I2 - Ok [does not occur]
claim woolam,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub-Hwang,R Nisynch_R3 - Ok [does not occur]
claim neustub-Hwang,R Niagree_R2 - Ok [does not occur]
claim neustub-Hwang,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-Hwang,I Nisynch_I3 - Ok [does not occur]
claim neustub-Hwang,I Niagree_I2 - Ok [does not occur]
claim neustub-Hwang,I Secret_I1 Kir Ok [no attack within bounds]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Ok [does not occur]
claim kaochow-3,R Nisynch_R1 - Ok [does not occur]
claim kaochow-3,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-3,I Niagree_I2 - Ok [does not occur]
claim kaochow-3,I Nisynch_I1 - Ok [does not occur]
claim woolamPi,R Nisynch_R1 - Ok [does not occur]
claim ccitt509-ban3,R Nisynch_5 - Ok [does not occur]
claim ccitt509-ban3,I Nisynch_4 - Ok [does not occur]
claim ksl,R Nisynch_R3 - Ok [does not occur]
claim ksl,R Niagree_R2 - Ok [does not occur]
claim ksl,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl,I Nisynch_I3 - Ok [does not occur]
claim ksl,I Niagree_I2 - Ok [does not occur]
claim ksl,I Secret_I1 Kir Ok [no attack within bounds]
claim ksl-Lowe,R Nisynch_R3 - Ok [does not occur]
claim ksl-Lowe,R Niagree_R2 - Ok [does not occur]
claim ksl-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl-Lowe,I Nisynch_I3 - Ok [does not occur]
claim ksl-Lowe,I Niagree_I2 - Ok [does not occur]
claim ksl-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Ok [does not occur]
claim neustub,R Niagree_R2 - Ok [does not occur]
claim neustub,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub,I Nisynch_I3 - Ok [does not occur]
claim neustub,I Niagree_I2 - Ok [does not occur]
claim neustub,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub^Repeat,R Nisynch_R3 - Ok [does not occur]
claim neustub^Repeat,R Niagree_R2 - Ok [does not occur]
claim neustub^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub^Repeat,I Nisynch_I3 - Ok [does not occur]
claim neustub^Repeat,I Niagree_I2 - Ok [does not occur]
claim neustub^Repeat,I Secret_I1 Kir Ok [no attack within bounds]
claim woolamPi-f,R Nisynch_R1 - Ok [does not occur]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Ok [does not occur]
claim denningSacco,R Niagree_R1 - Ok [does not occur]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Ok [does not occur]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Ok [does not occur]
claim spliceAS-CJ,R Niagree_11 - Ok [does not occur]
claim spliceAS-CJ,R Secret_8 N2 Ok [no attack within bounds]
claim spliceAS-CJ,I Nisynch_10 - Ok [does not occur]
claim spliceAS-CJ,I Niagree_9 - Ok [does not occur]
claim spliceAS-CJ,I Secret_7 N2 Ok [no attack within bounds]
claim needhamschroedersk-amend,R Nisynch_R3 - Ok [does not occur]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Ok [does not occur]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Ok [does not occur]
claim needhamschroedersk,R Secret_R1 Kir Ok [no attack within bounds]
claim needhamschroedersk,I Nisynch_I3 - Ok [does not occur]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Ok [does not occur]
claim andrew-Concrete,R Secret_R1 kir Ok [no attack within bounds]
claim andrew-Concrete,I Nisynch_I2 - Ok [no attack within bounds]
claim andrew-Concrete,I Secret_I1 kir Ok [no attack within bounds]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [no attack within bounds]
claim andrew-Ban,R Niagree_R2 - Ok [does not occur]
claim andrew-Ban,R Nisynch_R1 - Ok [does not occur]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [no attack within bounds]
claim andrew-Ban,I Niagree_I2 - Ok [does not occur]
claim andrew-Ban,I Nisynch_I1 - Ok [does not occur]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 1 attack]
claim yahalom-BAN,R Nisynch_R2 - Ok [does not occur]
claim yahalom-BAN,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-BAN,I Nisynch_I2 - Ok [does not occur]
claim yahalom-BAN,I Secret_I1 Kir Ok [no attack within bounds]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Ok [no attack within bounds]
claim tmn,I Nisynch_I2 - Ok [does not occur]
claim tmn,I Secret_I1 Kr Ok [no attack within bounds]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 1 attack]
claim andrew,R Niagree_R3 - Ok [does not occur]
claim andrew,R Nisynch_R2 - Ok [does not occur]
claim andrew,R Secret_R1 kir Ok [no attack within bounds]
claim andrew,I Niagree_I3 - Ok [does not occur]
claim andrew,I Nisynch_I2 - Ok [does not occur]
claim andrew,I Secret_I1 kir Ok [no attack within bounds]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 1 attack]
claim andrew-LoweBan,R Secret_R2 kir Ok [no attack within bounds]
claim andrew-LoweBan,R Nisynch_R1 - Ok [does not occur]
claim andrew-LoweBan,I Secret_I2 kir Ok [no attack within bounds]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Ok [does not occur]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [no attack within bounds]
claim yahalom,R Nisynch_R2 - Ok [does not occur]
claim yahalom,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom,I Nisynch_I2 - Ok [does not occur]
claim yahalom,I Secret_I1 Kir Ok [no attack within bounds]
claim wmf-Lowe,R Nisynch_R2 - Ok [does not occur]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Ok [does not occur]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Ok [does not occur]
claim needhamschroederpk,R Secret_R2 Ni Ok [no attack within bounds]
claim needhamschroederpk,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroederpk,I Nisynch_I3 - Ok [does not occur]
claim needhamschroederpk,I Secret_I2 Nr Ok [no attack within bounds]
claim needhamschroederpk,I Secret_I1 Ni Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Ok [does not occur]
claim neustub,R Niagree_R2 - Ok [does not occur]
claim neustub,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub,I Nisynch_I3 - Ok [does not occur]
claim neustub,I Niagree_I2 - Ok [does not occur]
claim neustub,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub^Repeat,R Nisynch_R3 - Ok [does not occur]
claim neustub^Repeat,R Niagree_R2 - Ok [does not occur]
claim neustub^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub^Repeat,I Nisynch_I3 - Ok [does not occur]
claim neustub^Repeat,I Niagree_I2 - Ok [does not occur]
claim neustub^Repeat,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Ok [does not occur]
claim neustub,R Niagree_R2 - Ok [does not occur]
claim neustub,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub,I Nisynch_I3 - Ok [does not occur]
claim neustub,I Niagree_I2 - Ok [does not occur]
claim neustub,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub^Repeat,R Nisynch_R3 - Ok [does not occur]
claim neustub^Repeat,R Niagree_R2 - Ok [does not occur]
claim neustub^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub^Repeat,I Nisynch_I3 - Ok [does not occur]
claim neustub^Repeat,I Niagree_I2 - Ok [does not occur]
claim neustub^Repeat,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [does not occur]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [does not occur]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [does not occur]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [does not occur]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [does not occur]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [does not occur]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [does not occur]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [does not occur]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [no attack within bounds]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [no attack within bounds]
claim andrewBan,R Niagree_8b - Ok [does not occur]
claim andrewBan,R Nisynch_8 - Ok [does not occur]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [no attack within bounds]
claim andrewBan,I Niagree_5b - Ok [does not occur]
claim andrewBan,I Nisynch_5 - Ok [does not occur]
claim nsl3,R Nisynch_r4 - Ok [does not occur]
claim nsl3,R Niagree_r3 - Ok [does not occur]
claim nsl3,R Secret_r2 nr Ok [no attack within bounds]
claim nsl3,R Secret_r1 ni Ok [no attack within bounds]
claim nsl3,I Nisynch_i4 - Ok [no attack within bounds]
claim nsl3,I Niagree_i3 - Ok [no attack within bounds]
claim nsl3,I Secret_i2 nr Ok [no attack within bounds]
claim nsl3,I Secret_i1 ni Ok [no attack within bounds]
claim bkebroken,R Secret_5 kir Ok [no attack within bounds]
claim bkebroken,I Secret_4 kir Ok [no attack within bounds]
claim spliceAS,S Nisynch_12 - Ok [does not occur]
claim spliceAS,S Niagree_11 - Ok [does not occur]
claim spliceAS,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAS,C Nisynch_10 - Ok [does not occur]
claim spliceAS,C Niagree_9 - Ok [does not occur]
claim spliceAS,C Secret_7 N2 Ok [no attack within bounds]
claim bkeONE,R Secret_5 kir Ok [no attack within bounds]
claim bkeONE,I Secret_4 kir Ok [no attack within bounds]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [no attack within bounds]
claim nsl7,R Secret_4 ni Ok [no attack within bounds]
claim ns3brutus,R Secret_5 ni Ok [no attack within bounds]
claim ns3brutus,I Secret_4 nr Ok [no attack within bounds]
claim woolampif,B Nisynch_7 - Ok [does not occur]
claim woolampif,B Niagree_6 - Ok [does not occur]
claim yahalomBan,B Secret_6 kab Ok [no attack within bounds]
claim yahalomBan,A Secret_5 kab Ok [no attack within bounds]
claim boyd,R Nisynch_12 - Ok [does not occur]
claim boyd,R Niagree_11 - Ok [does not occur]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [no attack within bounds]
claim boyd,I Nisynch_8 - Ok [does not occur]
claim boyd,I Niagree_7 - Ok [does not occur]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [no attack within bounds]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Ok [does not occur]
claim spliceAShc,S Niagree_11 - Ok [does not occur]
claim spliceAShc,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShc,C Nisynch_10 - Ok [does not occur]
claim spliceAShc,C Niagree_9 - Ok [does not occur]
claim spliceAShc,C Secret_7 N2 Ok [no attack within bounds]
claim isoiec11770213,R Secret_6 kir Ok [no attack within bounds]
claim isoiec11770213,I Secret_5 kir Ok [no attack within bounds]
claim gongnonceb,R Niagree_13 - Ok [does not occur]
claim gongnonceb,R Nisynch_12 - Ok [does not occur]
claim gongnonceb,R Secret_11 kr Ok [no attack within bounds]
claim gongnonceb,R Secret_10 ki Ok [no attack within bounds]
claim gongnonceb,I Niagree_9 - Ok [does not occur]
claim gongnonceb,I Nisynch_8 - Ok [does not occur]
claim gongnonceb,I Secret_7 kr Ok [no attack within bounds]
claim gongnonceb,I Secret_6 ki Ok [no attack within bounds]
claim yahalompaulson,R Niagree_13 - Ok [does not occur]
claim yahalompaulson,R Nisynch_12 - Ok [does not occur]
claim yahalompaulson,R Secret_11 kir Ok [no attack within bounds]
claim yahalompaulson,I Niagree_10 - Ok [does not occur]
claim yahalompaulson,I Nisynch_9 - Ok [does not occur]
claim yahalompaulson,I Secret_8 kir Ok [no attack within bounds]
claim ksl,B Nisynch_B3 - Ok [does not occur]
claim ksl,B Niagree_B2 - Ok [does not occur]
claim ksl,B Secret_B1 Kab Ok [no attack within bounds]
claim ksl,A Nisynch_A3 - Ok [does not occur]
claim ksl,A Niagree_A2 - Ok [does not occur]
claim ksl,A Secret_A1 Kab Ok [no attack within bounds]
claim denningsaccosh,B Niagree_9 - Ok [does not occur]
claim denningsaccosh,B Nisynch_8 - Ok [does not occur]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Ok [does not occur]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Ok [does not occur]
claim woolamcmv,B Niagree_12 - Ok [does not occur]
claim woolamcmv,B Secret_11 Kab Ok [no attack within bounds]
claim woolamcmv,A Nisynch_10 - Ok [does not occur]
claim woolamcmv,A Niagree_9 - Ok [does not occur]
claim woolamcmv,A Secret_8 Kab Ok [no attack within bounds]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [no attack within bounds]
claim andrewLoweBan,R Niagree_8b - Ok [does not occur]
claim andrewLoweBan,R Nisynch_8 - Ok [does not occur]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [no attack within bounds]
claim andrewLoweBan,I Niagree_5b - Ok [does not occur]
claim andrewLoweBan,I Nisynch_5 - Ok [does not occur]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [does not occur]
claim course2r890year0405ex3,I Niagree_i1 - Ok [does not occur]
claim ccitt509,R Niagree_11 - Ok [does not occur]
claim ccitt509,R Nisynch_10 - Ok [does not occur]
claim ccitt509,R Secret_9 yr Ok [no attack within bounds]
claim ccitt509,R Secret_8 yi Ok [no attack within bounds]
claim ccitt509,I Niagree_7 - Ok [does not occur]
claim ccitt509,I Nisynch_6 - Ok [does not occur]
claim ccitt509,I Secret_5 yr Ok [no attack within bounds]
claim ccitt509,I Secret_4 yi Ok [no attack within bounds]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [no attack within bounds]
claim bunava23,R2 Nisynch_C2 - Ok [does not occur]
claim bunava23,R2 Niagree_C1 - Ok [does not occur]
claim bunava23,R1 Nisynch_B2 - Ok [does not occur]
claim bunava23,R1 Niagree_B1 - Ok [does not occur]
claim bunava23,R0 Nisynch_A2 - Ok [does not occur]
claim bunava23,R0 Niagree_A1 - Ok [does not occur]
claim wmfbrutus,B Secret_3 kab Ok [no attack within bounds]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Ok [does not occur]
claim kaochow2,R Nisynch_8 - Ok [does not occur]
claim kaochow2,I Secret_7 kir Ok [no attack within bounds]
claim kaochow2,I Niagree_6 - Ok [does not occur]
claim kaochow2,I Nisynch_5 - Ok [does not occur]
claim otwayrees,B Nisynch_6b - Ok [does not occur]
claim otwayrees,B Niagree_6a - Ok [does not occur]
claim otwayrees,B Secret_6 kab Ok [no attack within bounds]
claim otwayrees,A Nisynch_5c - Ok [does not occur]
claim otwayrees,A Niagree_5b - Ok [does not occur]
claim otwayrees,A Secret_5 kab Ok [no attack within bounds]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [does not occur]
claim kaochowPalm,R Nisynch_8 - Ok [does not occur]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Ok [does not occur]
claim kaochowPalm,I Nisynch_5 - Ok [does not occur]
claim as3a,I Nisynch_i1 - Ok [does not occur]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Ok [no attack within bounds]
claim tmn,S Secret_7 Ka Fail [at least 1 attack]
claim tmn,B Secret_6 Kb Ok [no attack within bounds]
claim tmn,A Secret_8 Kb Ok [no attack within bounds]
claim tmn,A Secret_5 Ka Ok [no attack within bounds]
claim nssymmetricamended,B Nisynch_9b - Ok [does not occur]
claim nssymmetricamended,B Niagree_9a - Ok [does not occur]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Ok [does not occur]
claim nssymmetricamended,A Niagree_8a - Ok [does not occur]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Ok [does not occur]
claim gongnonce,R Nisynch_12 - Ok [does not occur]
claim gongnonce,R Secret_11 kr Ok [no attack within bounds]
claim gongnonce,R Secret_10 ki Ok [no attack within bounds]
claim gongnonce,I Niagree_9 - Ok [does not occur]
claim gongnonce,I Nisynch_8 - Ok [does not occur]
claim gongnonce,I Secret_7 kr Ok [no attack within bounds]
claim gongnonce,I Secret_6 ki Ok [no attack within bounds]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [does not occur]
claim course2r890year0405ex3,I Niagree_i1 - Ok [does not occur]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Ok [does not occur]
claim kaochow,R Nisynch_8 - Ok [does not occur]
claim kaochow,I Secret_7 kir Ok [no attack within bounds]
claim kaochow,I Niagree_6 - Ok [does not occur]
claim kaochow,I Nisynch_5 - Ok [does not occur]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Ok [no attack within bounds]
claim bkevariation,R Nisynch_9 - Ok [does not occur]
claim bkevariation,R Niagree_8 - Ok [does not occur]
claim bkevariation,R Secret_7 kir Ok [no attack within bounds]
claim bkevariation,I Nisynch_6 - Ok [does not occur]
claim bkevariation,I Niagree_5 - Ok [does not occur]
claim bkevariation,I Secret_4 kir Ok [no attack within bounds]
claim yahalomlowe,R Niagree_13 - Ok [does not occur]
claim yahalomlowe,R Nisynch_12 - Ok [does not occur]
claim yahalomlowe,R Secret_11 kir Ok [no attack within bounds]
claim yahalomlowe,I Nisynch_10 - Ok [does not occur]
claim yahalomlowe,I Niagree_9 - Ok [does not occur]
claim yahalomlowe,I Secret_8 kir Ok [no attack within bounds]
claim broken1,R Secret_4 PlainSight Ok [no attack within bounds]
claim bke,R Nisynch_9 - Ok [does not occur]
claim bke,R Niagree_8 - Ok [does not occur]
claim bke,R Secret_7 kir Ok [no attack within bounds]
claim bke,I Nisynch_6 - Ok [no attack within bounds]
claim bke,I Niagree_5 - Ok [no attack within bounds]
claim bke,I Secret_4 kir Ok [no attack within bounds]
claim spliceAShcCJ,S Nisynch_12 - Ok [does not occur]
claim spliceAShcCJ,S Niagree_11 - Ok [does not occur]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Ok [does not occur]
claim spliceAShcCJ,C Niagree_9 - Ok [does not occur]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Ok [does not occur]
claim soph,I Niagree_3 - Ok [does not occur]
claim bunava13,R2 Nisynch_C2 - Ok [does not occur]
claim bunava13,R2 Niagree_C1 - Ok [does not occur]
claim bunava13,R1 Nisynch_B2 - Ok [does not occur]
claim bunava13,R1 Niagree_B1 - Ok [does not occur]
claim bunava13,R0 Nisynch_A2 - Ok [does not occur]
claim bunava13,R0 Niagree_A1 - Ok [does not occur]
claim bunava24,A Nisynch_A2 - Ok [does not occur]
claim bunava24,A Niagree_A1 - Ok [does not occur]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Ok [does not occur]
claim kaochow3,R Nisynch_8 - Ok [does not occur]
claim kaochow3,I Secret_7 kir Ok [no attack within bounds]
claim kaochow3,I Niagree_6 - Ok [does not occur]
claim kaochow3,I Nisynch_5 - Ok [does not occur]
claim unknown2,R Secret_r3 kir Ok [no attack within bounds]
claim unknown2,R Niagree_r2 - Ok [does not occur]
claim unknown2,R Nisynch_r1 - Ok [does not occur]
claim unknown2,I Secret_i3 kir Ok [no attack within bounds]
claim unknown2,I Niagree_i2 - Ok [does not occur]
claim unknown2,I Nisynch_i1 - Ok [does not occur]
claim localclaims,R Secret_r1 ni Fail [at least 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Ok [no attack within bounds]
claim ns3speedtest,I Secret_4 nr Ok [no attack within bounds]
claim yahalom,B Secret_6 kab Ok [no attack within bounds]
claim yahalom,A Secret_5 kab Ok [no attack within bounds]
claim ns3,R Nisynch_r4 - Ok [does not occur]
claim ns3,R Niagree_r3 - Ok [does not occur]
claim ns3,R Secret_r2 nr Ok [no attack within bounds]
claim ns3,R Secret_r1 ni Ok [no attack within bounds]
claim ns3,I Nisynch_i4 - Ok [does not occur]
claim ns3,I Niagree_i3 - Ok [does not occur]
claim ns3,I Secret_i2 nr Ok [no attack within bounds]
claim ns3,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Ok [does not occur]
claim nsl3rep,R Nisynch_8 - Ok [does not occur]
claim nsl3rep,R Niagree_5 - Ok [does not occur]
claim nsl3rep,I Nisynch_7 - Ok [does not occur]
claim nsl3rep,I Niagree_4 - Ok [no attack within bounds]
claim bunava14,D Nisynch_D2 - Ok [does not occur]
claim bunava14,D Niagree_D1 - Ok [does not occur]
claim bunava14,C Nisynch_C2 - Ok [does not occur]
claim bunava14,C Niagree_C1 - Ok [does not occur]
claim bunava14,B Nisynch_B2 - Ok [does not occur]
claim bunava14,B Niagree_B1 - Ok [does not occur]
claim bunava14,A Nisynch_A2 - Ok [does not occur]
claim bunava14,A Niagree_A1 - Ok [does not occur]
claim boydNS,R Nisynch_r4 - Ok [does not occur]
claim boydNS,R Niagree_r3 - Ok [does not occur]
claim boydNS,R Secret_r2 nr Ok [no attack within bounds]
claim boydNS,R Secret_r1 ni Ok [no attack within bounds]
claim boydNS,I Nisynch_i4 - Ok [does not occur]
claim boydNS,I Niagree_i3 - Ok [does not occur]
claim boydNS,I Secret_i2 nr Ok [no attack within bounds]
claim boydNS,I Secret_i1 ni Ok [no attack within bounds]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [no attack within bounds]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [no attack within bounds]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [no attack within bounds]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [no attack within bounds]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [no attack within bounds]
claim ibe,R Nisynch_r4 - Ok [does not occur]
claim ibe,R Niagree_r3 - Ok [does not occur]
claim ibe,R Secret_r2 nr Ok [no attack within bounds]
claim ibe,R Secret_r1 ni Ok [no attack within bounds]
claim ibe,I Nisynch_i4 - Ok [does not occur]
claim ibe,I Niagree_i3 - Ok [does not occur]
claim ibe,I Secret_i2 nr Ok [no attack within bounds]
claim ibe,I Secret_i1 ni Ok [no attack within bounds]
claim ibe,R Secret_r1 ni Ok [no attack within bounds]
claim ibe,I Secret_i1 ni Ok [no attack within bounds]
claim tlspaulson-avispa,b Niagree_10c - Ok [does not occur]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [no attack within bounds]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [no attack within bounds]
claim tlspaulson-avispa,a Niagree_9c - Ok [no attack within bounds]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [no attack within bounds]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [no attack within bounds]
claim nsl3th2,R Nisynch_r - Ok [does not occur]
claim nsl3th2,I Nisynch_i - Ok [does not occur]
claim nsl3th1,R Nisynch_r - Ok [does not occur]
claim nsl3th1,I Nisynch_i - Ok [does not occur]
claim nsl3th3,R Nisynch_r2 - Ok [does not occur]
claim nsl3th3,I Nisynch_i2 - Ok [does not occur]
claim nsl3th1,R Nisynch_r - Ok [does not occur]
claim nsl3th1,I Nisynch_i - Ok [does not occur]
claim nsl3th3nr,R Nisynch_r2 - Ok [does not occur]
claim nsl3th3nr,I Nisynch_i2 - Ok [does not occur]
claim nsl3th2,R Nisynch_r - Ok [does not occur]
claim nsl3th2,I Nisynch_i - Ok [does not occur]
claim nsl3th3ni,R Nisynch_r2 - Ok [does not occur]
claim nsl3th3ni,I Nisynch_i2 - Ok [does not occur]
claim nsl3,R Nisynch_r4 - Ok [does not occur]
claim nsl3,R Niagree_r3 - Ok [does not occur]
claim nsl3,R Secret_r2 nr Ok [no attack within bounds]
claim nsl3,R Secret_r1 ni Ok [no attack within bounds]
claim nsl3,I Nisynch_i4 - Ok [no attack within bounds]
claim nsl3,I Niagree_i3 - Ok [no attack within bounds]
claim nsl3,I Secret_i2 nr Ok [no attack within bounds]
claim nsl3,I Secret_i1 ni Ok [no attack within bounds]
claim ns3,R Nisynch_r4 - Ok [does not occur]
claim ns3,R Niagree_r3 - Ok [does not occur]
claim ns3,R Secret_r2 nr Ok [no attack within bounds]
claim ns3,R Secret_r1 ni Ok [no attack within bounds]
claim ns3,I Nisynch_i4 - Ok [does not occur]
claim ns3,I Niagree_i3 - Ok [does not occur]
claim ns3,I Secret_i2 nr Ok [no attack within bounds]
claim ns3,I Secret_i1 ni Ok [no attack within bounds]

518
test/boundruns2.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Ok [does not occur]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [no attack within bounds]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Ok [does not occur]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [no attack within bounds]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [no attack within bounds]
claim spliceAS,R Nisynch_12 - Ok [does not occur]
claim spliceAS,R Niagree_11 - Ok [does not occur]
claim spliceAS,R Secret_8 N2 Ok [no attack within bounds]
claim spliceAS,I Nisynch_10 - Ok [does not occur]
claim spliceAS,I Niagree_9 - Ok [does not occur]
claim spliceAS,I Secret_7 N2 Ok [no attack within bounds]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Ok [does not occur]
claim kaochow-2,R Nisynch_R1 - Ok [does not occur]
claim kaochow-2,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-2,I Niagree_I2 - Ok [does not occur]
claim kaochow-2,I Nisynch_I1 - Ok [does not occur]
claim yahalom-Lowe,R Nisynch_R2 - Ok [does not occur]
claim yahalom-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
claim yahalom-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim otwayrees,R Nisynch_R2 - Fail [at least 1 attack]
claim otwayrees,R Secret_R1 Kir Ok [proof of correctness]
claim otwayrees,I Nisynch_I2 - Fail [at least 1 attack]
claim otwayrees,I Secret_I1 Kir Ok [proof of correctness]
claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 1 attack]
claim needhamschroedersk,I Nisynch_I3 - Ok [does not occur]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Fail [at least 2 attacks]
claim kaochow,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow,I Niagree_I2 - Ok [does not occur]
claim kaochow,I Nisynch_I1 - Ok [does not occur]
claim spliceAS-HC,R Nisynch_12 - Ok [does not occur]
claim spliceAS-HC,R Niagree_11 - Ok [does not occur]
claim spliceAS-HC,R Secret_8 N2 Ok [no attack within bounds]
claim spliceAS-HC,I Nisynch_10 - Ok [does not occur]
claim spliceAS-HC,I Niagree_9 - Ok [does not occur]
claim spliceAS-HC,I Secret_7 N2 Ok [no attack within bounds]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [no attack within bounds]
claim ccitt509-3,R Secret_R2 Ya Ok [no attack within bounds]
claim ccitt509-3,R Nisynch_R1 - Ok [no attack within bounds]
claim ccitt509-3,I Secret_I3 Yb Ok [no attack within bounds]
claim ccitt509-3,I Secret_I2 Ya Ok [no attack within bounds]
claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Ok [does not occur]
claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Ok [does not occur]
claim denningSacco-Lowe,I Niagree_I1 - Ok [does not occur]
claim yahalom-Paulson,R Nisynch_R2 - Ok [does not occur]
claim yahalom-Paulson,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-Paulson,I Nisynch_I2 - Ok [does not occur]
claim yahalom-Paulson,I Secret_I1 Kir Ok [no attack within bounds]
claim woolam,R Nisynch_R2 - Ok [does not occur]
claim woolam,R Secret_R1 Kir Ok [no attack within bounds]
claim woolam,I Nisynch_I2 - Ok [does not occur]
claim woolam,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub-Hwang,R Nisynch_R3 - Ok [does not occur]
claim neustub-Hwang,R Niagree_R2 - Ok [does not occur]
claim neustub-Hwang,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-Hwang,I Nisynch_I3 - Ok [does not occur]
claim neustub-Hwang,I Niagree_I2 - Ok [does not occur]
claim neustub-Hwang,I Secret_I1 Kir Ok [no attack within bounds]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Ok [does not occur]
claim kaochow-3,R Nisynch_R1 - Ok [does not occur]
claim kaochow-3,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-3,I Niagree_I2 - Ok [does not occur]
claim kaochow-3,I Nisynch_I1 - Ok [does not occur]
claim woolamPi,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness]
claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
claim ksl,R Nisynch_R3 - Ok [does not occur]
claim ksl,R Niagree_R2 - Ok [does not occur]
claim ksl,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl,I Nisynch_I3 - Ok [does not occur]
claim ksl,I Niagree_I2 - Ok [does not occur]
claim ksl,I Secret_I1 Kir Ok [no attack within bounds]
claim ksl-Lowe,R Nisynch_R3 - Ok [does not occur]
claim ksl-Lowe,R Niagree_R2 - Ok [does not occur]
claim ksl-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl-Lowe,I Nisynch_I3 - Ok [does not occur]
claim ksl-Lowe,I Niagree_I2 - Ok [does not occur]
claim ksl-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Ok [does not occur]
claim neustub,R Niagree_R2 - Ok [does not occur]
claim neustub,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [no attack within bounds]
claim neustub^Repeat,R Niagree_R2 - Ok [no attack within bounds]
claim neustub^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Ok [does not occur]
claim denningSacco,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Ok [does not occur]
claim spliceAS-CJ,R Niagree_11 - Ok [does not occur]
claim spliceAS-CJ,R Secret_8 N2 Ok [no attack within bounds]
claim spliceAS-CJ,I Nisynch_10 - Ok [does not occur]
claim spliceAS-CJ,I Niagree_9 - Ok [does not occur]
claim spliceAS-CJ,I Secret_7 N2 Ok [no attack within bounds]
claim needhamschroedersk-amend,R Nisynch_R3 - Ok [does not occur]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Ok [does not occur]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 1 attack]
claim needhamschroedersk,I Nisynch_I3 - Ok [does not occur]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Ok [no attack within bounds]
claim andrew-Concrete,R Secret_R1 kir Ok [no attack within bounds]
claim andrew-Concrete,I Nisynch_I2 - Ok [no attack within bounds]
claim andrew-Concrete,I Secret_I1 kir Ok [no attack within bounds]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness]
claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness]
claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [no attack within bounds]
claim andrew-Ban,I Niagree_I2 - Ok [no attack within bounds]
claim andrew-Ban,I Nisynch_I1 - Ok [no attack within bounds]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 1 attack]
claim yahalom-BAN,R Nisynch_R2 - Ok [does not occur]
claim yahalom-BAN,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-BAN,I Nisynch_I2 - Ok [does not occur]
claim yahalom-BAN,I Secret_I1 Kir Ok [no attack within bounds]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Fail [at least 1 attack]
claim tmn,I Nisynch_I2 - Fail [at least 1 attack]
claim tmn,I Secret_I1 Kr Fail [at least 1 attack]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 1 attack]
claim andrew,R Niagree_R3 - Ok [proof of correctness]
claim andrew,R Nisynch_R2 - Ok [proof of correctness]
claim andrew,R Secret_R1 kir Ok [proof of correctness]
claim andrew,I Niagree_I3 - Ok [no attack within bounds]
claim andrew,I Nisynch_I2 - Ok [no attack within bounds]
claim andrew,I Secret_I1 kir Ok [no attack within bounds]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 1 attack]
claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness]
claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Fail [at least 1 attack]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [no attack within bounds]
claim yahalom,R Nisynch_R2 - Ok [does not occur]
claim yahalom,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom,I Nisynch_I2 - Ok [does not occur]
claim yahalom,I Secret_I1 Kir Ok [no attack within bounds]
claim wmf-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Ok [does not occur]
claim needhamschroederpk,R Secret_R2 Ni Ok [no attack within bounds]
claim needhamschroederpk,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroederpk,I Nisynch_I3 - Ok [does not occur]
claim needhamschroederpk,I Secret_I2 Nr Ok [no attack within bounds]
claim needhamschroederpk,I Secret_I1 Ni Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Ok [does not occur]
claim neustub,R Niagree_R2 - Ok [does not occur]
claim neustub,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub,I Nisynch_I3 - Ok [does not occur]
claim neustub,I Niagree_I2 - Ok [does not occur]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [no attack within bounds]
claim neustub^Repeat,R Niagree_R2 - Ok [no attack within bounds]
claim neustub^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Ok [does not occur]
claim neustub,R Niagree_R2 - Ok [does not occur]
claim neustub,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [no attack within bounds]
claim neustub^Repeat,R Niagree_R2 - Ok [no attack within bounds]
claim neustub^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub^Repeat,I Nisynch_I3 - Ok [no attack within bounds]
claim neustub^Repeat,I Niagree_I2 - Ok [no attack within bounds]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [does not occur]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [does not occur]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [proof of correctness]
claim andrewBan,R Niagree_8b - Ok [proof of correctness]
claim andrewBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [no attack within bounds]
claim andrewBan,I Niagree_5b - Ok [no attack within bounds]
claim andrewBan,I Nisynch_5 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [no attack within bounds]
claim nsl3,R Niagree_r3 - Ok [no attack within bounds]
claim nsl3,R Secret_r2 nr Ok [no attack within bounds]
claim nsl3,R Secret_r1 ni Ok [no attack within bounds]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [no attack within bounds]
claim nsl3,I Secret_i1 ni Ok [no attack within bounds]
claim bkebroken,R Secret_5 kir Fail [at least 2 attacks]
claim bkebroken,I Secret_4 kir Ok [no attack within bounds]
claim spliceAS,S Nisynch_12 - Ok [does not occur]
claim spliceAS,S Niagree_11 - Ok [does not occur]
claim spliceAS,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAS,C Nisynch_10 - Ok [does not occur]
claim spliceAS,C Niagree_9 - Ok [does not occur]
claim spliceAS,C Secret_7 N2 Ok [no attack within bounds]
claim bkeONE,R Secret_5 kir Ok [proof of correctness]
claim bkeONE,I Secret_4 kir Ok [no attack within bounds]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [proof of correctness]
claim nsl7,R Secret_4 ni Ok [proof of correctness]
claim ns3brutus,R Secret_5 ni Fail [at least 1 attack]
claim ns3brutus,I Secret_4 nr Ok [no attack within bounds]
claim woolampif,B Nisynch_7 - Fail [at least 1 attack]
claim woolampif,B Niagree_6 - Fail [at least 1 attack]
claim yahalomBan,B Secret_6 kab Fail [at least 1 attack]
claim yahalomBan,A Secret_5 kab Fail [at least 1 attack]
claim boyd,R Nisynch_12 - Ok [does not occur]
claim boyd,R Niagree_11 - Ok [does not occur]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [no attack within bounds]
claim boyd,I Nisynch_8 - Ok [does not occur]
claim boyd,I Niagree_7 - Ok [does not occur]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [no attack within bounds]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Ok [does not occur]
claim spliceAShc,S Niagree_11 - Ok [does not occur]
claim spliceAShc,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShc,C Nisynch_10 - Ok [does not occur]
claim spliceAShc,C Niagree_9 - Ok [does not occur]
claim spliceAShc,C Secret_7 N2 Ok [no attack within bounds]
claim isoiec11770213,R Secret_6 kir Ok [no attack within bounds]
claim isoiec11770213,I Secret_5 kir Ok [no attack within bounds]
claim gongnonceb,R Niagree_13 - Fail [at least 1 attack]
claim gongnonceb,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonceb,R Secret_11 kr Ok [no attack within bounds]
claim gongnonceb,R Secret_10 ki Ok [no attack within bounds]
claim gongnonceb,I Niagree_9 - Fail [at least 1 attack]
claim gongnonceb,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonceb,I Secret_7 kr Ok [no attack within bounds]
claim gongnonceb,I Secret_6 ki Ok [no attack within bounds]
claim yahalompaulson,R Niagree_13 - Ok [does not occur]
claim yahalompaulson,R Nisynch_12 - Ok [does not occur]
claim yahalompaulson,R Secret_11 kir Ok [no attack within bounds]
claim yahalompaulson,I Niagree_10 - Ok [does not occur]
claim yahalompaulson,I Nisynch_9 - Ok [does not occur]
claim yahalompaulson,I Secret_8 kir Ok [proof of correctness]
claim ksl,B Nisynch_B3 - Ok [does not occur]
claim ksl,B Niagree_B2 - Ok [does not occur]
claim ksl,B Secret_B1 Kab Ok [no attack within bounds]
claim ksl,A Nisynch_A3 - Ok [does not occur]
claim ksl,A Niagree_A2 - Ok [does not occur]
claim ksl,A Secret_A1 Kab Ok [no attack within bounds]
claim denningsaccosh,B Niagree_9 - Ok [no attack within bounds]
claim denningsaccosh,B Nisynch_8 - Ok [does not occur]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Fail [at least 1 attack]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Ok [does not occur]
claim woolamcmv,B Niagree_12 - Ok [does not occur]
claim woolamcmv,B Secret_11 Kab Ok [no attack within bounds]
claim woolamcmv,A Nisynch_10 - Ok [does not occur]
claim woolamcmv,A Niagree_9 - Ok [does not occur]
claim woolamcmv,A Secret_8 Kab Ok [no attack within bounds]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [proof of correctness]
claim andrewLoweBan,R Niagree_8b - Ok [proof of correctness]
claim andrewLoweBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [proof of correctness]
claim andrewLoweBan,I Niagree_5b - Fail [exactly 1 attack]
claim andrewLoweBan,I Nisynch_5 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [does not occur]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim ccitt509,R Niagree_11 - Ok [proof of correctness]
claim ccitt509,R Nisynch_10 - Ok [proof of correctness]
claim ccitt509,R Secret_9 yr Ok [proof of correctness]
claim ccitt509,R Secret_8 yi Ok [proof of correctness]
claim ccitt509,I Niagree_7 - Ok [proof of correctness]
claim ccitt509,I Nisynch_6 - Ok [proof of correctness]
claim ccitt509,I Secret_5 yr Ok [proof of correctness]
claim ccitt509,I Secret_4 yi Ok [proof of correctness]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [proof of correctness]
claim bunava23,R2 Nisynch_C2 - Ok [does not occur]
claim bunava23,R2 Niagree_C1 - Ok [does not occur]
claim bunava23,R1 Nisynch_B2 - Ok [does not occur]
claim bunava23,R1 Niagree_B1 - Ok [does not occur]
claim bunava23,R0 Nisynch_A2 - Ok [does not occur]
claim bunava23,R0 Niagree_A1 - Ok [does not occur]
claim wmfbrutus,B Secret_3 kab Ok [no attack within bounds]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Ok [does not occur]
claim kaochow2,R Nisynch_8 - Ok [does not occur]
claim kaochow2,I Secret_7 kir Ok [no attack within bounds]
claim kaochow2,I Niagree_6 - Ok [does not occur]
claim kaochow2,I Nisynch_5 - Ok [does not occur]
claim otwayrees,B Nisynch_6b - Fail [at least 1 attack]
claim otwayrees,B Niagree_6a - Fail [at least 1 attack]
claim otwayrees,B Secret_6 kab Ok [proof of correctness]
claim otwayrees,A Nisynch_5c - Fail [at least 1 attack]
claim otwayrees,A Niagree_5b - Fail [at least 1 attack]
claim otwayrees,A Secret_5 kab Ok [proof of correctness]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [no attack within bounds]
claim kaochowPalm,R Nisynch_8 - Ok [no attack within bounds]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Ok [does not occur]
claim kaochowPalm,I Nisynch_5 - Ok [does not occur]
claim as3a,I Nisynch_i1 - Ok [does not occur]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Fail [at least 1 attack]
claim tmn,S Secret_7 Ka Fail [at least 2 attacks]
claim tmn,B Secret_6 Kb Fail [at least 1 attack]
claim tmn,A Secret_8 Kb Fail [at least 1 attack]
claim tmn,A Secret_5 Ka Fail [at least 1 attack]
claim nssymmetricamended,B Nisynch_9b - Ok [does not occur]
claim nssymmetricamended,B Niagree_9a - Ok [does not occur]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Ok [does not occur]
claim nssymmetricamended,A Niagree_8a - Ok [does not occur]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Fail [at least 1 attack]
claim gongnonce,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonce,R Secret_11 kr Ok [no attack within bounds]
claim gongnonce,R Secret_10 ki Ok [no attack within bounds]
claim gongnonce,I Niagree_9 - Fail [at least 1 attack]
claim gongnonce,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonce,I Secret_7 kr Ok [no attack within bounds]
claim gongnonce,I Secret_6 ki Ok [no attack within bounds]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [does not occur]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Ok [does not occur]
claim kaochow,R Nisynch_8 - Ok [does not occur]
claim kaochow,I Secret_7 kir Ok [no attack within bounds]
claim kaochow,I Niagree_6 - Ok [does not occur]
claim kaochow,I Nisynch_5 - Ok [does not occur]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Fail [at least 1 attack]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Ok [no attack within bounds]
claim bkevariation,R Nisynch_9 - Fail [at least 1 attack]
claim bkevariation,R Niagree_8 - Fail [at least 1 attack]
claim bkevariation,R Secret_7 kir Ok [proof of correctness]
claim bkevariation,I Nisynch_6 - Ok [no attack within bounds]
claim bkevariation,I Niagree_5 - Ok [no attack within bounds]
claim bkevariation,I Secret_4 kir Ok [no attack within bounds]
claim yahalomlowe,R Niagree_13 - Ok [does not occur]
claim yahalomlowe,R Nisynch_12 - Ok [does not occur]
claim yahalomlowe,R Secret_11 kir Ok [no attack within bounds]
claim yahalomlowe,I Nisynch_10 - Ok [proof of correctness]
claim yahalomlowe,I Niagree_9 - Ok [proof of correctness]
claim yahalomlowe,I Secret_8 kir Ok [proof of correctness]
claim broken1,R Secret_4 PlainSight Ok [no attack within bounds]
claim bke,R Nisynch_9 - Ok [no attack within bounds]
claim bke,R Niagree_8 - Ok [no attack within bounds]
claim bke,R Secret_7 kir Ok [proof of correctness]
claim bke,I Nisynch_6 - Ok [no attack within bounds]
claim bke,I Niagree_5 - Ok [no attack within bounds]
claim bke,I Secret_4 kir Ok [no attack within bounds]
claim spliceAShcCJ,S Nisynch_12 - Ok [does not occur]
claim spliceAShcCJ,S Niagree_11 - Ok [does not occur]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Ok [does not occur]
claim spliceAShcCJ,C Niagree_9 - Ok [does not occur]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Fail [exactly 1 attack]
claim soph,I Niagree_3 - Ok [proof of correctness]
claim bunava13,R2 Nisynch_C2 - Ok [does not occur]
claim bunava13,R2 Niagree_C1 - Ok [does not occur]
claim bunava13,R1 Nisynch_B2 - Ok [does not occur]
claim bunava13,R1 Niagree_B1 - Ok [does not occur]
claim bunava13,R0 Nisynch_A2 - Ok [does not occur]
claim bunava13,R0 Niagree_A1 - Ok [does not occur]
claim bunava24,A Nisynch_A2 - Ok [does not occur]
claim bunava24,A Niagree_A1 - Ok [does not occur]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Ok [does not occur]
claim kaochow3,R Nisynch_8 - Ok [does not occur]
claim kaochow3,I Secret_7 kir Ok [no attack within bounds]
claim kaochow3,I Niagree_6 - Ok [does not occur]
claim kaochow3,I Nisynch_5 - Ok [does not occur]
claim unknown2,R Secret_r3 kir Ok [no attack within bounds]
claim unknown2,R Niagree_r2 - Ok [does not occur]
claim unknown2,R Nisynch_r1 - Ok [does not occur]
claim unknown2,I Secret_i3 kir Ok [proof of correctness]
claim unknown2,I Niagree_i2 - Ok [does not occur]
claim unknown2,I Nisynch_i1 - Ok [does not occur]
claim localclaims,R Secret_r1 ni Fail [exactly 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Fail [at least 1 attack]
claim ns3speedtest,I Secret_4 nr Ok [no attack within bounds]
claim yahalom,B Secret_6 kab Ok [proof of correctness]
claim yahalom,A Secret_5 kab Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [at least 1 attack]
claim ns3,R Niagree_r3 - Fail [at least 1 attack]
claim ns3,R Secret_r2 nr Fail [at least 1 attack]
claim ns3,R Secret_r1 ni Fail [at least 1 attack]
claim ns3,I Nisynch_i4 - Ok [no attack within bounds]
claim ns3,I Niagree_i3 - Ok [no attack within bounds]
claim ns3,I Secret_i2 nr Ok [no attack within bounds]
claim ns3,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Fail [exactly 1 attack]
claim nsl3rep,R Nisynch_8 - Fail [at least 1 attack]
claim nsl3rep,R Niagree_5 - Ok [no attack within bounds]
claim nsl3rep,I Nisynch_7 - Fail [at least 1 attack]
claim nsl3rep,I Niagree_4 - Ok [proof of correctness]
claim bunava14,D Nisynch_D2 - Ok [does not occur]
claim bunava14,D Niagree_D1 - Ok [does not occur]
claim bunava14,C Nisynch_C2 - Ok [does not occur]
claim bunava14,C Niagree_C1 - Ok [does not occur]
claim bunava14,B Nisynch_B2 - Ok [does not occur]
claim bunava14,B Niagree_B1 - Ok [does not occur]
claim bunava14,A Nisynch_A2 - Ok [does not occur]
claim bunava14,A Niagree_A1 - Ok [does not occur]
claim boydNS,R Nisynch_r4 - Ok [no attack within bounds]
claim boydNS,R Niagree_r3 - Ok [no attack within bounds]
claim boydNS,R Secret_r2 nr Ok [proof of correctness]
claim boydNS,R Secret_r1 ni Ok [no attack within bounds]
claim boydNS,I Nisynch_i4 - Fail [at least 1 attack]
claim boydNS,I Niagree_i3 - Fail [at least 1 attack]
claim boydNS,I Secret_i2 nr Fail [at least 1 attack]
claim boydNS,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [proof of correctness]
claim ibe,R Nisynch_r4 - Ok [no attack within bounds]
claim ibe,R Niagree_r3 - Ok [no attack within bounds]
claim ibe,R Secret_r2 nr Ok [no attack within bounds]
claim ibe,R Secret_r1 ni Ok [no attack within bounds]
claim ibe,I Nisynch_i4 - Ok [no attack within bounds]
claim ibe,I Niagree_i3 - Ok [no attack within bounds]
claim ibe,I Secret_i2 nr Ok [no attack within bounds]
claim ibe,I Secret_i1 ni Ok [no attack within bounds]
claim ibe,R Secret_r1 ni Fail [at least 1 attack]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson-avispa,b Niagree_10c - Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Niagree_9c - Fail [at least 1 attack]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim nsl3th2,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th2,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th1,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th1,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th3,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3th1,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th1,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th3nr,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3nr,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th2,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th2,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th3ni,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3ni,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [no attack within bounds]
claim nsl3,R Niagree_r3 - Ok [no attack within bounds]
claim nsl3,R Secret_r2 nr Ok [no attack within bounds]
claim nsl3,R Secret_r1 ni Ok [no attack within bounds]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [no attack within bounds]
claim nsl3,I Secret_i1 ni Ok [no attack within bounds]
claim ns3,R Nisynch_r4 - Fail [at least 1 attack]
claim ns3,R Niagree_r3 - Fail [at least 1 attack]
claim ns3,R Secret_r2 nr Fail [at least 1 attack]
claim ns3,R Secret_r1 ni Fail [at least 1 attack]
claim ns3,I Nisynch_i4 - Ok [no attack within bounds]
claim ns3,I Niagree_i3 - Ok [no attack within bounds]
claim ns3,I Secret_i2 nr Ok [no attack within bounds]
claim ns3,I Secret_i1 ni Ok [no attack within bounds]

518
test/boundruns3.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [no attack within bounds]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 2 attacks]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [proof of correctness]
claim spliceAS,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS,I Nisynch_10 - Fail [at least 3 attacks]
claim spliceAS,I Niagree_9 - Fail [at least 3 attacks]
claim spliceAS,I Secret_7 N2 Ok [proof of correctness]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-2,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-2,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-2,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-2,I Nisynch_I1 - Fail [at least 2 attacks]
claim yahalom-Lowe,R Nisynch_R2 - Ok [no attack within bounds]
claim yahalom-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim otwayrees,R Nisynch_R2 - Fail [at least 1 attack]
claim otwayrees,R Secret_R1 Kir Ok [proof of correctness]
claim otwayrees,I Nisynch_I2 - Fail [at least 1 attack]
claim otwayrees,I Secret_I1 Kir Ok [proof of correctness]
claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 1 attack]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Fail [at least 4 attacks]
claim kaochow,R Niagree_R2 - Fail [at least 5 attacks]
claim kaochow,R Nisynch_R1 - Fail [at least 5 attacks]
claim kaochow,I Secret_I3 kir Ok [proof of correctness]
claim kaochow,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_I1 - Fail [at least 2 attacks]
claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-HC,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-HC,I Nisynch_10 - Fail [at least 3 attacks]
claim spliceAS-HC,I Niagree_9 - Fail [at least 3 attacks]
claim spliceAS-HC,I Secret_7 N2 Ok [proof of correctness]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [proof of correctness]
claim ccitt509-3,R Secret_R2 Ya Ok [no attack within bounds]
claim ccitt509-3,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness]
claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness]
claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco-Lowe,I Niagree_I1 - Ok [no attack within bounds]
claim yahalom-Paulson,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom-Paulson,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-Paulson,I Nisynch_I2 - Fail [exactly 1 attack]
claim yahalom-Paulson,I Secret_I1 Kir Ok [proof of correctness]
claim woolam,R Nisynch_R2 - Fail [at least 2 attacks]
claim woolam,R Secret_R1 Kir Ok [proof of correctness]
claim woolam,I Nisynch_I2 - Fail [at least 2 attacks]
claim woolam,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub-Hwang,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub-Hwang,R Niagree_R2 - Fail [at least 1 attack]
claim neustub-Hwang,R Secret_R1 Kir Ok [no attack within bounds]
claim neustub-Hwang,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub-Hwang,I Niagree_I2 - Fail [at least 1 attack]
claim neustub-Hwang,I Secret_I1 Kir Ok [proof of correctness]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-3,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-3,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-3,I Nisynch_I1 - Fail [at least 2 attacks]
claim woolamPi,R Nisynch_R1 - Fail [at least 2 attacks]
claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness]
claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
claim ksl,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl,R Niagree_R2 - Fail [at least 1 attack]
claim ksl,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl,I Niagree_I2 - Fail [at least 1 attack]
claim ksl,I Secret_I1 Kir Ok [no attack within bounds]
claim ksl-Lowe,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl-Lowe,R Niagree_R2 - Fail [at least 1 attack]
claim ksl-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl-Lowe,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl-Lowe,I Niagree_I2 - Fail [at least 1 attack]
claim ksl-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 1 attack]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Fail [at least 2 attacks]
claim spliceAS-CJ,R Niagree_11 - Fail [at least 2 attacks]
claim spliceAS-CJ,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-CJ,I Nisynch_10 - Fail [at least 3 attacks]
claim spliceAS-CJ,I Niagree_9 - Fail [at least 3 attacks]
claim spliceAS-CJ,I Secret_7 N2 Ok [proof of correctness]
claim needhamschroedersk-amend,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 1 attack]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Fail [exactly 1 attack]
claim andrew-Concrete,R Secret_R1 kir Ok [proof of correctness]
claim andrew-Concrete,I Nisynch_I2 - Fail [exactly 1 attack]
claim andrew-Concrete,I Secret_I1 kir Ok [proof of correctness]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness]
claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness]
claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [proof of correctness]
claim andrew-Ban,I Niagree_I2 - Ok [no attack within bounds]
claim andrew-Ban,I Nisynch_I1 - Ok [no attack within bounds]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks]
claim yahalom-BAN,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom-BAN,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom-BAN,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom-BAN,I Secret_I1 Kir Ok [proof of correctness]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Fail [at least 1 attack]
claim tmn,I Nisynch_I2 - Fail [at least 2 attacks]
claim tmn,I Secret_I1 Kr Fail [at least 2 attacks]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew,R Niagree_R3 - Ok [proof of correctness]
claim andrew,R Nisynch_R2 - Ok [proof of correctness]
claim andrew,R Secret_R1 kir Ok [proof of correctness]
claim andrew,I Niagree_I3 - Fail [at least 1 attack]
claim andrew,I Nisynch_I2 - Fail [at least 1 attack]
claim andrew,I Secret_I1 kir Fail [exactly 1 attack]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness]
claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Fail [at least 1 attack]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [proof of correctness]
claim yahalom,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom,R Secret_R1 Kir Ok [no attack within bounds]
claim yahalom,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom,I Secret_I1 Kir Ok [proof of correctness]
claim wmf-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroederpk,R Secret_R2 Ni Fail [at least 2 attacks]
claim needhamschroederpk,R Secret_R1 Nr Fail [at least 2 attacks]
claim needhamschroederpk,I Nisynch_I3 - Fail [at least 2 attacks]
claim needhamschroederpk,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk,I Secret_I1 Ni Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub,I Niagree_I2 - Fail [at least 1 attack]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 1 attack]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub,R Niagree_R2 - Fail [at least 1 attack]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [no attack within bounds]
claim neustub^Repeat,R Niagree_R2 - Ok [no attack within bounds]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [no attack within bounds]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [proof of correctness]
claim andrewBan,R Niagree_8b - Ok [proof of correctness]
claim andrewBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [proof of correctness]
claim andrewBan,I Niagree_5b - Ok [no attack within bounds]
claim andrewBan,I Nisynch_5 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [no attack within bounds]
claim nsl3,R Niagree_r3 - Ok [no attack within bounds]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [no attack within bounds]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim bkebroken,R Secret_5 kir Fail [at least 2 attacks]
claim bkebroken,I Secret_4 kir Ok [proof of correctness]
claim spliceAS,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,S Niagree_11 - Fail [at least 1 attack]
claim spliceAS,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAS,C Nisynch_10 - Fail [at least 3 attacks]
claim spliceAS,C Niagree_9 - Fail [at least 3 attacks]
claim spliceAS,C Secret_7 N2 Fail [at least 3 attacks]
claim bkeONE,R Secret_5 kir Ok [proof of correctness]
claim bkeONE,I Secret_4 kir Ok [proof of correctness]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [proof of correctness]
claim nsl7,R Secret_4 ni Ok [proof of correctness]
claim ns3brutus,R Secret_5 ni Fail [at least 1 attack]
claim ns3brutus,I Secret_4 nr Ok [proof of correctness]
claim woolampif,B Nisynch_7 - Fail [at least 1 attack]
claim woolampif,B Niagree_6 - Fail [exactly 1 attack]
claim yahalomBan,B Secret_6 kab Fail [at least 2 attacks]
claim yahalomBan,A Secret_5 kab Fail [at least 1 attack]
claim boyd,R Nisynch_12 - Fail [at least 2 attacks]
claim boyd,R Niagree_11 - Fail [at least 2 attacks]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [proof of correctness]
claim boyd,I Nisynch_8 - Fail [at least 2 attacks]
claim boyd,I Niagree_7 - Fail [at least 2 attacks]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShc,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShc,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShc,C Nisynch_10 - Fail [at least 3 attacks]
claim spliceAShc,C Niagree_9 - Fail [at least 3 attacks]
claim spliceAShc,C Secret_7 N2 Fail [at least 3 attacks]
claim isoiec11770213,R Secret_6 kir Ok [proof of correctness]
claim isoiec11770213,I Secret_5 kir Ok [no attack within bounds]
claim gongnonceb,R Niagree_13 - Fail [at least 1 attack]
claim gongnonceb,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonceb,R Secret_11 kr Ok [no attack within bounds]
claim gongnonceb,R Secret_10 ki Ok [no attack within bounds]
claim gongnonceb,I Niagree_9 - Fail [at least 1 attack]
claim gongnonceb,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonceb,I Secret_7 kr Ok [no attack within bounds]
claim gongnonceb,I Secret_6 ki Ok [no attack within bounds]
claim yahalompaulson,R Niagree_13 - Fail [at least 1 attack]
claim yahalompaulson,R Nisynch_12 - Fail [at least 1 attack]
claim yahalompaulson,R Secret_11 kir Ok [proof of correctness]
claim yahalompaulson,I Niagree_10 - Fail [at least 1 attack]
claim yahalompaulson,I Nisynch_9 - Fail [at least 1 attack]
claim yahalompaulson,I Secret_8 kir Ok [proof of correctness]
claim ksl,B Nisynch_B3 - Fail [at least 1 attack]
claim ksl,B Niagree_B2 - Fail [at least 1 attack]
claim ksl,B Secret_B1 Kab Ok [no attack within bounds]
claim ksl,A Nisynch_A3 - Fail [at least 1 attack]
claim ksl,A Niagree_A2 - Fail [at least 1 attack]
claim ksl,A Secret_A1 Kab Ok [no attack within bounds]
claim denningsaccosh,B Niagree_9 - Ok [no attack within bounds]
claim denningsaccosh,B Nisynch_8 - Fail [at least 1 attack]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Fail [at least 1 attack]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Fail [at least 2 attacks]
claim woolamcmv,B Niagree_12 - Fail [at least 2 attacks]
claim woolamcmv,B Secret_11 Kab Ok [proof of correctness]
claim woolamcmv,A Nisynch_10 - Fail [at least 2 attacks]
claim woolamcmv,A Niagree_9 - Fail [at least 2 attacks]
claim woolamcmv,A Secret_8 Kab Ok [no attack within bounds]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [proof of correctness]
claim andrewLoweBan,R Niagree_8b - Ok [proof of correctness]
claim andrewLoweBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [proof of correctness]
claim andrewLoweBan,I Niagree_5b - Fail [exactly 1 attack]
claim andrewLoweBan,I Nisynch_5 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [proof of correctness]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim ccitt509,R Niagree_11 - Ok [proof of correctness]
claim ccitt509,R Nisynch_10 - Ok [proof of correctness]
claim ccitt509,R Secret_9 yr Ok [proof of correctness]
claim ccitt509,R Secret_8 yi Ok [proof of correctness]
claim ccitt509,I Niagree_7 - Ok [proof of correctness]
claim ccitt509,I Nisynch_6 - Ok [proof of correctness]
claim ccitt509,I Secret_5 yr Ok [proof of correctness]
claim ccitt509,I Secret_4 yi Ok [proof of correctness]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [proof of correctness]
claim bunava23,R2 Nisynch_C2 - Fail [at least 2 attacks]
claim bunava23,R2 Niagree_C1 - Fail [at least 2 attacks]
claim bunava23,R1 Nisynch_B2 - Fail [at least 1 attack]
claim bunava23,R1 Niagree_B1 - Fail [at least 1 attack]
claim bunava23,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava23,R0 Niagree_A1 - Fail [at least 1 attack]
claim wmfbrutus,B Secret_3 kab Ok [no attack within bounds]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow2,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow2,I Secret_7 kir Ok [no attack within bounds]
claim kaochow2,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow2,I Nisynch_5 - Fail [at least 2 attacks]
claim otwayrees,B Nisynch_6b - Fail [at least 1 attack]
claim otwayrees,B Niagree_6a - Fail [at least 1 attack]
claim otwayrees,B Secret_6 kab Ok [proof of correctness]
claim otwayrees,A Nisynch_5c - Fail [at least 1 attack]
claim otwayrees,A Niagree_5b - Fail [at least 1 attack]
claim otwayrees,A Secret_5 kab Ok [proof of correctness]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [no attack within bounds]
claim kaochowPalm,R Nisynch_8 - Ok [no attack within bounds]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Fail [at least 1 attack]
claim kaochowPalm,I Nisynch_5 - Fail [at least 1 attack]
claim as3a,I Nisynch_i1 - Ok [proof of correctness]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Fail [at least 1 attack]
claim tmn,S Secret_7 Ka Fail [at least 3 attacks]
claim tmn,B Secret_6 Kb Fail [at least 1 attack]
claim tmn,A Secret_8 Kb Fail [at least 2 attacks]
claim tmn,A Secret_5 Ka Fail [at least 2 attacks]
claim nssymmetricamended,B Nisynch_9b - Fail [at least 1 attack]
claim nssymmetricamended,B Niagree_9a - Fail [at least 1 attack]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Fail [at least 1 attack]
claim nssymmetricamended,A Niagree_8a - Fail [at least 1 attack]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Fail [at least 1 attack]
claim gongnonce,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonce,R Secret_11 kr Ok [no attack within bounds]
claim gongnonce,R Secret_10 ki Ok [no attack within bounds]
claim gongnonce,I Niagree_9 - Fail [at least 1 attack]
claim gongnonce,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonce,I Secret_7 kr Ok [no attack within bounds]
claim gongnonce,I Secret_6 ki Ok [no attack within bounds]
claim course2r890year0405ex3,I Nisynch_i2 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow,I Secret_7 kir Ok [proof of correctness]
claim kaochow,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_5 - Fail [at least 2 attacks]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Fail [at least 3 attacks]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Fail [at least 1 attack]
claim bkevariation,R Nisynch_9 - Fail [at least 1 attack]
claim bkevariation,R Niagree_8 - Fail [at least 1 attack]
claim bkevariation,R Secret_7 kir Ok [proof of correctness]
claim bkevariation,I Nisynch_6 - Ok [proof of correctness]
claim bkevariation,I Niagree_5 - Ok [proof of correctness]
claim bkevariation,I Secret_4 kir Ok [proof of correctness]
claim yahalomlowe,R Niagree_13 - Ok [proof of correctness]
claim yahalomlowe,R Nisynch_12 - Ok [proof of correctness]
claim yahalomlowe,R Secret_11 kir Ok [proof of correctness]
claim yahalomlowe,I Nisynch_10 - Ok [proof of correctness]
claim yahalomlowe,I Niagree_9 - Ok [proof of correctness]
claim yahalomlowe,I Secret_8 kir Ok [proof of correctness]
claim broken1,R Secret_4 PlainSight Fail [at least 1 attack]
claim bke,R Nisynch_9 - Ok [proof of correctness]
claim bke,R Niagree_8 - Ok [proof of correctness]
claim bke,R Secret_7 kir Ok [proof of correctness]
claim bke,I Nisynch_6 - Ok [proof of correctness]
claim bke,I Niagree_5 - Ok [proof of correctness]
claim bke,I Secret_4 kir Ok [proof of correctness]
claim spliceAShcCJ,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShcCJ,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Fail [at least 3 attacks]
claim spliceAShcCJ,C Niagree_9 - Fail [at least 3 attacks]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Fail [exactly 1 attack]
claim soph,I Niagree_3 - Ok [proof of correctness]
claim bunava13,R2 Nisynch_C2 - Ok [no attack within bounds]
claim bunava13,R2 Niagree_C1 - Ok [no attack within bounds]
claim bunava13,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava13,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava13,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava13,R0 Niagree_A1 - Fail [at least 1 attack]
claim bunava24,A Nisynch_A2 - Ok [does not occur]
claim bunava24,A Niagree_A1 - Ok [does not occur]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow3,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow3,I Secret_7 kir Ok [no attack within bounds]
claim kaochow3,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow3,I Nisynch_5 - Fail [at least 2 attacks]
claim unknown2,R Secret_r3 kir Ok [proof of correctness]
claim unknown2,R Niagree_r2 - Fail [at least 2 attacks]
claim unknown2,R Nisynch_r1 - Fail [at least 2 attacks]
claim unknown2,I Secret_i3 kir Ok [proof of correctness]
claim unknown2,I Niagree_i2 - Fail [at least 1 attack]
claim unknown2,I Nisynch_i1 - Fail [at least 1 attack]
claim localclaims,R Secret_r1 ni Fail [exactly 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Fail [at least 1 attack]
claim ns3speedtest,I Secret_4 nr Ok [proof of correctness]
claim yahalom,B Secret_6 kab Ok [proof of correctness]
claim yahalom,A Secret_5 kab Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [at least 1 attack]
claim ns3,R Niagree_r3 - Fail [at least 1 attack]
claim ns3,R Secret_r2 nr Fail [at least 1 attack]
claim ns3,R Secret_r1 ni Fail [at least 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Fail [exactly 1 attack]
claim nsl3rep,R Nisynch_8 - Fail [at least 1 attack]
claim nsl3rep,R Niagree_5 - Ok [no attack within bounds]
claim nsl3rep,I Nisynch_7 - Fail [at least 1 attack]
claim nsl3rep,I Niagree_4 - Ok [proof of correctness]
claim bunava14,D Nisynch_D2 - Ok [does not occur]
claim bunava14,D Niagree_D1 - Ok [does not occur]
claim bunava14,C Nisynch_C2 - Ok [does not occur]
claim bunava14,C Niagree_C1 - Ok [does not occur]
claim bunava14,B Nisynch_B2 - Ok [does not occur]
claim bunava14,B Niagree_B1 - Ok [does not occur]
claim bunava14,A Nisynch_A2 - Ok [does not occur]
claim bunava14,A Niagree_A1 - Ok [does not occur]
claim boydNS,R Nisynch_r4 - Fail [at least 1 attack]
claim boydNS,R Niagree_r3 - Fail [at least 1 attack]
claim boydNS,R Secret_r2 nr Ok [proof of correctness]
claim boydNS,R Secret_r1 ni Fail [at least 1 attack]
claim boydNS,I Nisynch_i4 - Fail [at least 2 attacks]
claim boydNS,I Niagree_i3 - Fail [at least 2 attacks]
claim boydNS,I Secret_i2 nr Fail [exactly 1 attack]
claim boydNS,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [proof of correctness]
claim ibe,R Nisynch_r4 - Ok [no attack within bounds]
claim ibe,R Niagree_r3 - Ok [no attack within bounds]
claim ibe,R Secret_r2 nr Ok [no attack within bounds]
claim ibe,R Secret_r1 ni Ok [no attack within bounds]
claim ibe,I Nisynch_i4 - Ok [proof of correctness]
claim ibe,I Niagree_i3 - Ok [proof of correctness]
claim ibe,I Secret_i2 nr Ok [proof of correctness]
claim ibe,I Secret_i1 ni Ok [no attack within bounds]
claim ibe,R Secret_r1 ni Fail [at least 1 attack]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson-avispa,b Niagree_10c - Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Niagree_9c - Fail [at least 1 attack]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim nsl3th2,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th2,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th1,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th1,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th3,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3th1,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th1,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th3nr,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3nr,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th2,R Nisynch_r - Ok [no attack within bounds]
claim nsl3th2,I Nisynch_i - Ok [no attack within bounds]
claim nsl3th3ni,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3ni,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [no attack within bounds]
claim nsl3,R Niagree_r3 - Ok [no attack within bounds]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [no attack within bounds]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [at least 1 attack]
claim ns3,R Niagree_r3 - Fail [at least 1 attack]
claim ns3,R Secret_r2 nr Fail [at least 1 attack]
claim ns3,R Secret_r1 ni Fail [at least 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]

518
test/boundruns4.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [proof of correctness]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [proof of correctness]
claim spliceAS,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS,I Secret_7 N2 Ok [proof of correctness]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-2,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-2,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-2,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-2,I Nisynch_I1 - Fail [at least 2 attacks]
claim yahalom-Lowe,R Nisynch_R2 - Ok [no attack within bounds]
claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim otwayrees,R Nisynch_R2 - Fail [at least 1 attack]
claim otwayrees,R Secret_R1 Kir Ok [proof of correctness]
claim otwayrees,I Nisynch_I2 - Fail [at least 1 attack]
claim otwayrees,I Secret_I1 Kir Ok [proof of correctness]
claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Fail [at least 5 attacks]
claim kaochow,R Niagree_R2 - Fail [at least 6 attacks]
claim kaochow,R Nisynch_R1 - Fail [at least 6 attacks]
claim kaochow,I Secret_I3 kir Ok [proof of correctness]
claim kaochow,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_I1 - Fail [at least 2 attacks]
claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-HC,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-HC,I Secret_7 N2 Ok [proof of correctness]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [proof of correctness]
claim ccitt509-3,R Secret_R2 Ya Ok [proof of correctness]
claim ccitt509-3,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness]
claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness]
claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco-Lowe,I Niagree_I1 - Ok [no attack within bounds]
claim yahalom-Paulson,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom-Paulson,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Paulson,I Nisynch_I2 - Fail [exactly 1 attack]
claim yahalom-Paulson,I Secret_I1 Kir Ok [proof of correctness]
claim woolam,R Nisynch_R2 - Fail [at least 2 attacks]
claim woolam,R Secret_R1 Kir Ok [proof of correctness]
claim woolam,I Nisynch_I2 - Fail [at least 2 attacks]
claim woolam,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-Hwang,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub-Hwang,R Niagree_R2 - Fail [at least 1 attack]
claim neustub-Hwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-Hwang,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub-Hwang,I Niagree_I2 - Fail [at least 1 attack]
claim neustub-Hwang,I Secret_I1 Kir Ok [proof of correctness]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-3,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-3,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-3,I Nisynch_I1 - Fail [at least 2 attacks]
claim woolamPi,R Nisynch_R1 - Fail [at least 3 attacks]
claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness]
claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
claim ksl,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl,R Niagree_R2 - Fail [at least 1 attack]
claim ksl,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl,I Niagree_I2 - Fail [at least 1 attack]
claim ksl,I Secret_I1 Kir Ok [no attack within bounds]
claim ksl-Lowe,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl-Lowe,R Niagree_R2 - Fail [at least 1 attack]
claim ksl-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim ksl-Lowe,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl-Lowe,I Niagree_I2 - Fail [at least 1 attack]
claim ksl-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-CJ,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-CJ,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-CJ,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-CJ,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-CJ,I Secret_7 N2 Ok [proof of correctness]
claim needhamschroedersk-amend,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Fail [exactly 1 attack]
claim andrew-Concrete,R Secret_R1 kir Ok [proof of correctness]
claim andrew-Concrete,I Nisynch_I2 - Fail [exactly 1 attack]
claim andrew-Concrete,I Secret_I1 kir Ok [proof of correctness]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness]
claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness]
claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [proof of correctness]
claim andrew-Ban,I Niagree_I2 - Ok [proof of correctness]
claim andrew-Ban,I Nisynch_I1 - Ok [proof of correctness]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks]
claim yahalom-BAN,R Nisynch_R2 - Fail [at least 2 attacks]
claim yahalom-BAN,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-BAN,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom-BAN,I Secret_I1 Kir Ok [proof of correctness]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Fail [at least 3 attacks]
claim tmn,I Nisynch_I2 - Fail [at least 2 attacks]
claim tmn,I Secret_I1 Kr Fail [at least 4 attacks]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew,R Niagree_R3 - Ok [proof of correctness]
claim andrew,R Nisynch_R2 - Ok [proof of correctness]
claim andrew,R Secret_R1 kir Ok [proof of correctness]
claim andrew,I Niagree_I3 - Fail [at least 2 attacks]
claim andrew,I Nisynch_I2 - Fail [at least 2 attacks]
claim andrew,I Secret_I1 kir Fail [exactly 1 attack]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness]
claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Fail [at least 2 attacks]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [proof of correctness]
claim yahalom,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom,I Secret_I1 Kir Ok [proof of correctness]
claim wmf-Lowe,R Nisynch_R2 - Fail [at least 2 attacks]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Fail [at least 2 attacks]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk,R Secret_R2 Ni Fail [at least 5 attacks]
claim needhamschroederpk,R Secret_R1 Nr Fail [at least 5 attacks]
claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk,I Secret_I1 Ni Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Fail [exactly 1 attack]
claim neustub,I Niagree_I2 - Fail [exactly 1 attack]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub,R Niagree_R2 - Fail [at least 1 attack]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [proof of correctness]
claim andrewBan,R Niagree_8b - Ok [proof of correctness]
claim andrewBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [proof of correctness]
claim andrewBan,I Niagree_5b - Ok [proof of correctness]
claim andrewBan,I Nisynch_5 - Ok [proof of correctness]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim bkebroken,R Secret_5 kir Fail [at least 2 attacks]
claim bkebroken,I Secret_4 kir Ok [proof of correctness]
claim spliceAS,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,S Niagree_11 - Fail [at least 1 attack]
claim spliceAS,S Secret_8 N2 Fail [at least 5 attacks]
claim spliceAS,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,C Niagree_9 - Fail [at least 1 attack]
claim spliceAS,C Secret_7 N2 Fail [at least 5 attacks]
claim bkeONE,R Secret_5 kir Ok [proof of correctness]
claim bkeONE,I Secret_4 kir Ok [proof of correctness]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [proof of correctness]
claim nsl7,R Secret_4 ni Ok [proof of correctness]
claim ns3brutus,R Secret_5 ni Fail [exactly 1 attack]
claim ns3brutus,I Secret_4 nr Ok [proof of correctness]
claim woolampif,B Nisynch_7 - Fail [at least 1 attack]
claim woolampif,B Niagree_6 - Fail [exactly 1 attack]
claim yahalomBan,B Secret_6 kab Fail [at least 2 attacks]
claim yahalomBan,A Secret_5 kab Fail [at least 1 attack]
claim boyd,R Nisynch_12 - Fail [at least 2 attacks]
claim boyd,R Niagree_11 - Fail [at least 2 attacks]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [proof of correctness]
claim boyd,I Nisynch_8 - Fail [at least 2 attacks]
claim boyd,I Niagree_7 - Fail [at least 2 attacks]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShc,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShc,S Secret_8 N2 Fail [at least 5 attacks]
claim spliceAShc,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShc,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShc,C Secret_7 N2 Fail [at least 5 attacks]
claim isoiec11770213,R Secret_6 kir Ok [proof of correctness]
claim isoiec11770213,I Secret_5 kir Ok [no attack within bounds]
claim gongnonceb,R Niagree_13 - Fail [at least 2 attacks]
claim gongnonceb,R Nisynch_12 - Fail [at least 2 attacks]
claim gongnonceb,R Secret_11 kr Ok [no attack within bounds]
claim gongnonceb,R Secret_10 ki Ok [no attack within bounds]
claim gongnonceb,I Niagree_9 - Fail [at least 2 attacks]
claim gongnonceb,I Nisynch_8 - Fail [at least 2 attacks]
claim gongnonceb,I Secret_7 kr Ok [no attack within bounds]
claim gongnonceb,I Secret_6 ki Ok [no attack within bounds]
claim yahalompaulson,R Niagree_13 - Fail [at least 1 attack]
claim yahalompaulson,R Nisynch_12 - Fail [at least 1 attack]
claim yahalompaulson,R Secret_11 kir Ok [proof of correctness]
claim yahalompaulson,I Niagree_10 - Fail [exactly 1 attack]
claim yahalompaulson,I Nisynch_9 - Fail [exactly 1 attack]
claim yahalompaulson,I Secret_8 kir Ok [proof of correctness]
claim ksl,B Nisynch_B3 - Fail [at least 1 attack]
claim ksl,B Niagree_B2 - Fail [at least 1 attack]
claim ksl,B Secret_B1 Kab Ok [no attack within bounds]
claim ksl,A Nisynch_A3 - Fail [at least 1 attack]
claim ksl,A Niagree_A2 - Fail [at least 1 attack]
claim ksl,A Secret_A1 Kab Ok [no attack within bounds]
claim denningsaccosh,B Niagree_9 - Ok [no attack within bounds]
claim denningsaccosh,B Nisynch_8 - Fail [at least 1 attack]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Fail [at least 1 attack]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Fail [at least 2 attacks]
claim woolamcmv,B Niagree_12 - Fail [at least 2 attacks]
claim woolamcmv,B Secret_11 Kab Ok [proof of correctness]
claim woolamcmv,A Nisynch_10 - Fail [at least 2 attacks]
claim woolamcmv,A Niagree_9 - Fail [at least 2 attacks]
claim woolamcmv,A Secret_8 Kab Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [proof of correctness]
claim andrewLoweBan,R Niagree_8b - Ok [proof of correctness]
claim andrewLoweBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [proof of correctness]
claim andrewLoweBan,I Niagree_5b - Fail [exactly 1 attack]
claim andrewLoweBan,I Nisynch_5 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [proof of correctness]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim ccitt509,R Niagree_11 - Ok [proof of correctness]
claim ccitt509,R Nisynch_10 - Ok [proof of correctness]
claim ccitt509,R Secret_9 yr Ok [proof of correctness]
claim ccitt509,R Secret_8 yi Ok [proof of correctness]
claim ccitt509,I Niagree_7 - Ok [proof of correctness]
claim ccitt509,I Nisynch_6 - Ok [proof of correctness]
claim ccitt509,I Secret_5 yr Ok [proof of correctness]
claim ccitt509,I Secret_4 yi Ok [proof of correctness]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [proof of correctness]
claim bunava23,R2 Nisynch_C2 - Fail [at least 3 attacks]
claim bunava23,R2 Niagree_C1 - Fail [at least 3 attacks]
claim bunava23,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava23,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava23,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava23,R0 Niagree_A1 - Fail [at least 1 attack]
claim wmfbrutus,B Secret_3 kab Ok [proof of correctness]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow2,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow2,I Secret_7 kir Ok [no attack within bounds]
claim kaochow2,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow2,I Nisynch_5 - Fail [at least 2 attacks]
claim otwayrees,B Nisynch_6b - Fail [at least 1 attack]
claim otwayrees,B Niagree_6a - Fail [at least 1 attack]
claim otwayrees,B Secret_6 kab Ok [proof of correctness]
claim otwayrees,A Nisynch_5c - Fail [at least 1 attack]
claim otwayrees,A Niagree_5b - Fail [at least 1 attack]
claim otwayrees,A Secret_5 kab Ok [proof of correctness]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [no attack within bounds]
claim kaochowPalm,R Nisynch_8 - Ok [no attack within bounds]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Fail [at least 1 attack]
claim kaochowPalm,I Nisynch_5 - Fail [at least 1 attack]
claim as3a,I Nisynch_i1 - Ok [proof of correctness]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Fail [at least 2 attacks]
claim tmn,S Secret_7 Ka Fail [at least 3 attacks]
claim tmn,B Secret_6 Kb Fail [at least 2 attacks]
claim tmn,A Secret_8 Kb Fail [at least 4 attacks]
claim tmn,A Secret_5 Ka Fail [at least 3 attacks]
claim nssymmetricamended,B Nisynch_9b - Fail [at least 1 attack]
claim nssymmetricamended,B Niagree_9a - Fail [at least 1 attack]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Fail [at least 1 attack]
claim nssymmetricamended,A Niagree_8a - Fail [at least 1 attack]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Fail [at least 1 attack]
claim gongnonce,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonce,R Secret_11 kr Ok [no attack within bounds]
claim gongnonce,R Secret_10 ki Ok [no attack within bounds]
claim gongnonce,I Niagree_9 - Fail [at least 1 attack]
claim gongnonce,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonce,I Secret_7 kr Ok [no attack within bounds]
claim gongnonce,I Secret_6 ki Ok [no attack within bounds]
claim course2r890year0405ex3,I Nisynch_i2 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow,I Secret_7 kir Ok [proof of correctness]
claim kaochow,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_5 - Fail [at least 2 attacks]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Fail [at least 3 attacks]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Fail [at least 1 attack]
claim bkevariation,R Nisynch_9 - Fail [at least 1 attack]
claim bkevariation,R Niagree_8 - Fail [at least 1 attack]
claim bkevariation,R Secret_7 kir Ok [proof of correctness]
claim bkevariation,I Nisynch_6 - Ok [proof of correctness]
claim bkevariation,I Niagree_5 - Ok [proof of correctness]
claim bkevariation,I Secret_4 kir Ok [proof of correctness]
claim yahalomlowe,R Niagree_13 - Ok [proof of correctness]
claim yahalomlowe,R Nisynch_12 - Ok [proof of correctness]
claim yahalomlowe,R Secret_11 kir Ok [proof of correctness]
claim yahalomlowe,I Nisynch_10 - Ok [proof of correctness]
claim yahalomlowe,I Niagree_9 - Ok [proof of correctness]
claim yahalomlowe,I Secret_8 kir Ok [proof of correctness]
claim broken1,R Secret_4 PlainSight Fail [at least 1 attack]
claim bke,R Nisynch_9 - Ok [proof of correctness]
claim bke,R Niagree_8 - Ok [proof of correctness]
claim bke,R Secret_7 kir Ok [proof of correctness]
claim bke,I Nisynch_6 - Ok [proof of correctness]
claim bke,I Niagree_5 - Ok [proof of correctness]
claim bke,I Secret_4 kir Ok [proof of correctness]
claim spliceAShcCJ,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShcCJ,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShcCJ,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Fail [exactly 1 attack]
claim soph,I Niagree_3 - Ok [proof of correctness]
claim bunava13,R2 Nisynch_C2 - Fail [at least 2 attacks]
claim bunava13,R2 Niagree_C1 - Fail [at least 2 attacks]
claim bunava13,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava13,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava13,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava13,R0 Niagree_A1 - Fail [at least 1 attack]
claim bunava24,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava24,A Niagree_A1 - Fail [at least 1 attack]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow3,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow3,I Secret_7 kir Ok [no attack within bounds]
claim kaochow3,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow3,I Nisynch_5 - Fail [at least 2 attacks]
claim unknown2,R Secret_r3 kir Ok [proof of correctness]
claim unknown2,R Niagree_r2 - Fail [at least 2 attacks]
claim unknown2,R Nisynch_r1 - Fail [at least 2 attacks]
claim unknown2,I Secret_i3 kir Ok [proof of correctness]
claim unknown2,I Niagree_i2 - Fail [at least 1 attack]
claim unknown2,I Nisynch_i1 - Fail [at least 1 attack]
claim localclaims,R Secret_r1 ni Fail [exactly 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Fail [exactly 1 attack]
claim ns3speedtest,I Secret_4 nr Ok [proof of correctness]
claim yahalom,B Secret_6 kab Ok [proof of correctness]
claim yahalom,A Secret_5 kab Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [at least 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Fail [exactly 1 attack]
claim nsl3rep,R Nisynch_8 - Fail [at least 1 attack]
claim nsl3rep,R Niagree_5 - Ok [proof of correctness]
claim nsl3rep,I Nisynch_7 - Fail [at least 1 attack]
claim nsl3rep,I Niagree_4 - Ok [proof of correctness]
claim bunava14,D Nisynch_D2 - Ok [no attack within bounds]
claim bunava14,D Niagree_D1 - Ok [no attack within bounds]
claim bunava14,C Nisynch_C2 - Fail [at least 1 attack]
claim bunava14,C Niagree_C1 - Fail [at least 1 attack]
claim bunava14,B Nisynch_B2 - Fail [at least 2 attacks]
claim bunava14,B Niagree_B1 - Fail [at least 2 attacks]
claim bunava14,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava14,A Niagree_A1 - Fail [at least 1 attack]
claim boydNS,R Nisynch_r4 - Fail [at least 1 attack]
claim boydNS,R Niagree_r3 - Fail [at least 1 attack]
claim boydNS,R Secret_r2 nr Ok [proof of correctness]
claim boydNS,R Secret_r1 ni Fail [exactly 1 attack]
claim boydNS,I Nisynch_i4 - Fail [at least 2 attacks]
claim boydNS,I Niagree_i3 - Fail [at least 2 attacks]
claim boydNS,I Secret_i2 nr Fail [exactly 1 attack]
claim boydNS,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [proof of correctness]
claim ibe,R Nisynch_r4 - Ok [proof of correctness]
claim ibe,R Niagree_r3 - Ok [proof of correctness]
claim ibe,R Secret_r2 nr Ok [proof of correctness]
claim ibe,R Secret_r1 ni Ok [proof of correctness]
claim ibe,I Nisynch_i4 - Ok [proof of correctness]
claim ibe,I Niagree_i3 - Ok [proof of correctness]
claim ibe,I Secret_i2 nr Ok [proof of correctness]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim ibe,R Secret_r1 ni Fail [at least 1 attack]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson-avispa,b Niagree_10c - Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Niagree_9c - Fail [at least 1 attack]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3nr,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3nr,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3ni,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3ni,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [at least 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]

518
test/boundruns5.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [proof of correctness]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [proof of correctness]
claim spliceAS,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS,I Secret_7 N2 Ok [proof of correctness]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-2,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-2,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-2,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-2,I Nisynch_I1 - Fail [at least 2 attacks]
claim yahalom-Lowe,R Nisynch_R2 - Ok [proof of correctness]
claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim otwayrees,R Nisynch_R2 - Fail [at least 1 attack]
claim otwayrees,R Secret_R1 Kir Ok [proof of correctness]
claim otwayrees,I Nisynch_I2 - Fail [at least 1 attack]
claim otwayrees,I Secret_I1 Kir Ok [proof of correctness]
claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Fail [at least 5 attacks]
claim kaochow,R Niagree_R2 - Fail [at least 6 attacks]
claim kaochow,R Nisynch_R1 - Fail [at least 6 attacks]
claim kaochow,I Secret_I3 kir Ok [proof of correctness]
claim kaochow,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_I1 - Fail [at least 2 attacks]
claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-HC,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-HC,I Secret_7 N2 Ok [proof of correctness]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [proof of correctness]
claim ccitt509-3,R Secret_R2 Ya Ok [proof of correctness]
claim ccitt509-3,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness]
claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness]
claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco-Lowe,I Niagree_I1 - Ok [no attack within bounds]
claim yahalom-Paulson,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom-Paulson,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Paulson,I Nisynch_I2 - Fail [exactly 1 attack]
claim yahalom-Paulson,I Secret_I1 Kir Ok [proof of correctness]
claim woolam,R Nisynch_R2 - Fail [at least 2 attacks]
claim woolam,R Secret_R1 Kir Ok [proof of correctness]
claim woolam,I Nisynch_I2 - Fail [at least 2 attacks]
claim woolam,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-Hwang,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub-Hwang,R Niagree_R2 - Fail [at least 1 attack]
claim neustub-Hwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-Hwang,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub-Hwang,I Niagree_I2 - Fail [at least 1 attack]
claim neustub-Hwang,I Secret_I1 Kir Ok [proof of correctness]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-3,I Secret_I3 kir Ok [no attack within bounds]
claim kaochow-3,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-3,I Nisynch_I1 - Fail [at least 2 attacks]
claim woolamPi,R Nisynch_R1 - Fail [at least 3 attacks]
claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness]
claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
claim ksl,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl,R Niagree_R2 - Fail [at least 1 attack]
claim ksl,R Secret_R1 Kir Ok [proof of correctness]
claim ksl,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl,I Niagree_I2 - Fail [at least 1 attack]
claim ksl,I Secret_I1 Kir Ok [proof of correctness]
claim ksl-Lowe,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl-Lowe,R Niagree_R2 - Fail [at least 1 attack]
claim ksl-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim ksl-Lowe,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl-Lowe,I Niagree_I2 - Fail [at least 1 attack]
claim ksl-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-CJ,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-CJ,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-CJ,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-CJ,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-CJ,I Secret_7 N2 Ok [proof of correctness]
claim needhamschroedersk-amend,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Fail [exactly 1 attack]
claim andrew-Concrete,R Secret_R1 kir Ok [proof of correctness]
claim andrew-Concrete,I Nisynch_I2 - Fail [exactly 1 attack]
claim andrew-Concrete,I Secret_I1 kir Ok [proof of correctness]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness]
claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness]
claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [proof of correctness]
claim andrew-Ban,I Niagree_I2 - Ok [proof of correctness]
claim andrew-Ban,I Nisynch_I1 - Ok [proof of correctness]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks]
claim yahalom-BAN,R Nisynch_R2 - Fail [at least 2 attacks]
claim yahalom-BAN,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-BAN,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom-BAN,I Secret_I1 Kir Ok [proof of correctness]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Fail [at least 3 attacks]
claim tmn,I Nisynch_I2 - Fail [at least 2 attacks]
claim tmn,I Secret_I1 Kr Fail [at least 4 attacks]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew,R Niagree_R3 - Ok [proof of correctness]
claim andrew,R Nisynch_R2 - Ok [proof of correctness]
claim andrew,R Secret_R1 kir Ok [proof of correctness]
claim andrew,I Niagree_I3 - Fail [at least 2 attacks]
claim andrew,I Nisynch_I2 - Fail [at least 2 attacks]
claim andrew,I Secret_I1 kir Fail [exactly 1 attack]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness]
claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Fail [at least 3 attacks]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [proof of correctness]
claim yahalom,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom,I Secret_I1 Kir Ok [proof of correctness]
claim wmf-Lowe,R Nisynch_R2 - Fail [at least 3 attacks]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Fail [at least 3 attacks]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk,R Secret_R2 Ni Fail [at least 7 attacks]
claim needhamschroederpk,R Secret_R1 Nr Fail [at least 7 attacks]
claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk,I Secret_I1 Ni Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Fail [exactly 1 attack]
claim neustub,I Niagree_I2 - Fail [exactly 1 attack]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub,R Niagree_R2 - Fail [at least 1 attack]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [proof of correctness]
claim andrewBan,R Niagree_8b - Ok [proof of correctness]
claim andrewBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [proof of correctness]
claim andrewBan,I Niagree_5b - Ok [proof of correctness]
claim andrewBan,I Nisynch_5 - Ok [proof of correctness]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim bkebroken,R Secret_5 kir Fail [at least 2 attacks]
claim bkebroken,I Secret_4 kir Ok [proof of correctness]
claim spliceAS,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,S Niagree_11 - Fail [at least 1 attack]
claim spliceAS,S Secret_8 N2 Fail [at least 6 attacks]
claim spliceAS,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,C Niagree_9 - Fail [at least 1 attack]
claim spliceAS,C Secret_7 N2 Fail [at least 7 attacks]
claim bkeONE,R Secret_5 kir Ok [proof of correctness]
claim bkeONE,I Secret_4 kir Ok [proof of correctness]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [proof of correctness]
claim nsl7,R Secret_4 ni Ok [proof of correctness]
claim ns3brutus,R Secret_5 ni Fail [exactly 1 attack]
claim ns3brutus,I Secret_4 nr Ok [proof of correctness]
claim woolampif,B Nisynch_7 - Fail [at least 1 attack]
claim woolampif,B Niagree_6 - Fail [exactly 1 attack]
claim yahalomBan,B Secret_6 kab Fail [at least 2 attacks]
claim yahalomBan,A Secret_5 kab Fail [at least 1 attack]
claim boyd,R Nisynch_12 - Fail [at least 2 attacks]
claim boyd,R Niagree_11 - Fail [at least 2 attacks]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [proof of correctness]
claim boyd,I Nisynch_8 - Fail [at least 2 attacks]
claim boyd,I Niagree_7 - Fail [at least 2 attacks]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShc,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShc,S Secret_8 N2 Fail [at least 7 attacks]
claim spliceAShc,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShc,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShc,C Secret_7 N2 Fail [at least 7 attacks]
claim isoiec11770213,R Secret_6 kir Ok [proof of correctness]
claim isoiec11770213,I Secret_5 kir Ok [proof of correctness]
claim gongnonceb,R Niagree_13 - Fail [at least 2 attacks]
claim gongnonceb,R Nisynch_12 - Fail [at least 2 attacks]
claim gongnonceb,R Secret_11 kr Ok [proof of correctness]
claim gongnonceb,R Secret_10 ki Ok [proof of correctness]
claim gongnonceb,I Niagree_9 - Fail [at least 2 attacks]
claim gongnonceb,I Nisynch_8 - Fail [at least 2 attacks]
claim gongnonceb,I Secret_7 kr Ok [proof of correctness]
claim gongnonceb,I Secret_6 ki Ok [proof of correctness]
claim yahalompaulson,R Niagree_13 - Fail [at least 1 attack]
claim yahalompaulson,R Nisynch_12 - Fail [at least 1 attack]
claim yahalompaulson,R Secret_11 kir Ok [proof of correctness]
claim yahalompaulson,I Niagree_10 - Fail [exactly 1 attack]
claim yahalompaulson,I Nisynch_9 - Fail [exactly 1 attack]
claim yahalompaulson,I Secret_8 kir Ok [proof of correctness]
claim ksl,B Nisynch_B3 - Fail [at least 1 attack]
claim ksl,B Niagree_B2 - Fail [at least 1 attack]
claim ksl,B Secret_B1 Kab Ok [proof of correctness]
claim ksl,A Nisynch_A3 - Fail [at least 1 attack]
claim ksl,A Niagree_A2 - Fail [at least 1 attack]
claim ksl,A Secret_A1 Kab Ok [proof of correctness]
claim denningsaccosh,B Niagree_9 - Ok [no attack within bounds]
claim denningsaccosh,B Nisynch_8 - Fail [at least 1 attack]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Fail [at least 1 attack]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Fail [at least 2 attacks]
claim woolamcmv,B Niagree_12 - Fail [at least 2 attacks]
claim woolamcmv,B Secret_11 Kab Ok [proof of correctness]
claim woolamcmv,A Nisynch_10 - Fail [at least 2 attacks]
claim woolamcmv,A Niagree_9 - Fail [at least 2 attacks]
claim woolamcmv,A Secret_8 Kab Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [proof of correctness]
claim andrewLoweBan,R Niagree_8b - Ok [proof of correctness]
claim andrewLoweBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [proof of correctness]
claim andrewLoweBan,I Niagree_5b - Fail [exactly 1 attack]
claim andrewLoweBan,I Nisynch_5 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [proof of correctness]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim ccitt509,R Niagree_11 - Ok [proof of correctness]
claim ccitt509,R Nisynch_10 - Ok [proof of correctness]
claim ccitt509,R Secret_9 yr Ok [proof of correctness]
claim ccitt509,R Secret_8 yi Ok [proof of correctness]
claim ccitt509,I Niagree_7 - Ok [proof of correctness]
claim ccitt509,I Nisynch_6 - Ok [proof of correctness]
claim ccitt509,I Secret_5 yr Ok [proof of correctness]
claim ccitt509,I Secret_4 yi Ok [proof of correctness]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [proof of correctness]
claim bunava23,R2 Nisynch_C2 - Fail [at least 3 attacks]
claim bunava23,R2 Niagree_C1 - Fail [at least 3 attacks]
claim bunava23,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava23,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava23,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava23,R0 Niagree_A1 - Fail [at least 1 attack]
claim wmfbrutus,B Secret_3 kab Ok [proof of correctness]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow2,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow2,I Secret_7 kir Ok [no attack within bounds]
claim kaochow2,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow2,I Nisynch_5 - Fail [at least 2 attacks]
claim otwayrees,B Nisynch_6b - Fail [at least 1 attack]
claim otwayrees,B Niagree_6a - Fail [at least 1 attack]
claim otwayrees,B Secret_6 kab Ok [proof of correctness]
claim otwayrees,A Nisynch_5c - Fail [at least 1 attack]
claim otwayrees,A Niagree_5b - Fail [at least 1 attack]
claim otwayrees,A Secret_5 kab Ok [proof of correctness]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [no attack within bounds]
claim kaochowPalm,R Nisynch_8 - Ok [no attack within bounds]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Fail [at least 1 attack]
claim kaochowPalm,I Nisynch_5 - Fail [at least 1 attack]
claim as3a,I Nisynch_i1 - Ok [proof of correctness]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Fail [at least 2 attacks]
claim tmn,S Secret_7 Ka Fail [at least 4 attacks]
claim tmn,B Secret_6 Kb Fail [at least 2 attacks]
claim tmn,A Secret_8 Kb Fail [at least 4 attacks]
claim tmn,A Secret_5 Ka Fail [at least 4 attacks]
claim nssymmetricamended,B Nisynch_9b - Fail [at least 1 attack]
claim nssymmetricamended,B Niagree_9a - Fail [at least 1 attack]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Fail [at least 1 attack]
claim nssymmetricamended,A Niagree_8a - Fail [at least 1 attack]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Fail [at least 1 attack]
claim gongnonce,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonce,R Secret_11 kr Ok [proof of correctness]
claim gongnonce,R Secret_10 ki Ok [no attack within bounds]
claim gongnonce,I Niagree_9 - Fail [at least 1 attack]
claim gongnonce,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonce,I Secret_7 kr Ok [no attack within bounds]
claim gongnonce,I Secret_6 ki Ok [proof of correctness]
claim course2r890year0405ex3,I Nisynch_i2 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow,I Secret_7 kir Ok [proof of correctness]
claim kaochow,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_5 - Fail [at least 2 attacks]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Fail [at least 3 attacks]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Fail [at least 1 attack]
claim bkevariation,R Nisynch_9 - Fail [at least 1 attack]
claim bkevariation,R Niagree_8 - Fail [at least 1 attack]
claim bkevariation,R Secret_7 kir Ok [proof of correctness]
claim bkevariation,I Nisynch_6 - Ok [proof of correctness]
claim bkevariation,I Niagree_5 - Ok [proof of correctness]
claim bkevariation,I Secret_4 kir Ok [proof of correctness]
claim yahalomlowe,R Niagree_13 - Ok [proof of correctness]
claim yahalomlowe,R Nisynch_12 - Ok [proof of correctness]
claim yahalomlowe,R Secret_11 kir Ok [proof of correctness]
claim yahalomlowe,I Nisynch_10 - Ok [proof of correctness]
claim yahalomlowe,I Niagree_9 - Ok [proof of correctness]
claim yahalomlowe,I Secret_8 kir Ok [proof of correctness]
claim broken1,R Secret_4 PlainSight Fail [at least 1 attack]
claim bke,R Nisynch_9 - Ok [proof of correctness]
claim bke,R Niagree_8 - Ok [proof of correctness]
claim bke,R Secret_7 kir Ok [proof of correctness]
claim bke,I Nisynch_6 - Ok [proof of correctness]
claim bke,I Niagree_5 - Ok [proof of correctness]
claim bke,I Secret_4 kir Ok [proof of correctness]
claim spliceAShcCJ,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShcCJ,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShcCJ,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Fail [exactly 1 attack]
claim soph,I Niagree_3 - Ok [proof of correctness]
claim bunava13,R2 Nisynch_C2 - Fail [at least 2 attacks]
claim bunava13,R2 Niagree_C1 - Fail [at least 2 attacks]
claim bunava13,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava13,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava13,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava13,R0 Niagree_A1 - Fail [at least 1 attack]
claim bunava24,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava24,A Niagree_A1 - Fail [at least 1 attack]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow3,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow3,I Secret_7 kir Ok [no attack within bounds]
claim kaochow3,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow3,I Nisynch_5 - Fail [at least 2 attacks]
claim unknown2,R Secret_r3 kir Ok [proof of correctness]
claim unknown2,R Niagree_r2 - Fail [at least 2 attacks]
claim unknown2,R Nisynch_r1 - Fail [at least 2 attacks]
claim unknown2,I Secret_i3 kir Ok [proof of correctness]
claim unknown2,I Niagree_i2 - Fail [at least 1 attack]
claim unknown2,I Nisynch_i1 - Fail [at least 1 attack]
claim localclaims,R Secret_r1 ni Fail [exactly 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Fail [exactly 1 attack]
claim ns3speedtest,I Secret_4 nr Ok [proof of correctness]
claim yahalom,B Secret_6 kab Ok [proof of correctness]
claim yahalom,A Secret_5 kab Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [exactly 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Fail [exactly 1 attack]
claim nsl3rep,R Nisynch_8 - Fail [at least 1 attack]
claim nsl3rep,R Niagree_5 - Ok [proof of correctness]
claim nsl3rep,I Nisynch_7 - Fail [at least 1 attack]
claim nsl3rep,I Niagree_4 - Ok [proof of correctness]
claim bunava14,D Nisynch_D2 - Fail [at least 1 attack]
claim bunava14,D Niagree_D1 - Fail [at least 1 attack]
claim bunava14,C Nisynch_C2 - Fail [at least 2 attacks]
claim bunava14,C Niagree_C1 - Fail [at least 2 attacks]
claim bunava14,B Nisynch_B2 - Fail [at least 2 attacks]
claim bunava14,B Niagree_B1 - Fail [at least 2 attacks]
claim bunava14,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava14,A Niagree_A1 - Fail [at least 1 attack]
claim boydNS,R Nisynch_r4 - Fail [at least 1 attack]
claim boydNS,R Niagree_r3 - Fail [at least 1 attack]
claim boydNS,R Secret_r2 nr Ok [proof of correctness]
claim boydNS,R Secret_r1 ni Fail [exactly 1 attack]
claim boydNS,I Nisynch_i4 - Fail [at least 2 attacks]
claim boydNS,I Niagree_i3 - Fail [at least 2 attacks]
claim boydNS,I Secret_i2 nr Fail [exactly 1 attack]
claim boydNS,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [proof of correctness]
claim ibe,R Nisynch_r4 - Ok [proof of correctness]
claim ibe,R Niagree_r3 - Ok [proof of correctness]
claim ibe,R Secret_r2 nr Ok [proof of correctness]
claim ibe,R Secret_r1 ni Ok [proof of correctness]
claim ibe,I Nisynch_i4 - Ok [proof of correctness]
claim ibe,I Niagree_i3 - Ok [proof of correctness]
claim ibe,I Secret_i2 nr Ok [proof of correctness]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim ibe,R Secret_r1 ni Fail [at least 1 attack]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson-avispa,b Niagree_10c - Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Niagree_9c - Fail [at least 1 attack]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3nr,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3nr,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3ni,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3ni,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [exactly 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]

518
test/boundruns6.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [proof of correctness]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [proof of correctness]
claim spliceAS,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS,I Secret_7 N2 Ok [proof of correctness]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-2,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-2,I Secret_I3 kir Ok [proof of correctness]
claim kaochow-2,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-2,I Nisynch_I1 - Fail [at least 2 attacks]
claim yahalom-Lowe,R Nisynch_R2 - Ok [proof of correctness]
claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim otwayrees,R Nisynch_R2 - Fail [at least 1 attack]
claim otwayrees,R Secret_R1 Kir Ok [proof of correctness]
claim otwayrees,I Nisynch_I2 - Fail [at least 1 attack]
claim otwayrees,I Secret_I1 Kir Ok [proof of correctness]
claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Fail [at least 5 attacks]
claim kaochow,R Niagree_R2 - Fail [at least 6 attacks]
claim kaochow,R Nisynch_R1 - Fail [at least 6 attacks]
claim kaochow,I Secret_I3 kir Ok [proof of correctness]
claim kaochow,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_I1 - Fail [at least 2 attacks]
claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-HC,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-HC,I Secret_7 N2 Ok [proof of correctness]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [proof of correctness]
claim ccitt509-3,R Secret_R2 Ya Ok [proof of correctness]
claim ccitt509-3,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness]
claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness]
claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco-Lowe,I Niagree_I1 - Ok [no attack within bounds]
claim yahalom-Paulson,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom-Paulson,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Paulson,I Nisynch_I2 - Fail [exactly 1 attack]
claim yahalom-Paulson,I Secret_I1 Kir Ok [proof of correctness]
claim woolam,R Nisynch_R2 - Fail [at least 2 attacks]
claim woolam,R Secret_R1 Kir Ok [proof of correctness]
claim woolam,I Nisynch_I2 - Fail [at least 2 attacks]
claim woolam,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-Hwang,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub-Hwang,R Niagree_R2 - Fail [at least 1 attack]
claim neustub-Hwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-Hwang,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub-Hwang,I Niagree_I2 - Fail [at least 1 attack]
claim neustub-Hwang,I Secret_I1 Kir Ok [proof of correctness]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-3,I Secret_I3 kir Ok [proof of correctness]
claim kaochow-3,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-3,I Nisynch_I1 - Fail [at least 2 attacks]
claim woolamPi,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness]
claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
claim ksl,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl,R Niagree_R2 - Fail [at least 1 attack]
claim ksl,R Secret_R1 Kir Ok [proof of correctness]
claim ksl,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl,I Niagree_I2 - Fail [at least 1 attack]
claim ksl,I Secret_I1 Kir Ok [proof of correctness]
claim ksl-Lowe,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl-Lowe,R Niagree_R2 - Fail [at least 1 attack]
claim ksl-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim ksl-Lowe,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl-Lowe,I Niagree_I2 - Fail [at least 1 attack]
claim ksl-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-CJ,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-CJ,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-CJ,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-CJ,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-CJ,I Secret_7 N2 Ok [proof of correctness]
claim needhamschroedersk-amend,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Fail [exactly 1 attack]
claim andrew-Concrete,R Secret_R1 kir Ok [proof of correctness]
claim andrew-Concrete,I Nisynch_I2 - Fail [exactly 1 attack]
claim andrew-Concrete,I Secret_I1 kir Ok [proof of correctness]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness]
claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness]
claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [proof of correctness]
claim andrew-Ban,I Niagree_I2 - Ok [proof of correctness]
claim andrew-Ban,I Nisynch_I1 - Ok [proof of correctness]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks]
claim yahalom-BAN,R Nisynch_R2 - Fail [at least 2 attacks]
claim yahalom-BAN,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-BAN,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom-BAN,I Secret_I1 Kir Ok [proof of correctness]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Fail [at least 5 attacks]
claim tmn,I Nisynch_I2 - Fail [at least 2 attacks]
claim tmn,I Secret_I1 Kr Fail [at least 6 attacks]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew,R Niagree_R3 - Ok [proof of correctness]
claim andrew,R Nisynch_R2 - Ok [proof of correctness]
claim andrew,R Secret_R1 kir Ok [proof of correctness]
claim andrew,I Niagree_I3 - Fail [at least 2 attacks]
claim andrew,I Nisynch_I2 - Fail [at least 2 attacks]
claim andrew,I Secret_I1 kir Fail [exactly 1 attack]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness]
claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Fail [at least 4 attacks]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [proof of correctness]
claim yahalom,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom,I Secret_I1 Kir Ok [proof of correctness]
claim wmf-Lowe,R Nisynch_R2 - Fail [at least 4 attacks]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Fail [at least 4 attacks]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk,R Secret_R2 Ni Fail [at least 9 attacks]
claim needhamschroederpk,R Secret_R1 Nr Fail [at least 9 attacks]
claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk,I Secret_I1 Ni Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Fail [exactly 1 attack]
claim neustub,I Niagree_I2 - Fail [exactly 1 attack]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub,R Niagree_R2 - Fail [at least 1 attack]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [proof of correctness]
claim andrewBan,R Niagree_8b - Ok [proof of correctness]
claim andrewBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [proof of correctness]
claim andrewBan,I Niagree_5b - Ok [proof of correctness]
claim andrewBan,I Nisynch_5 - Ok [proof of correctness]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim bkebroken,R Secret_5 kir Fail [at least 2 attacks]
claim bkebroken,I Secret_4 kir Ok [proof of correctness]
claim spliceAS,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,S Niagree_11 - Fail [at least 1 attack]
claim spliceAS,S Secret_8 N2 Fail [at least 6 attacks]
claim spliceAS,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,C Niagree_9 - Fail [at least 1 attack]
claim spliceAS,C Secret_7 N2 Fail [at least 8 attacks]
claim bkeONE,R Secret_5 kir Ok [proof of correctness]
claim bkeONE,I Secret_4 kir Ok [proof of correctness]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [proof of correctness]
claim nsl7,R Secret_4 ni Ok [proof of correctness]
claim ns3brutus,R Secret_5 ni Fail [exactly 1 attack]
claim ns3brutus,I Secret_4 nr Ok [proof of correctness]
claim woolampif,B Nisynch_7 - Fail [at least 1 attack]
claim woolampif,B Niagree_6 - Fail [exactly 1 attack]
claim yahalomBan,B Secret_6 kab Fail [at least 2 attacks]
claim yahalomBan,A Secret_5 kab Fail [at least 1 attack]
claim boyd,R Nisynch_12 - Fail [at least 2 attacks]
claim boyd,R Niagree_11 - Fail [at least 2 attacks]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [proof of correctness]
claim boyd,I Nisynch_8 - Fail [at least 2 attacks]
claim boyd,I Niagree_7 - Fail [at least 2 attacks]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShc,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShc,S Secret_8 N2 Fail [at least 6 attacks]
claim spliceAShc,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShc,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShc,C Secret_7 N2 Fail [at least 8 attacks]
claim isoiec11770213,R Secret_6 kir Ok [proof of correctness]
claim isoiec11770213,I Secret_5 kir Ok [proof of correctness]
claim gongnonceb,R Niagree_13 - Fail [at least 2 attacks]
claim gongnonceb,R Nisynch_12 - Fail [at least 2 attacks]
claim gongnonceb,R Secret_11 kr Ok [proof of correctness]
claim gongnonceb,R Secret_10 ki Ok [proof of correctness]
claim gongnonceb,I Niagree_9 - Fail [at least 2 attacks]
claim gongnonceb,I Nisynch_8 - Fail [at least 2 attacks]
claim gongnonceb,I Secret_7 kr Ok [proof of correctness]
claim gongnonceb,I Secret_6 ki Ok [proof of correctness]
claim yahalompaulson,R Niagree_13 - Fail [at least 1 attack]
claim yahalompaulson,R Nisynch_12 - Fail [at least 1 attack]
claim yahalompaulson,R Secret_11 kir Ok [proof of correctness]
claim yahalompaulson,I Niagree_10 - Fail [exactly 1 attack]
claim yahalompaulson,I Nisynch_9 - Fail [exactly 1 attack]
claim yahalompaulson,I Secret_8 kir Ok [proof of correctness]
claim ksl,B Nisynch_B3 - Fail [at least 1 attack]
claim ksl,B Niagree_B2 - Fail [at least 1 attack]
claim ksl,B Secret_B1 Kab Ok [proof of correctness]
claim ksl,A Nisynch_A3 - Fail [at least 1 attack]
claim ksl,A Niagree_A2 - Fail [at least 1 attack]
claim ksl,A Secret_A1 Kab Ok [proof of correctness]
claim denningsaccosh,B Niagree_9 - Ok [no attack within bounds]
claim denningsaccosh,B Nisynch_8 - Fail [at least 1 attack]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Fail [at least 1 attack]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Fail [at least 2 attacks]
claim woolamcmv,B Niagree_12 - Fail [at least 2 attacks]
claim woolamcmv,B Secret_11 Kab Ok [proof of correctness]
claim woolamcmv,A Nisynch_10 - Fail [at least 2 attacks]
claim woolamcmv,A Niagree_9 - Fail [at least 2 attacks]
claim woolamcmv,A Secret_8 Kab Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [proof of correctness]
claim andrewLoweBan,R Niagree_8b - Ok [proof of correctness]
claim andrewLoweBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [proof of correctness]
claim andrewLoweBan,I Niagree_5b - Fail [exactly 1 attack]
claim andrewLoweBan,I Nisynch_5 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [proof of correctness]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim ccitt509,R Niagree_11 - Ok [proof of correctness]
claim ccitt509,R Nisynch_10 - Ok [proof of correctness]
claim ccitt509,R Secret_9 yr Ok [proof of correctness]
claim ccitt509,R Secret_8 yi Ok [proof of correctness]
claim ccitt509,I Niagree_7 - Ok [proof of correctness]
claim ccitt509,I Nisynch_6 - Ok [proof of correctness]
claim ccitt509,I Secret_5 yr Ok [proof of correctness]
claim ccitt509,I Secret_4 yi Ok [proof of correctness]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [proof of correctness]
claim bunava23,R2 Nisynch_C2 - Fail [at least 3 attacks]
claim bunava23,R2 Niagree_C1 - Fail [at least 3 attacks]
claim bunava23,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava23,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava23,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava23,R0 Niagree_A1 - Fail [at least 1 attack]
claim wmfbrutus,B Secret_3 kab Ok [proof of correctness]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow2,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow2,I Secret_7 kir Ok [proof of correctness]
claim kaochow2,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow2,I Nisynch_5 - Fail [at least 2 attacks]
claim otwayrees,B Nisynch_6b - Fail [at least 1 attack]
claim otwayrees,B Niagree_6a - Fail [at least 1 attack]
claim otwayrees,B Secret_6 kab Ok [proof of correctness]
claim otwayrees,A Nisynch_5c - Fail [at least 1 attack]
claim otwayrees,A Niagree_5b - Fail [at least 1 attack]
claim otwayrees,A Secret_5 kab Ok [proof of correctness]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [no attack within bounds]
claim kaochowPalm,R Nisynch_8 - Ok [no attack within bounds]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Fail [at least 1 attack]
claim kaochowPalm,I Nisynch_5 - Fail [at least 1 attack]
claim as3a,I Nisynch_i1 - Ok [proof of correctness]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Fail [at least 3 attacks]
claim tmn,S Secret_7 Ka Fail [at least 4 attacks]
claim tmn,B Secret_6 Kb Fail [at least 3 attacks]
claim tmn,A Secret_8 Kb Fail [at least 5 attacks]
claim tmn,A Secret_5 Ka Fail [at least 4 attacks]
claim nssymmetricamended,B Nisynch_9b - Fail [at least 1 attack]
claim nssymmetricamended,B Niagree_9a - Fail [at least 1 attack]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Fail [at least 1 attack]
claim nssymmetricamended,A Niagree_8a - Fail [at least 1 attack]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Fail [at least 1 attack]
claim gongnonce,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonce,R Secret_11 kr Ok [proof of correctness]
claim gongnonce,R Secret_10 ki Ok [proof of correctness]
claim gongnonce,I Niagree_9 - Fail [at least 1 attack]
claim gongnonce,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonce,I Secret_7 kr Ok [proof of correctness]
claim gongnonce,I Secret_6 ki Ok [proof of correctness]
claim course2r890year0405ex3,I Nisynch_i2 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow,I Secret_7 kir Ok [proof of correctness]
claim kaochow,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_5 - Fail [at least 2 attacks]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Fail [at least 3 attacks]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Fail [at least 1 attack]
claim bkevariation,R Nisynch_9 - Fail [at least 1 attack]
claim bkevariation,R Niagree_8 - Fail [at least 1 attack]
claim bkevariation,R Secret_7 kir Ok [proof of correctness]
claim bkevariation,I Nisynch_6 - Ok [proof of correctness]
claim bkevariation,I Niagree_5 - Ok [proof of correctness]
claim bkevariation,I Secret_4 kir Ok [proof of correctness]
claim yahalomlowe,R Niagree_13 - Ok [proof of correctness]
claim yahalomlowe,R Nisynch_12 - Ok [proof of correctness]
claim yahalomlowe,R Secret_11 kir Ok [proof of correctness]
claim yahalomlowe,I Nisynch_10 - Ok [proof of correctness]
claim yahalomlowe,I Niagree_9 - Ok [proof of correctness]
claim yahalomlowe,I Secret_8 kir Ok [proof of correctness]
claim broken1,R Secret_4 PlainSight Fail [at least 1 attack]
claim bke,R Nisynch_9 - Ok [proof of correctness]
claim bke,R Niagree_8 - Ok [proof of correctness]
claim bke,R Secret_7 kir Ok [proof of correctness]
claim bke,I Nisynch_6 - Ok [proof of correctness]
claim bke,I Niagree_5 - Ok [proof of correctness]
claim bke,I Secret_4 kir Ok [proof of correctness]
claim spliceAShcCJ,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShcCJ,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShcCJ,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Fail [exactly 1 attack]
claim soph,I Niagree_3 - Ok [proof of correctness]
claim bunava13,R2 Nisynch_C2 - Fail [at least 2 attacks]
claim bunava13,R2 Niagree_C1 - Fail [at least 2 attacks]
claim bunava13,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava13,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava13,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava13,R0 Niagree_A1 - Fail [at least 1 attack]
claim bunava24,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava24,A Niagree_A1 - Fail [at least 1 attack]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow3,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow3,I Secret_7 kir Ok [proof of correctness]
claim kaochow3,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow3,I Nisynch_5 - Fail [at least 2 attacks]
claim unknown2,R Secret_r3 kir Ok [proof of correctness]
claim unknown2,R Niagree_r2 - Fail [at least 2 attacks]
claim unknown2,R Nisynch_r1 - Fail [at least 2 attacks]
claim unknown2,I Secret_i3 kir Ok [proof of correctness]
claim unknown2,I Niagree_i2 - Fail [at least 1 attack]
claim unknown2,I Nisynch_i1 - Fail [at least 1 attack]
claim localclaims,R Secret_r1 ni Fail [exactly 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Fail [exactly 1 attack]
claim ns3speedtest,I Secret_4 nr Ok [proof of correctness]
claim yahalom,B Secret_6 kab Ok [proof of correctness]
claim yahalom,A Secret_5 kab Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [exactly 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Fail [exactly 1 attack]
claim nsl3rep,R Nisynch_8 - Fail [at least 1 attack]
claim nsl3rep,R Niagree_5 - Ok [proof of correctness]
claim nsl3rep,I Nisynch_7 - Fail [at least 1 attack]
claim nsl3rep,I Niagree_4 - Ok [proof of correctness]
claim bunava14,D Nisynch_D2 - Fail [at least 2 attacks]
claim bunava14,D Niagree_D1 - Fail [at least 2 attacks]
claim bunava14,C Nisynch_C2 - Fail [at least 2 attacks]
claim bunava14,C Niagree_C1 - Fail [at least 2 attacks]
claim bunava14,B Nisynch_B2 - Fail [at least 2 attacks]
claim bunava14,B Niagree_B1 - Fail [at least 2 attacks]
claim bunava14,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava14,A Niagree_A1 - Fail [at least 1 attack]
claim boydNS,R Nisynch_r4 - Fail [at least 1 attack]
claim boydNS,R Niagree_r3 - Fail [at least 1 attack]
claim boydNS,R Secret_r2 nr Ok [proof of correctness]
claim boydNS,R Secret_r1 ni Fail [exactly 1 attack]
claim boydNS,I Nisynch_i4 - Fail [at least 2 attacks]
claim boydNS,I Niagree_i3 - Fail [at least 2 attacks]
claim boydNS,I Secret_i2 nr Fail [exactly 1 attack]
claim boydNS,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [proof of correctness]
claim ibe,R Nisynch_r4 - Ok [proof of correctness]
claim ibe,R Niagree_r3 - Ok [proof of correctness]
claim ibe,R Secret_r2 nr Ok [proof of correctness]
claim ibe,R Secret_r1 ni Ok [proof of correctness]
claim ibe,I Nisynch_i4 - Ok [proof of correctness]
claim ibe,I Niagree_i3 - Ok [proof of correctness]
claim ibe,I Secret_i2 nr Ok [proof of correctness]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim ibe,R Secret_r1 ni Fail [at least 1 attack]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson-avispa,b Niagree_10c - Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Niagree_9c - Fail [at least 1 attack]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3nr,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3nr,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3ni,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3ni,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [exactly 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]

518
test/boundruns7.txt Normal file
View File

@ -0,0 +1,518 @@
claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [proof of correctness]
claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [proof of correctness]
claim spliceAS,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS,I Secret_7 N2 Ok [proof of correctness]
claim kaochow-2,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-2,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-2,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-2,I Secret_I3 kir Ok [proof of correctness]
claim kaochow-2,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-2,I Nisynch_I1 - Fail [at least 2 attacks]
claim yahalom-Lowe,R Nisynch_R2 - Ok [proof of correctness]
claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim otwayrees,R Nisynch_R2 - Fail [at least 1 attack]
claim otwayrees,R Secret_R1 Kir Ok [proof of correctness]
claim otwayrees,I Nisynch_I2 - Fail [at least 1 attack]
claim otwayrees,I Secret_I1 Kir Ok [proof of correctness]
claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim kaochow,R Secret_R3 kir Fail [at least 5 attacks]
claim kaochow,R Niagree_R2 - Fail [at least 6 attacks]
claim kaochow,R Nisynch_R1 - Fail [at least 6 attacks]
claim kaochow,I Secret_I3 kir Ok [proof of correctness]
claim kaochow,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_I1 - Fail [at least 2 attacks]
claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-HC,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-HC,I Secret_7 N2 Ok [proof of correctness]
claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
claim ccitt509-3,R Secret_R3 Yb Ok [proof of correctness]
claim ccitt509-3,R Secret_R2 Ya Ok [proof of correctness]
claim ccitt509-3,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness]
claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness]
claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
claim denningSacco-Lowe,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco-Lowe,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco-Lowe,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco-Lowe,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco-Lowe,I Niagree_I1 - Ok [no attack within bounds]
claim yahalom-Paulson,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom-Paulson,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-Paulson,I Nisynch_I2 - Fail [exactly 1 attack]
claim yahalom-Paulson,I Secret_I1 Kir Ok [proof of correctness]
claim woolam,R Nisynch_R2 - Fail [at least 2 attacks]
claim woolam,R Secret_R1 Kir Ok [proof of correctness]
claim woolam,I Nisynch_I2 - Fail [at least 2 attacks]
claim woolam,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-Hwang,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub-Hwang,R Niagree_R2 - Fail [at least 1 attack]
claim neustub-Hwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-Hwang,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub-Hwang,I Niagree_I2 - Fail [at least 1 attack]
claim neustub-Hwang,I Secret_I1 Kir Ok [proof of correctness]
claim kaochow-3,R Secret_R3 kir Ok [no attack within bounds]
claim kaochow-3,R Niagree_R2 - Fail [at least 2 attacks]
claim kaochow-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim kaochow-3,I Secret_I3 kir Ok [proof of correctness]
claim kaochow-3,I Niagree_I2 - Fail [at least 2 attacks]
claim kaochow-3,I Nisynch_I1 - Fail [at least 2 attacks]
claim woolamPi,R Nisynch_R1 - Fail [at least 4 attacks]
claim ccitt509-ban3,R Nisynch_5 - Ok [proof of correctness]
claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
claim ksl,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl,R Niagree_R2 - Fail [at least 1 attack]
claim ksl,R Secret_R1 Kir Ok [proof of correctness]
claim ksl,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl,I Niagree_I2 - Fail [at least 1 attack]
claim ksl,I Secret_I1 Kir Ok [proof of correctness]
claim ksl-Lowe,R Nisynch_R3 - Fail [at least 1 attack]
claim ksl-Lowe,R Niagree_R2 - Fail [at least 1 attack]
claim ksl-Lowe,R Secret_R1 Kir Ok [proof of correctness]
claim ksl-Lowe,I Nisynch_I3 - Fail [at least 1 attack]
claim ksl-Lowe,I Niagree_I2 - Fail [at least 1 attack]
claim ksl-Lowe,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
claim denningSacco,R Secret_R3 Kir Ok [no attack within bounds]
claim denningSacco,R Nisynch_R2 - Fail [at least 1 attack]
claim denningSacco,R Niagree_R1 - Ok [no attack within bounds]
claim denningSacco,I Secret_I3 Kir Ok [no attack within bounds]
claim denningSacco,I Nisynch_I2 - Fail [at least 1 attack]
claim denningSacco,I Niagree_I1 - Ok [no attack within bounds]
claim spliceAS-CJ,R Nisynch_12 - Fail [at least 1 attack]
claim spliceAS-CJ,R Niagree_11 - Fail [at least 1 attack]
claim spliceAS-CJ,R Secret_8 N2 Ok [proof of correctness]
claim spliceAS-CJ,I Nisynch_10 - Fail [at least 1 attack]
claim spliceAS-CJ,I Niagree_9 - Fail [at least 1 attack]
claim spliceAS-CJ,I Secret_7 N2 Ok [proof of correctness]
claim needhamschroedersk-amend,R Nisynch_R3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,R Secret_R1 Nr Ok [no attack within bounds]
claim needhamschroedersk-amend,I Nisynch_I3 - Fail [at least 1 attack]
claim needhamschroedersk-amend,I Secret_I2 Kir Ok [no attack within bounds]
claim needhamschroedersk,R Nisynch_R3 - Fail [at least 2 attacks]
claim needhamschroedersk,R Secret_R1 Kir Fail [at least 2 attacks]
claim needhamschroedersk,I Nisynch_I3 - Ok [no attack within bounds]
claim needhamschroedersk,I Secret_I2 Kir Ok [no attack within bounds]
claim andrew-Concrete,R Nisynch_R2 - Fail [exactly 1 attack]
claim andrew-Concrete,R Secret_R1 kir Ok [proof of correctness]
claim andrew-Concrete,I Nisynch_I2 - Fail [exactly 1 attack]
claim andrew-Concrete,I Secret_I1 kir Ok [proof of correctness]
claim andrew-Ban,R Secret_R4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,R Secret_R3 kir Ok [proof of correctness]
claim andrew-Ban,R Niagree_R2 - Ok [proof of correctness]
claim andrew-Ban,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-Ban,I Secret_I4 k(I,R) Ok [proof of correctness]
claim andrew-Ban,I Secret_I3 kir Ok [proof of correctness]
claim andrew-Ban,I Niagree_I2 - Ok [proof of correctness]
claim andrew-Ban,I Nisynch_I1 - Ok [proof of correctness]
claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks]
claim yahalom-BAN,R Nisynch_R2 - Fail [at least 2 attacks]
claim yahalom-BAN,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom-BAN,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom-BAN,I Secret_I1 Kir Ok [proof of correctness]
claim tmn,R Nisynch_R2 - Fail [exactly 1 attack]
claim tmn,R Secret_R1 Kr Fail [at least 5 attacks]
claim tmn,I Nisynch_I2 - Fail [at least 2 attacks]
claim tmn,I Secret_I1 Kr Fail [at least 6 attacks]
claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew,R Niagree_R3 - Ok [proof of correctness]
claim andrew,R Nisynch_R2 - Ok [proof of correctness]
claim andrew,R Secret_R1 kir Ok [proof of correctness]
claim andrew,I Niagree_I3 - Fail [at least 2 attacks]
claim andrew,I Nisynch_I2 - Fail [at least 2 attacks]
claim andrew,I Secret_I1 kir Fail [exactly 1 attack]
claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks]
claim andrew-LoweBan,R Secret_R2 kir Ok [proof of correctness]
claim andrew-LoweBan,R Nisynch_R1 - Ok [proof of correctness]
claim andrew-LoweBan,I Secret_I2 kir Ok [proof of correctness]
claim andrew-LoweBan,I Nisynch_I1 - Ok [proof of correctness]
claim wmf,R Nisynch_R2 - Fail [at least 4 attacks]
claim wmf,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf,I Secret_I1 Kir Ok [proof of correctness]
claim yahalom,R Nisynch_R2 - Fail [at least 1 attack]
claim yahalom,R Secret_R1 Kir Ok [proof of correctness]
claim yahalom,I Nisynch_I2 - Fail [at least 1 attack]
claim yahalom,I Secret_I1 Kir Ok [proof of correctness]
claim wmf-Lowe,R Nisynch_R2 - Fail [at least 4 attacks]
claim wmf-Lowe,R Secret_R1 Kir Ok [no attack within bounds]
claim wmf-Lowe,I Nisynch_I2 - Fail [at least 4 attacks]
claim wmf-Lowe,I Secret_I1 Kir Ok [no attack within bounds]
claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks]
claim needhamschroederpk,R Secret_R2 Ni Fail [at least 9 attacks]
claim needhamschroederpk,R Secret_R1 Nr Fail [at least 9 attacks]
claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks]
claim needhamschroederpk,I Secret_I2 Nr Ok [proof of correctness]
claim needhamschroederpk,I Secret_I1 Ni Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 2 attacks]
claim neustub,R Niagree_R2 - Fail [at least 2 attacks]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Fail [exactly 1 attack]
claim neustub,I Niagree_I2 - Fail [exactly 1 attack]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Fail [at least 3 attacks]
claim neustub^Repeat,R Niagree_R2 - Fail [at least 3 attacks]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Fail [at least 1 attack]
claim neustub^Repeat,I Niagree_I2 - Fail [at least 1 attack]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub,R Nisynch_R3 - Fail [at least 1 attack]
claim neustub,R Niagree_R2 - Fail [at least 1 attack]
claim neustub,R Secret_R1 Kir Ok [proof of correctness]
claim neustub,I Nisynch_I3 - Ok [proof of correctness]
claim neustub,I Niagree_I2 - Ok [proof of correctness]
claim neustub,I Secret_I1 Kir Ok [proof of correctness]
claim neustub^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang,I Secret_I1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Nisynch_R3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Niagree_R2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,R Secret_R1 Kir Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Nisynch_I3 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Niagree_I2 - Ok [proof of correctness]
claim neustub-GuttmanHwang^Repeat,I Secret_I1 Kir Ok [proof of correctness]
claim r5bound,R Secret_6 k2 Ok [proof of correctness]
claim andrewBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewBan,R Secret_9 kir Ok [proof of correctness]
claim andrewBan,R Niagree_8b - Ok [proof of correctness]
claim andrewBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewBan,I Secret_6 kir Ok [proof of correctness]
claim andrewBan,I Niagree_5b - Ok [proof of correctness]
claim andrewBan,I Nisynch_5 - Ok [proof of correctness]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim bkebroken,R Secret_5 kir Fail [at least 2 attacks]
claim bkebroken,I Secret_4 kir Ok [proof of correctness]
claim spliceAS,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAS,S Niagree_11 - Fail [at least 1 attack]
claim spliceAS,S Secret_8 N2 Fail [at least 6 attacks]
claim spliceAS,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAS,C Niagree_9 - Fail [at least 1 attack]
claim spliceAS,C Secret_7 N2 Fail [at least 8 attacks]
claim bkeONE,R Secret_5 kir Ok [proof of correctness]
claim bkeONE,I Secret_4 kir Ok [proof of correctness]
claim carkeyni,R Nisynch_2 - Ok [proof of correctness]
claim nsl7,R Secret_5 nr Ok [proof of correctness]
claim nsl7,R Secret_4 ni Ok [proof of correctness]
claim ns3brutus,R Secret_5 ni Fail [exactly 1 attack]
claim ns3brutus,I Secret_4 nr Ok [proof of correctness]
claim woolampif,B Nisynch_7 - Fail [at least 1 attack]
claim woolampif,B Niagree_6 - Fail [exactly 1 attack]
claim yahalomBan,B Secret_6 kab Fail [at least 2 attacks]
claim yahalomBan,A Secret_5 kab Fail [at least 1 attack]
claim boyd,R Nisynch_12 - Fail [at least 2 attacks]
claim boyd,R Niagree_11 - Fail [at least 2 attacks]
claim boyd,R Secret_10 m(ks,ni,nr) Ok [proof of correctness]
claim boyd,I Nisynch_8 - Fail [at least 2 attacks]
claim boyd,I Niagree_7 - Fail [at least 2 attacks]
claim boyd,I Secret_6 m(ks,ni,nr) Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim onetrace,I Secret_4 input Fail [exactly 1 attack]
claim spliceAShc,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShc,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShc,S Secret_8 N2 Fail [at least 6 attacks]
claim spliceAShc,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShc,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShc,C Secret_7 N2 Fail [at least 8 attacks]
claim isoiec11770213,R Secret_6 kir Ok [proof of correctness]
claim isoiec11770213,I Secret_5 kir Ok [proof of correctness]
claim gongnonceb,R Niagree_13 - Fail [at least 2 attacks]
claim gongnonceb,R Nisynch_12 - Fail [at least 2 attacks]
claim gongnonceb,R Secret_11 kr Ok [proof of correctness]
claim gongnonceb,R Secret_10 ki Ok [proof of correctness]
claim gongnonceb,I Niagree_9 - Fail [at least 2 attacks]
claim gongnonceb,I Nisynch_8 - Fail [at least 2 attacks]
claim gongnonceb,I Secret_7 kr Ok [proof of correctness]
claim gongnonceb,I Secret_6 ki Ok [proof of correctness]
claim yahalompaulson,R Niagree_13 - Fail [at least 1 attack]
claim yahalompaulson,R Nisynch_12 - Fail [at least 1 attack]
claim yahalompaulson,R Secret_11 kir Ok [proof of correctness]
claim yahalompaulson,I Niagree_10 - Fail [exactly 1 attack]
claim yahalompaulson,I Nisynch_9 - Fail [exactly 1 attack]
claim yahalompaulson,I Secret_8 kir Ok [proof of correctness]
claim ksl,B Nisynch_B3 - Fail [at least 1 attack]
claim ksl,B Niagree_B2 - Fail [at least 1 attack]
claim ksl,B Secret_B1 Kab Ok [proof of correctness]
claim ksl,A Nisynch_A3 - Fail [at least 1 attack]
claim ksl,A Niagree_A2 - Fail [at least 1 attack]
claim ksl,A Secret_A1 Kab Ok [proof of correctness]
claim denningsaccosh,B Niagree_9 - Ok [no attack within bounds]
claim denningsaccosh,B Nisynch_8 - Fail [at least 1 attack]
claim denningsaccosh,B Secret_7 kab Ok [no attack within bounds]
claim denningsaccosh,A Niagree_6 - Ok [no attack within bounds]
claim denningsaccosh,A Nisynch_5 - Fail [at least 1 attack]
claim denningsaccosh,A Secret_4 kab Ok [no attack within bounds]
claim woolamcmv,S Secret_14 Kab Ok [proof of correctness]
claim woolamcmv,B Nisynch_13 - Fail [at least 2 attacks]
claim woolamcmv,B Niagree_12 - Fail [at least 2 attacks]
claim woolamcmv,B Secret_11 Kab Ok [proof of correctness]
claim woolamcmv,A Nisynch_10 - Fail [at least 2 attacks]
claim woolamcmv,A Niagree_9 - Fail [at least 2 attacks]
claim woolamcmv,A Secret_8 Kab Ok [proof of correctness]
claim f4,I Niagree_i1 - Ok [does not occur]
claim carkeybrokenlim,R Nisynch_2 - Fail [exactly 1 attack]
claim andrewLoweBan,R Secret_10 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,R Secret_9 kir Ok [proof of correctness]
claim andrewLoweBan,R Niagree_8b - Ok [proof of correctness]
claim andrewLoweBan,R Nisynch_8 - Ok [proof of correctness]
claim andrewLoweBan,I Secret_7 k(I,R) Ok [proof of correctness]
claim andrewLoweBan,I Secret_6 kir Ok [proof of correctness]
claim andrewLoweBan,I Niagree_5b - Fail [exactly 1 attack]
claim andrewLoweBan,I Nisynch_5 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Nisynch_i2 - Ok [proof of correctness]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim ccitt509,R Niagree_11 - Ok [proof of correctness]
claim ccitt509,R Nisynch_10 - Ok [proof of correctness]
claim ccitt509,R Secret_9 yr Ok [proof of correctness]
claim ccitt509,R Secret_8 yi Ok [proof of correctness]
claim ccitt509,I Niagree_7 - Ok [proof of correctness]
claim ccitt509,I Nisynch_6 - Ok [proof of correctness]
claim ccitt509,I Secret_5 yr Ok [proof of correctness]
claim ccitt509,I Secret_4 yi Ok [proof of correctness]
claim simplest,I Secret_3 n Fail [exactly 1 attack]
claim sophkx,I Secret_4 kir Ok [proof of correctness]
claim bunava23,R2 Nisynch_C2 - Fail [at least 3 attacks]
claim bunava23,R2 Niagree_C1 - Fail [at least 3 attacks]
claim bunava23,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava23,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava23,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava23,R0 Niagree_A1 - Fail [at least 1 attack]
claim wmfbrutus,B Secret_3 kab Ok [proof of correctness]
claim kaochow2,R Secret_10 kir Ok [no attack within bounds]
claim kaochow2,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow2,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow2,I Secret_7 kir Ok [proof of correctness]
claim kaochow2,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow2,I Nisynch_5 - Fail [at least 2 attacks]
claim otwayrees,B Nisynch_6b - Fail [at least 1 attack]
claim otwayrees,B Niagree_6a - Fail [at least 1 attack]
claim otwayrees,B Secret_6 kab Ok [proof of correctness]
claim otwayrees,A Nisynch_5c - Fail [at least 1 attack]
claim otwayrees,A Niagree_5b - Fail [at least 1 attack]
claim otwayrees,A Secret_5 kab Ok [proof of correctness]
claim kaochowPalm,R Secret_10 kir Ok [no attack within bounds]
claim kaochowPalm,R Niagree_9 - Ok [no attack within bounds]
claim kaochowPalm,R Nisynch_8 - Ok [no attack within bounds]
claim kaochowPalm,I Secret_7 kir Ok [no attack within bounds]
claim kaochowPalm,I Niagree_6 - Fail [at least 1 attack]
claim kaochowPalm,I Nisynch_5 - Fail [at least 1 attack]
claim as3a,I Nisynch_i1 - Ok [proof of correctness]
claim samascbroken,R Secret_4 kir Ok [proof of correctness]
claim tmn,B Secret_6 Kb Fail [at least 3 attacks]
claim tmn,S Secret_7 Ka Fail [at least 4 attacks]
claim tmn,B Secret_6 Kb Fail [at least 3 attacks]
claim tmn,A Secret_8 Kb Fail [at least 5 attacks]
claim tmn,A Secret_5 Ka Fail [at least 4 attacks]
claim nssymmetricamended,B Nisynch_9b - Fail [at least 1 attack]
claim nssymmetricamended,B Niagree_9a - Fail [at least 1 attack]
claim nssymmetricamended,B Secret_9 kab Ok [no attack within bounds]
claim nssymmetricamended,A Nisynch_8b - Fail [at least 1 attack]
claim nssymmetricamended,A Niagree_8a - Fail [at least 1 attack]
claim nssymmetricamended,A Secret_8 kab Ok [no attack within bounds]
claim nssymmetric,B Secret_7 kab Ok [no attack within bounds]
claim nssymmetric,A Secret_6 kab Ok [no attack within bounds]
claim gongnonce,R Niagree_13 - Fail [at least 1 attack]
claim gongnonce,R Nisynch_12 - Fail [at least 1 attack]
claim gongnonce,R Secret_11 kr Ok [proof of correctness]
claim gongnonce,R Secret_10 ki Ok [proof of correctness]
claim gongnonce,I Niagree_9 - Fail [at least 1 attack]
claim gongnonce,I Nisynch_8 - Fail [at least 1 attack]
claim gongnonce,I Secret_7 kr Ok [proof of correctness]
claim gongnonce,I Secret_6 ki Ok [proof of correctness]
claim course2r890year0405ex3,I Nisynch_i2 - Fail [exactly 1 attack]
claim course2r890year0405ex3,I Niagree_i1 - Ok [proof of correctness]
claim kaochow,R Secret_10 kir Ok [no attack within bounds]
claim kaochow,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow,I Secret_7 kir Ok [proof of correctness]
claim kaochow,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow,I Nisynch_5 - Fail [at least 2 attacks]
claim lcbreakerS1,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreakerS1,R Secret_r0 ni2 Fail [at least 3 attacks]
claim lcbreakerS1,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i1 ni Ok [no attack within bounds]
claim lcbreakerS1,I Secret_i0 ni2 Fail [at least 1 attack]
claim bkevariation,R Nisynch_9 - Fail [at least 1 attack]
claim bkevariation,R Niagree_8 - Fail [at least 1 attack]
claim bkevariation,R Secret_7 kir Ok [proof of correctness]
claim bkevariation,I Nisynch_6 - Ok [proof of correctness]
claim bkevariation,I Niagree_5 - Ok [proof of correctness]
claim bkevariation,I Secret_4 kir Ok [proof of correctness]
claim yahalomlowe,R Niagree_13 - Ok [proof of correctness]
claim yahalomlowe,R Nisynch_12 - Ok [proof of correctness]
claim yahalomlowe,R Secret_11 kir Ok [proof of correctness]
claim yahalomlowe,I Nisynch_10 - Ok [proof of correctness]
claim yahalomlowe,I Niagree_9 - Ok [proof of correctness]
claim yahalomlowe,I Secret_8 kir Ok [proof of correctness]
claim broken1,R Secret_4 PlainSight Fail [at least 1 attack]
claim bke,R Nisynch_9 - Ok [proof of correctness]
claim bke,R Niagree_8 - Ok [proof of correctness]
claim bke,R Secret_7 kir Ok [proof of correctness]
claim bke,I Nisynch_6 - Ok [proof of correctness]
claim bke,I Niagree_5 - Ok [proof of correctness]
claim bke,I Secret_4 kir Ok [proof of correctness]
claim spliceAShcCJ,S Nisynch_12 - Fail [at least 1 attack]
claim spliceAShcCJ,S Niagree_11 - Fail [at least 1 attack]
claim spliceAShcCJ,S Secret_8 N2 Ok [no attack within bounds]
claim spliceAShcCJ,C Nisynch_10 - Fail [at least 1 attack]
claim spliceAShcCJ,C Niagree_9 - Fail [at least 1 attack]
claim spliceAShcCJ,C Secret_7 N2 Ok [no attack within bounds]
claim carkeyni2,R Nisynch_4 - Fail [exactly 1 attack]
claim soph,I Niagree_3 - Ok [proof of correctness]
claim bunava13,R2 Nisynch_C2 - Fail [at least 2 attacks]
claim bunava13,R2 Niagree_C1 - Fail [at least 2 attacks]
claim bunava13,R1 Nisynch_B2 - Fail [at least 2 attacks]
claim bunava13,R1 Niagree_B1 - Fail [at least 2 attacks]
claim bunava13,R0 Nisynch_A2 - Fail [at least 1 attack]
claim bunava13,R0 Niagree_A1 - Fail [at least 1 attack]
claim bunava24,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava24,A Niagree_A1 - Fail [at least 1 attack]
claim kaochow3,R Secret_10 kir Ok [no attack within bounds]
claim kaochow3,R Niagree_9 - Fail [at least 2 attacks]
claim kaochow3,R Nisynch_8 - Fail [at least 2 attacks]
claim kaochow3,I Secret_7 kir Ok [proof of correctness]
claim kaochow3,I Niagree_6 - Fail [at least 2 attacks]
claim kaochow3,I Nisynch_5 - Fail [at least 2 attacks]
claim unknown2,R Secret_r3 kir Ok [proof of correctness]
claim unknown2,R Niagree_r2 - Fail [at least 2 attacks]
claim unknown2,R Nisynch_r1 - Fail [at least 2 attacks]
claim unknown2,I Secret_i3 kir Ok [proof of correctness]
claim unknown2,I Niagree_i2 - Fail [at least 1 attack]
claim unknown2,I Nisynch_i1 - Fail [at least 1 attack]
claim localclaims,R Secret_r1 ni Fail [exactly 1 attack]
claim localclaims,I Secret_i1 ni Ok [proof of correctness]
claim woolamce,B Secret_8 authToken Ok [proof of correctness]
claim ns3speedtest,R Secret_5 ni Fail [exactly 1 attack]
claim ns3speedtest,I Secret_4 nr Ok [proof of correctness]
claim yahalom,B Secret_6 kab Ok [proof of correctness]
claim yahalom,A Secret_5 kab Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [exactly 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]
claim lcbreaker,R Secret_r2 nr Ok [no attack within bounds]
claim lcbreaker,R Secret_r1 ni Ok [no attack within bounds]
claim lcbreaker,I Secret_i2 nr Ok [no attack within bounds]
claim lcbreaker,I Secret_i1 ni Ok [no attack within bounds]
claim carkeybroken,R Nisynch_2 - Fail [exactly 1 attack]
claim nsl3rep,R Nisynch_8 - Fail [at least 1 attack]
claim nsl3rep,R Niagree_5 - Ok [proof of correctness]
claim nsl3rep,I Nisynch_7 - Fail [at least 1 attack]
claim nsl3rep,I Niagree_4 - Ok [proof of correctness]
claim bunava14,D Nisynch_D2 - Fail [at least 2 attacks]
claim bunava14,D Niagree_D1 - Fail [at least 2 attacks]
claim bunava14,C Nisynch_C2 - Fail [at least 2 attacks]
claim bunava14,C Niagree_C1 - Fail [at least 2 attacks]
claim bunava14,B Nisynch_B2 - Fail [at least 2 attacks]
claim bunava14,B Niagree_B1 - Fail [at least 2 attacks]
claim bunava14,A Nisynch_A2 - Fail [at least 1 attack]
claim bunava14,A Niagree_A1 - Fail [at least 1 attack]
claim boydNS,R Nisynch_r4 - Fail [at least 1 attack]
claim boydNS,R Niagree_r3 - Fail [at least 1 attack]
claim boydNS,R Secret_r2 nr Ok [proof of correctness]
claim boydNS,R Secret_r1 ni Fail [exactly 1 attack]
claim boydNS,I Nisynch_i4 - Fail [at least 2 attacks]
claim boydNS,I Niagree_i3 - Fail [at least 2 attacks]
claim boydNS,I Secret_i2 nr Fail [exactly 1 attack]
claim boydNS,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson,b Secret_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,b Secret_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim tlspaulson,a Secret_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [proof of correctness]
claim tlspaulson,a Secret_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [proof of correctness]
claim ibe,S Secret_s1 ibesecret(param(S),R) Ok [proof of correctness]
claim ibe,R Nisynch_r4 - Ok [proof of correctness]
claim ibe,R Niagree_r3 - Ok [proof of correctness]
claim ibe,R Secret_r2 nr Ok [proof of correctness]
claim ibe,R Secret_r1 ni Ok [proof of correctness]
claim ibe,I Nisynch_i4 - Ok [proof of correctness]
claim ibe,I Niagree_i3 - Ok [proof of correctness]
claim ibe,I Secret_i2 nr Ok [proof of correctness]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim ibe,R Secret_r1 ni Fail [at least 1 attack]
claim ibe,I Secret_i1 ni Ok [proof of correctness]
claim tlspaulson-avispa,b Niagree_10c - Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,b Secret_10a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Niagree_9c - Fail [at least 1 attack]
claim tlspaulson-avispa,a Secret_9b keygen(a,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim tlspaulson-avispa,a Secret_9a keygen(b,na,nb,hash(pms,na,nb)) Ok [proof of correctness]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th1,R Nisynch_r - Ok [proof of correctness]
claim nsl3th1,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3nr,R Nisynch_r2 - Fail [at least 1 attack]
claim nsl3th3nr,I Nisynch_i2 - Fail [at least 1 attack]
claim nsl3th2,R Nisynch_r - Ok [proof of correctness]
claim nsl3th2,I Nisynch_i - Ok [proof of correctness]
claim nsl3th3ni,R Nisynch_r2 - Ok [no attack within bounds]
claim nsl3th3ni,I Nisynch_i2 - Ok [no attack within bounds]
claim nsl3,R Nisynch_r4 - Ok [proof of correctness]
claim nsl3,R Niagree_r3 - Ok [proof of correctness]
claim nsl3,R Secret_r2 nr Ok [proof of correctness]
claim nsl3,R Secret_r1 ni Ok [proof of correctness]
claim nsl3,I Nisynch_i4 - Ok [proof of correctness]
claim nsl3,I Niagree_i3 - Ok [proof of correctness]
claim nsl3,I Secret_i2 nr Ok [proof of correctness]
claim nsl3,I Secret_i1 ni Ok [proof of correctness]
claim ns3,R Nisynch_r4 - Fail [exactly 1 attack]
claim ns3,R Niagree_r3 - Fail [exactly 1 attack]
claim ns3,R Secret_r2 nr Fail [exactly 1 attack]
claim ns3,R Secret_r1 ni Fail [exactly 1 attack]
claim ns3,I Nisynch_i4 - Ok [proof of correctness]
claim ns3,I Niagree_i3 - Ok [proof of correctness]
claim ns3,I Secret_i2 nr Ok [proof of correctness]
claim ns3,I Secret_i1 ni Ok [proof of correctness]

24
test/boundtime1.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r1 --plain"
User time (seconds): 0.44
System time (seconds): 0.13
Percent of CPU this job got: 50%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:01.12
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 21472
Voluntary context switches: 150
Involuntary context switches: 1126
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

24
test/boundtime2.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r2 --plain"
User time (seconds): 2.26
System time (seconds): 0.14
Percent of CPU this job got: 73%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.28
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 22257
Voluntary context switches: 179
Involuntary context switches: 1537
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

24
test/boundtime3.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r3 --plain"
User time (seconds): 10.08
System time (seconds): 0.16
Percent of CPU this job got: 83%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.34
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 22852
Voluntary context switches: 200
Involuntary context switches: 3130
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

24
test/boundtime4.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r4 --plain"
User time (seconds): 37.98
System time (seconds): 0.27
Percent of CPU this job got: 64%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:58.95
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 24560
Voluntary context switches: 198
Involuntary context switches: 10032
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

24
test/boundtime5.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r5 --plain"
User time (seconds): 149.73
System time (seconds): 0.50
Percent of CPU this job got: 87%
Elapsed (wall clock) time (h:mm:ss or m:ss): 2:50.77
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 31019
Voluntary context switches: 197
Involuntary context switches: 34959
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

24
test/boundtime6.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r6 --plain"
User time (seconds): 591.45
System time (seconds): 1.16
Percent of CPU this job got: 88%
Elapsed (wall clock) time (h:mm:ss or m:ss): 11:10.77
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 51219
Voluntary context switches: 204
Involuntary context switches: 133969
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

24
test/boundtime7.txt Normal file
View File

@ -0,0 +1,24 @@
Command exited with non-zero status 123
Command being timed: "./test-all.sh scyther -r6 --plain"
User time (seconds): 590.43
System time (seconds): 1.32
Percent of CPU this job got: 86%
Elapsed (wall clock) time (h:mm:ss or m:ss): 11:25.74
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 0
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 51110
Voluntary context switches: 200
Involuntary context switches: 131751
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 123

View File

@ -198,47 +198,47 @@ def main():
sharedproblems = []
firstproblem = True
for g in range(-1,512):
if (g != 0) and ((g == -1) or ((g & (64+16+8+4+1)) == 0)):
(ra,rb,rp,nc,np,st,timeouts,prot_undec) = test_goal_selector(g, options,
boundstatesmax.get())
heuristics = [-1,32,2,128,162]
for g in heuristics:
(ra,rb,rp,nc,np,st,timeouts,prot_undec) = test_goal_selector(g, options,
boundstatesmax.get())
res = str(g)
if ra < 0:
# Error: not well bounded
res += "\tWent over bound, stopped investigation."
else:
undecided = rb + timeouts
boundstates = undecided * undecided * st
res = str(g)
if ra < 0:
# Error: not well bounded
res += "\tWent over bound, stopped investigation."
else:
undecided = rb + timeouts
boundstates = undecided * undecided * st
def shows (res, mx, data):
return res + "\t" + str(data) + mx.reg(data)
def shows (res, mx, data):
return res + "\t" + str(data) + mx.reg(data)
decide = (100 * (ra + rp)) / nc
res = shows (res, decidemax, decide)
res += "%"
res = shows (res, ramax, ra)
res = shows (res, rpmax, rp)
res = shows (res, rbmax, rb)
res = shows (res, timeoutsmax, timeouts)
res = res + "\t%i" % nc
res += "\t%i" % np
res = shows (res, statesmax, st)
res = shows (res, boundstatesmax, boundstates)
decide = (100 * (ra + rp)) / nc
problems[g] = prot_undec
if firstproblem:
firstproblem = False
sharedproblems = prot_undec
else:
nl = []
for p in sharedproblems:
if p in prot_undec:
nl += [p]
sharedproblems = nl
res = shows (res, decidemax, decide)
res += "%"
res = shows (res, ramax, ra)
res = shows (res, rpmax, rp)
res = shows (res, rbmax, rb)
res = shows (res, timeoutsmax, timeouts)
res = res + "\t%i" % nc
res += "\t%i" % np
res = shows (res, statesmax, st)
res = shows (res, boundstatesmax, boundstates)
print res
problems[g] = prot_undec
if firstproblem:
firstproblem = False
sharedproblems = prot_undec
else:
nl = []
for p in sharedproblems:
if p in prot_undec:
nl += [p]
sharedproblems = nl
print res
print
print "Goal selector scan completed."
print