65 lines
5.2 KiB
Plaintext
65 lines
5.2 KiB
Plaintext
|
BKE.spdl claim bke,I SKR_4 kir Ok [no attack within bounds]
|
||
|
|
BKE.spdl claim bke,R SKR_7 kir Ok [no attack within bounds]
|
||
|
|
TLS-Paulson.spdl claim tlspaulson,a SKR_9a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [no attack within bounds]
|
||
|
|
TLS-Paulson.spdl claim tlspaulson,a SKR_9b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [no attack within bounds]
|
||
|
|
TLS-Paulson.spdl claim tlspaulson,b SKR_10a hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) Ok [no attack within bounds]
|
||
|
|
TLS-Paulson.spdl claim tlspaulson,b SKR_10b hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) Ok [no attack within bounds]
|
||
|
|
ccitt509-1.spdl claim ccitt509-1,R Nisynch_3 - Ok [proof of correctness]
|
||
|
|
ccitt509-1c.spdl claim ccitt509-1c,R Nisynch_3 - Ok [proof of correctness]
|
||
|
|
ccitt509-3.spdl claim ccitt509-3,I Nisynch_I1 - Ok [proof of correctness]
|
||
|
|
ccitt509-3.spdl claim ccitt509-3,I Secret_I2 Ya Ok [proof of correctness]
|
||
|
|
ccitt509-3.spdl claim ccitt509-3,I Secret_I3 Yb Ok [proof of correctness]
|
||
|
|
ccitt509-3.spdl claim ccitt509-3,R Nisynch_R1 - Fail [at least 3 attacks]
|
||
|
|
ccitt509-3.spdl claim ccitt509-3,R Secret_R2 Ya Ok [no attack within bounds]
|
||
|
|
ccitt509-3.spdl claim ccitt509-3,R Secret_R3 Yb Ok [no attack within bounds]
|
||
|
|
ccitt509-ban3.spdl claim ccitt509-ban3,I Nisynch_4 - Ok [proof of correctness]
|
||
|
|
ccitt509-ban3.spdl claim ccitt509-ban3,R Nisynch_5 - Ok [no attack within bounds]
|
||
|
|
needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,I Secret_I1 Ni Ok [no attack within bounds]
|
||
|
|
needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,I Secret_I2 Nr Ok [no attack within bounds]
|
||
|
|
needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,I Nisynch_I3 - Fail [at least 3 attacks]
|
||
|
|
needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,R Secret_R1 Nr Ok [no attack within bounds]
|
||
|
|
needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,R Secret_R2 Ni Ok [no attack within bounds]
|
||
|
|
needham-schroeder-lowe.spdl claim needhamschroederpk-Lowe,R Nisynch_R3 - Fail [at least 3 attacks]
|
||
|
|
needham-schroeder.spdl claim needhamschroederpk,I Secret_I1 Ni Ok [no attack within bounds]
|
||
|
|
needham-schroeder.spdl claim needhamschroederpk,I Secret_I2 Nr Ok [no attack within bounds]
|
||
|
|
needham-schroeder.spdl claim needhamschroederpk,I Nisynch_I3 - Fail [at least 3 attacks]
|
||
|
|
needham-schroeder.spdl claim needhamschroederpk,R Secret_R1 Nr Fail [at least 5 attacks]
|
||
|
|
needham-schroeder.spdl claim needhamschroederpk,R Secret_R2 Ni Fail [at least 5 attacks]
|
||
|
|
needham-schroeder.spdl claim needhamschroederpk,R Nisynch_R3 - Fail [at least 3 attacks]
|
||
|
|
smartright.spdl claim smartright,R Nisynch_R1 - Fail [at least 1 attack]
|
||
|
|
splice-as-cj.spdl claim spliceAS-CJ,I Secret_7 N2 Ok [no attack within bounds]
|
||
|
|
splice-as-cj.spdl claim spliceAS-CJ,I Niagree_9 - Fail [at least 1 attack]
|
||
|
|
splice-as-cj.spdl claim spliceAS-CJ,I Nisynch_10 - Fail [at least 1 attack]
|
||
|
|
splice-as-cj.spdl claim spliceAS-CJ,R Secret_8 N2 Ok [no attack within bounds]
|
||
|
|
splice-as-cj.spdl claim spliceAS-CJ,R Niagree_11 - Fail [at least 1 attack]
|
||
|
|
splice-as-cj.spdl claim spliceAS-CJ,R Nisynch_12 - Fail [at least 1 attack]
|
||
|
|
splice-as-hc.spdl claim spliceAS-HC,I Secret_7 N2 Ok [no attack within bounds]
|
||
|
|
splice-as-hc.spdl claim spliceAS-HC,I Niagree_9 - Fail [at least 1 attack]
|
||
|
|
splice-as-hc.spdl claim spliceAS-HC,I Nisynch_10 - Fail [at least 1 attack]
|
||
|
|
splice-as-hc.spdl claim spliceAS-HC,R Secret_8 N2 Ok [no attack within bounds]
|
||
|
|
splice-as-hc.spdl claim spliceAS-HC,R Niagree_11 - Fail [at least 1 attack]
|
||
|
|
splice-as-hc.spdl claim spliceAS-HC,R Nisynch_12 - Fail [at least 1 attack]
|
||
|
|
splice-as.spdl claim spliceAS,I Secret_7 N2 Ok [no attack within bounds]
|
||
|
|
splice-as.spdl claim spliceAS,I Niagree_9 - Fail [at least 1 attack]
|
||
|
|
splice-as.spdl claim spliceAS,I Nisynch_10 - Fail [at least 1 attack]
|
||
|
|
splice-as.spdl claim spliceAS,R Secret_8 N2 Ok [no attack within bounds]
|
||
|
|
splice-as.spdl claim spliceAS,R Niagree_11 - Fail [at least 1 attack]
|
||
|
|
splice-as.spdl claim spliceAS,R Nisynch_12 - Fail [at least 1 attack]
|
||
|
|
woo-lam-pi-1.spdl claim woolamPi-1,R Nisynch_R1 - Fail [at least 2 attacks]
|
||
|
|
woo-lam-pi-2.spdl claim woolamPi-2,R Nisynch_R1 - Fail [at least 3 attacks]
|
||
|
|
woo-lam-pi-3.spdl claim woolamPi-3,R Nisynch_R1 - Fail [at least 2 attacks]
|
||
|
|
woo-lam-pi-f.spdl claim woolamPi-f,R Nisynch_R1 - Fail [at least 1 attack]
|
||
|
|
woo-lam-pi.spdl claim woolamPi,R Nisynch_R1 - Fail [at least 2 attacks]
|
||
|
|
yahalom-ban-paulson-modified.spdl claim yahalom-BAN-Paulson-modified,A Secret_5 kab Ok [no attack within bounds]
|
||
|
|
yahalom-ban-paulson-modified.spdl claim yahalom-BAN-Paulson-modified,B Secret_6 kab Ok [no attack within bounds]
|
||
|
|
yahalom-ban-paulson.spdl claim yahalom-BAN-Paulson,A SKR_5 kab Ok [no attack within bounds]
|
||
|
|
yahalom-ban-paulson.spdl claim yahalom-BAN-Paulson,B SKR_6 kab Ok [no attack within bounds]
|
||
|
|
yahalom-lowe.spdl claim yahalom-Lowe,I Secret_I1 Kir Ok [proof of correctness]
|
||
|
|
yahalom-lowe.spdl claim yahalom-Lowe,I Nisynch_I2 - Ok [proof of correctness]
|
||
|
|
yahalom-lowe.spdl claim yahalom-Lowe,R Secret_R1 Kir Ok [proof of correctness]
|
||
|
|
yahalom-lowe.spdl claim yahalom-Lowe,R Nisynch_R2 - Ok [no attack within bounds]
|
||
|
|
yahalom.spdl claim yahalom,I Secret_I1 Kir Ok [no attack within bounds]
|
||
|
|
yahalom.spdl claim yahalom,R Secret_R1 Kir Ok [no attack within bounds]
|
||
|
|
yahalom.spdl claim yahalom,S Secret_S1 Ni Fail [at least 1 attack]
|
||
|
|
yahalom.spdl claim yahalom,S Secret_S2 Nr Ok [no attack within bounds]
|