Lemma legend

• WorkingDH = WorkingDH (exists-trace) ----- NOT displayed
• WorkingCommit = WorkingCommit (exists-trace) ----- NOT displayed
• IA_C = InjAgreeClient (all-traces) ----- displayed
• IA_AP = InjAgreeAP (all-traces) ----- displayed
• NIA_C = NonInjAgreeClient (all-traces) ----- displayed
• NIA_AP = NonInjAgreeAP (all-traces) ----- displayed
• IAK_C = KeysInjAgreeClient (all-traces) ----- displayed
• IAK_AP = KeysInjAgreeAP (all-traces) ----- displayed
• NIAK_C = KeysNonInjAgreeClient (all-traces) ----- displayed
• NIAK_AP = KeysNonInjAgreeAP (all-traces) ----- displayed
• S_AP = WeakSecrecyAP (all-traces) ----- displayed
• S_C = WeakSecrecyClient (all-traces) ----- displayed
• KF_C = KeyFreshnessClient (all-traces) ----- displayed
• KF_AP = KeyFreshnessAP (all-traces) ----- displayed

Protocol	Option	Misuse case	Misuse nonce	IA_C	IA_AP	NIA_C	NIA_AP	IAK_C	IAK_AP	NIAK_C	NIAK_AP	S_AP	S_C	KF_C	KF_AP
dragonfly_basic.spthy	NoPatchReflection	No misuse	N/A
dragonfly_leak_always_0.spthy	NoPatchReflection	Leak always	N0
dragonfly_leak_always_1.spthy	NoPatchReflection	Leak always	N1
dragonfly_reuse_once_0_0.spthy	NoPatchReflection	Reuse once	N0 = N0
dragonfly_reuse_once_0_1.spthy	NoPatchReflection	Reuse once	N0 = N1
dragonfly_reuse_once_1_1.spthy	NoPatchReflection	Reuse once	N1 = N1
dragonfly_reuse_always_0.spthy	NoPatchReflection	Reuse always	N0
dragonfly_reuse_always_1.spthy	NoPatchReflection	Reuse always	N1
dragonfly_basic.spthy	PatchReflection	No misuse	N/A
dragonfly_leak_always_0.spthy	PatchReflection	Leak always	N0
dragonfly_leak_always_1.spthy	PatchReflection	Leak always	N1
dragonfly_reuse_once_0_0.spthy	PatchReflection	Reuse once	N0 = N0
dragonfly_reuse_once_0_1.spthy	PatchReflection	Reuse once	N0 = N1
dragonfly_reuse_once_1_1.spthy	PatchReflection	Reuse once	N1 = N1
dragonfly_reuse_always_0.spthy	PatchReflection	Reuse always	N0
dragonfly_reuse_always_1.spthy	PatchReflection	Reuse always	N1