Lemma legend

• step1 = step1 (exists-trace) ----- NOT displayed
• step2 = step2 (exists-trace) ----- NOT displayed
• protocol_completion = protocol_completion (exists-trace) ----- NOT displayed
• IA_D = s_inj_agree_simple_device (all-traces) ----- displayed
• IA_N = s_inj_agree_simple_network (all-traces) ----- displayed
• NIA_D = s_noninj_agree_simple_device (all-traces) ----- displayed
• NIA_N = s_noninj_agree_simple_network (all-traces) ----- displayed
• IAK = s_inj_agree_keys (all-traces) ----- displayed
• NIAK = s_noninj_agree_keys (all-traces) ----- displayed
• KF_N = keys_freshness_network (all-traces) ----- displayed
• KF_D = keys_freshness_device (all-traces) ----- displayed
• S_D = weaksecret_device (all-traces) ----- displayed
• S_N = weaksecret_network (all-traces) ----- displayed

Protocol	Option	Misuse case	Misuse nonce	IA_D	IA_N	NIA_D	NIA_N	IAK	NIAK	KF_N	KF_D	S_D	S_N
lorawan_10_basic.spthy	Standard	No misuse	N/A
lorawan_10_leak_always_0.spthy	Standard	Leak always	N0
lorawan_10_leak_always_1.spthy	Standard	Leak always	N1
lorawan_10_reuse_once_0_0.spthy	Standard	Reuse once	N0 = N0
lorawan_10_reuse_once_0_1.spthy	Standard	Reuse once	N0 = N1
lorawan_10_reuse_once_1_1.spthy	Standard	Reuse once	N1 = N1
lorawan_10_reuse_always_0.spthy	Standard	Reuse always	N0
lorawan_10_reuse_always_1.spthy	Standard	Reuse always	N1