From fc6923a7be333e952d40aad5d09187d616af91b3 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 1 Jul 2006 11:53:26 +0000 Subject: [PATCH] - Added new results (typo fix). --- test/boundanalyze.txt | 5 ++--- test/boundruns7.txt | 26 +++++++++++++------------- test/boundtest.sh | 2 +- test/boundtime7.txt | 16 ++++++++-------- 4 files changed, 24 insertions(+), 25 deletions(-) diff --git a/test/boundanalyze.txt b/test/boundanalyze.txt index dfe3adc..3799813 100644 --- a/test/boundanalyze.txt +++ b/test/boundanalyze.txt @@ -5,16 +5,15 @@ prot claims attacks correct decided [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% +[boundruns7.txt] 518 236 236 91.1196911197% - 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 +boundtime7.txt 2159.35 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'] diff --git a/test/boundruns7.txt b/test/boundruns7.txt index 477d639..59aa134 100644 --- a/test/boundruns7.txt +++ b/test/boundruns7.txt @@ -156,20 +156,20 @@ 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 Nisynch_R2 - Fail [at least 5 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 Nisynch_R2 - Fail [at least 5 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 Nisynch_I2 - Fail [at least 5 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,R Secret_R2 Ni Fail [at least 11 attacks] +claim needhamschroederpk,R Secret_R1 Nr Fail [at least 11 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] @@ -230,10 +230,10 @@ 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,S Secret_8 N2 Fail [at least 8 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 spliceAS,C Secret_7 N2 Fail [at least 10 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] @@ -255,10 +255,10 @@ 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,S Secret_8 N2 Fail [at least 8 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 spliceAShc,C Secret_7 N2 Fail [at least 10 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] @@ -344,10 +344,10 @@ 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,S Secret_7 Ka Fail [at least 5 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 tmn,A Secret_5 Ka Fail [at least 5 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] @@ -399,7 +399,7 @@ 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,S Secret_8 N2 Ok [proof of correctness] 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] @@ -499,7 +499,7 @@ 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 nsl3th3ni,I Nisynch_i2 - 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] diff --git a/test/boundtest.sh b/test/boundtest.sh index d35ea1d..52b7a74 100755 --- a/test/boundtest.sh +++ b/test/boundtest.sh @@ -9,4 +9,4 @@ rm boundruns?.txt \time -v -o boundtime4.txt ./test-all.sh scyther -r4 --plain >boundruns4.txt \time -v -o boundtime5.txt ./test-all.sh scyther -r5 --plain >boundruns5.txt \time -v -o boundtime6.txt ./test-all.sh scyther -r6 --plain >boundruns6.txt -\time -v -o boundtime7.txt ./test-all.sh scyther -r6 --plain >boundruns7.txt +\time -v -o boundtime7.txt ./test-all.sh scyther -r7 --plain >boundruns7.txt diff --git a/test/boundtime7.txt b/test/boundtime7.txt index e2bb9b8..101cac3 100644 --- a/test/boundtime7.txt +++ b/test/boundtime7.txt @@ -1,9 +1,9 @@ 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 + Command being timed: "./test-all.sh scyther -r7 --plain" + User time (seconds): 2159.35 + System time (seconds): 5.62 + Percent of CPU this job got: 39% + Elapsed (wall clock) time (h:mm:ss or m:ss): 1:30:45 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 @@ -11,9 +11,9 @@ Command exited with non-zero status 123 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 + Minor (reclaiming a frame) page faults: 105332 + Voluntary context switches: 202 + Involuntary context switches: 541255 Swaps: 0 File system inputs: 0 File system outputs: 0