Lemma legend

• functional_4way = functional_4way (exists-trace) ----- NOT displayed
• IA_AP = inj_agree_ap (all-traces) ----- displayed
• IA_C = inj_agree_client (all-traces) ----- displayed
• NIA_AP = noninj_agree_ap (all-traces) ----- displayed
• NIA_C = noninj_agree_client (all-traces) ----- displayed
• IAK_AP = keys_inj_agree_ap (all-traces) ----- displayed
• IAK_C = keys_inj_agree_client (all-traces) ----- displayed
• NIAK_AP = keys_noninj_agree_ap (all-traces) ----- displayed
• NIAK_C = keys_noninj_agree_client (all-traces) ----- displayed
• S_AP = weak_secrecy_ap (all-traces) ----- displayed
• S_C = weak_secrecy_Client (all-traces) ----- displayed
• KF_C = key_freshness_client (all-traces) ----- displayed
• KF_AP = key_freshness_ap (all-traces) ----- displayed

Protocol	Option	Misuse case	Misuse nonce	IA_AP	IA_C	NIA_AP	NIA_C	IAK_AP	IAK_C	NIAK_AP	NIAK_C	S_AP	S_C	KF_C	KF_AP
wpa2_basic.spthy	StaticKey	No misuse	N/A
wpa2_leak_always_0.spthy	StaticKey	Leak always	N0
wpa2_leak_always_1.spthy	StaticKey	Leak always	N1
wpa2_reuse_once_0_0.spthy	StaticKey	Reuse once	N0 = N0
wpa2_reuse_once_0_1.spthy	StaticKey	Reuse once	N0 = N1
wpa2_reuse_once_1_1.spthy	StaticKey	Reuse once	N1 = N1
wpa2_reuse_always_0.spthy	StaticKey	Reuse always	N0
wpa2_reuse_always_1.spthy	StaticKey	Reuse always	N1
wpa2_basic.spthy	FreshKey	No misuse	N/A
wpa2_leak_always_0.spthy	FreshKey	Leak always	N0
wpa2_leak_always_1.spthy	FreshKey	Leak always	N1
wpa2_reuse_once_0_0.spthy	FreshKey	Reuse once	N0 = N0
wpa2_reuse_once_0_1.spthy	FreshKey	Reuse once	N0 = N1
wpa2_reuse_once_1_1.spthy	FreshKey	Reuse once	N1 = N1
wpa2_reuse_always_0.spthy	FreshKey	Reuse always	N0
wpa2_reuse_always_1.spthy	FreshKey	Reuse always	N1