Lemma legend

• weak_functional = weak_functional (exists-trace) ----- NOT displayed
• functional = functional (exists-trace) ----- NOT displayed
• NIA_I = noninj_agree_init (all-traces) ----- displayed
• NIA_R = noninj_agree_resp (all-traces) ----- displayed
• IA_I = inj_agree_init (all-traces) ----- displayed
• IA_R = inj_agree_resp (all-traces) ----- displayed
• NIAK_I = noninj_agree_init_keys (all-traces) ----- displayed
• NIAK_R = noninj_agree_resp_keys (all-traces) ----- displayed
• IAK_I = inj_agree_init_keys (all-traces) ----- displayed
• IAK_R = inj_agree_resp_keys (all-traces) ----- displayed
• S_I = key_secrecy_init (all-traces) ----- displayed
• S_R = key_secrecy_resp (all-traces) ----- displayed
• KF_I = key_freshness_init (all-traces) ----- displayed
• KF_R = key_freshness_resp (all-traces) ----- displayed
• leakage = leakage (all-traces) ----- NOT displayed

Protocol	Option	Misuse case	Misuse nonce	NIA_I	NIA_R	IA_I	IA_R	NIAK_I	NIAK_R	IAK_I	IAK_R	S_I	S_R	KF_I	KF_R
bluetooth_nc_basic.spthy	Standard	No misuse	N/A
bluetooth_nc_leak_always_0.spthy	Standard	Leak always	N0
bluetooth_nc_leak_always_1.spthy	Standard	Leak always	N1
bluetooth_nc_reuse_once_0_0.spthy	Standard	Reuse once	N0 = N0
bluetooth_nc_reuse_once_0_1.spthy	Standard	Reuse once	N0 = N1
bluetooth_nc_reuse_once_1_1.spthy	Standard	Reuse once	N1 = N1
bluetooth_nc_reuse_always_0.spthy	Standard	Reuse always	N0
bluetooth_nc_reuse_always_1.spthy	Standard	Reuse always	N1