From 3b330d40de9720fcd3dbab89e10a5ec82e80244c Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 1 Jul 2006 10:11:08 +0000 Subject: [PATCH] - Added preliminary results, which will be used in the thesis. - Modified heuristics test for stuff in the thesis. --- test/boundanalyze.py | 4 + test/boundanalyze.txt | 32 +++ test/boundruns1.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundruns2.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundruns3.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundruns4.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundruns5.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundruns6.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundruns7.txt | 518 ++++++++++++++++++++++++++++++++++++++ test/boundtime1.txt | 24 ++ test/boundtime2.txt | 24 ++ test/boundtime3.txt | 24 ++ test/boundtime4.txt | 24 ++ test/boundtime5.txt | 24 ++ test/boundtime6.txt | 24 ++ test/boundtime7.txt | 24 ++ test/compareheuristics.py | 72 +++--- 17 files changed, 3866 insertions(+), 36 deletions(-) create mode 100644 test/boundanalyze.txt create mode 100644 test/boundruns1.txt create mode 100644 test/boundruns2.txt create mode 100644 test/boundruns3.txt create mode 100644 test/boundruns4.txt create mode 100644 test/boundruns5.txt create mode 100644 test/boundruns6.txt create mode 100644 test/boundruns7.txt create mode 100644 test/boundtime1.txt create mode 100644 test/boundtime2.txt create mode 100644 test/boundtime3.txt create mode 100644 test/boundtime4.txt create mode 100644 test/boundtime5.txt create mode 100644 test/boundtime6.txt create mode 100644 test/boundtime7.txt diff --git a/test/boundanalyze.py b/test/boundanalyze.py index 0240043..50d331a 100755 --- a/test/boundanalyze.py +++ b/test/boundanalyze.py @@ -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(): diff --git a/test/boundanalyze.txt b/test/boundanalyze.txt new file mode 100644 index 0000000..dfe3adc --- /dev/null +++ b/test/boundanalyze.txt @@ -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: +[] diff --git a/test/boundruns1.txt b/test/boundruns1.txt new file mode 100644 index 0000000..afcba19 --- /dev/null +++ b/test/boundruns1.txt @@ -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] diff --git a/test/boundruns2.txt b/test/boundruns2.txt new file mode 100644 index 0000000..8283d00 --- /dev/null +++ b/test/boundruns2.txt @@ -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] diff --git a/test/boundruns3.txt b/test/boundruns3.txt new file mode 100644 index 0000000..41d5b68 --- /dev/null +++ b/test/boundruns3.txt @@ -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] diff --git a/test/boundruns4.txt b/test/boundruns4.txt new file mode 100644 index 0000000..b7d35a8 --- /dev/null +++ b/test/boundruns4.txt @@ -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] diff --git a/test/boundruns5.txt b/test/boundruns5.txt new file mode 100644 index 0000000..15608f4 --- /dev/null +++ b/test/boundruns5.txt @@ -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] diff --git a/test/boundruns6.txt b/test/boundruns6.txt new file mode 100644 index 0000000..477d639 --- /dev/null +++ b/test/boundruns6.txt @@ -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] diff --git a/test/boundruns7.txt b/test/boundruns7.txt new file mode 100644 index 0000000..477d639 --- /dev/null +++ b/test/boundruns7.txt @@ -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] diff --git a/test/boundtime1.txt b/test/boundtime1.txt new file mode 100644 index 0000000..712083a --- /dev/null +++ b/test/boundtime1.txt @@ -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 diff --git a/test/boundtime2.txt b/test/boundtime2.txt new file mode 100644 index 0000000..e3cdf87 --- /dev/null +++ b/test/boundtime2.txt @@ -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 diff --git a/test/boundtime3.txt b/test/boundtime3.txt new file mode 100644 index 0000000..4eb8803 --- /dev/null +++ b/test/boundtime3.txt @@ -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 diff --git a/test/boundtime4.txt b/test/boundtime4.txt new file mode 100644 index 0000000..72ff0d7 --- /dev/null +++ b/test/boundtime4.txt @@ -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 diff --git a/test/boundtime5.txt b/test/boundtime5.txt new file mode 100644 index 0000000..981b234 --- /dev/null +++ b/test/boundtime5.txt @@ -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 diff --git a/test/boundtime6.txt b/test/boundtime6.txt new file mode 100644 index 0000000..fae1e4d --- /dev/null +++ b/test/boundtime6.txt @@ -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 diff --git a/test/boundtime7.txt b/test/boundtime7.txt new file mode 100644 index 0000000..e2bb9b8 --- /dev/null +++ b/test/boundtime7.txt @@ -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 diff --git a/test/compareheuristics.py b/test/compareheuristics.py index 238b13c..27c4f5d 100755 --- a/test/compareheuristics.py +++ b/test/compareheuristics.py @@ -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