diff --git a/test/compareheuristics.txt b/test/compareheuristics.txt new file mode 100644 index 0000000..341a868 --- /dev/null +++ b/test/compareheuristics.txt @@ -0,0 +1,20 @@ +G-sel Decide Attack Proof Bound TOuts Claims Prots States BndTo*Sts + +-1 28[+]% 92[+] 54[+] 46[-] 326[-] 518 122 4107709[-] 568441202256 +32 60[+]% 207[+] 108[+] 167 36[-] 518 122 447456[-] 18439214304 +2 74[+]% 229[+] 157[+] 132 0[-] 518 122 184723[-] 3218613552[-] +128 77[+]% 229[+] 171[+] 118 0[-] 518 122 195636 2724035664[-] +162 84[+]% 229[+] 207[+] 82 0[-] 518 122 100228[-] 673933072[-] + +Goal selector scan completed. + +34 shared problem protocols: +['/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/kaochow-v2.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder-sk.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/denning-sacco-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub-hwang.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/kaochow-v3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ksl.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ksl-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/denning-sacco.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder-sk-amend.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew-ban-concrete.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/wmf.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/wmf-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub-guttman-hwang.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/f4.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/isoiec11770-2-13.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/gong-nonce-b.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ksl.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/denning-sacco-shared.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/f5.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/kaochow-v2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/kaochow-palm.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ns-symmetric-amended.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ns-symmetric.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/gong-nonce.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/localclaims-seq1.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/splice-as-hc-cj.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/kaochow-v3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/localclaims-breaker.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bunava-1-4.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ibe-ns.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1seq2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1seq2-rename-ni.spdl'] + +32 has 38 extra problems: ['/home/cas/svn/ecss/protocols/spdl/SPORE/splice-as.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/otwayrees.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/kaochow.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/splice-as-hc.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ccitt509-3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/woo-lam.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ccitt509-ban3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/splice-as-cj.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub-keycompromise.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub-guttman.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/andrew-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke-broken.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke-one.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/boyd.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/woolam-cmv.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ccitt509-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/otwayrees.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/kaochow.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke-variation.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/unknown2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson-avispa.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1par2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-2.spdl', '/home/cas/svn/ecss/protocols/spdl/demo/nsl3.spdl'] +128 has 11 extra problems: ['/home/cas/svn/ecss/protocols/spdl/SPORE/ccitt509-3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3-nisynch-rep.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson-avispa.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1par2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-2.spdl', '/home/cas/svn/ecss/protocols/spdl/demo/nsl3.spdl'] +2 has 17 extra problems: ['/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/otwayrees.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ccitt509-ban3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/andrew-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ccitt509-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3-nisynch-rep.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson-avispa.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1par2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-2.spdl', '/home/cas/svn/ecss/protocols/spdl/demo/nsl3.spdl'] +162 has 1 extra problems: ['/home/cas/svn/ecss/protocols/spdl/misc/kaochow.spdl'] +-1 has 56 extra problems: ['/home/cas/svn/ecss/protocols/spdl/SPORE/splice-as.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/otwayrees.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/kaochow.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/splice-as-hc.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ccitt509-3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/woo-lam.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/ccitt509-ban3.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/splice-as-cj.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/tmn.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/andrew-lowe-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/yahalom.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/needham-schroeder.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub-keycompromise.spdl', '/home/cas/svn/ecss/protocols/spdl/SPORE/neumannstub-guttman.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/five-run-bound.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/andrew-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke-broken.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/splice-as.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke-one.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl7.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ns3-brutus.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/boyd.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/splice-as-hc.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/woolam-cmv.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/andrew-lowe-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ccitt509-ban.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bunava-2-3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/wmf-brutus.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/otwayrees.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tmn.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/kaochow.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke-variation.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom-lowe.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bke.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/bunava-2-4.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/unknown2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/speedtest.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/yahalom.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/ns3.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/nsl3-nisynch-rep.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/tls-paulson-avispa.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1par2.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-1.spdl', '/home/cas/svn/ecss/protocols/spdl/misc/trondheim/th-2.spdl', '/home/cas/svn/ecss/protocols/spdl/demo/nsl3.spdl', '/home/cas/svn/ecss/protocols/spdl/demo/ns3.spdl'] + +