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]
