Results table

wpa3.spthy

Lemma legend

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
wpa3_basic.spthy Standard No misuse N/A
wpa3_leak_always_0.spthy Standard Leak always N0
wpa3_leak_always_1.spthy Standard Leak always N1
wpa3_leak_always_2.spthy Standard Leak always N2
wpa3_leak_always_3.spthy Standard Leak always N3
wpa3_reuse_once_0_0.spthy Standard Reuse once N0 = N0
wpa3_reuse_once_0_1.spthy Standard Reuse once N0 = N1
wpa3_reuse_once_0_2.spthy Standard Reuse once N0 = N2
wpa3_reuse_once_0_3.spthy Standard Reuse once N0 = N3
wpa3_reuse_once_1_1.spthy Standard Reuse once N1 = N1
wpa3_reuse_once_1_2.spthy Standard Reuse once N1 = N2
wpa3_reuse_once_1_3.spthy Standard Reuse once N1 = N3
wpa3_reuse_once_2_2.spthy Standard Reuse once N2 = N2
wpa3_reuse_once_2_3.spthy Standard Reuse once N2 = N3
wpa3_reuse_once_3_3.spthy Standard Reuse once N3 = N3
wpa3_reuse_always_0.spthy Standard Reuse always N0
wpa3_reuse_always_1.spthy Standard Reuse always N1
wpa3_reuse_always_2.spthy Standard Reuse always N2
wpa3_reuse_always_3.spthy Standard Reuse always N3
wpa3_basic.spthy Freshness No misuse N/A
wpa3_leak_always_0.spthy Freshness Leak always N0
wpa3_leak_always_1.spthy Freshness Leak always N1
wpa3_leak_always_2.spthy Freshness Leak always N2
wpa3_leak_always_3.spthy Freshness Leak always N3
wpa3_reuse_once_0_0.spthy Freshness Reuse once N0 = N0
wpa3_reuse_once_0_1.spthy Freshness Reuse once N0 = N1
wpa3_reuse_once_0_2.spthy Freshness Reuse once N0 = N2
wpa3_reuse_once_0_3.spthy Freshness Reuse once N0 = N3
wpa3_reuse_once_1_1.spthy Freshness Reuse once N1 = N1
wpa3_reuse_once_1_2.spthy Freshness Reuse once N1 = N2
wpa3_reuse_once_1_3.spthy Freshness Reuse once N1 = N3
wpa3_reuse_once_2_2.spthy Freshness Reuse once N2 = N2
wpa3_reuse_once_2_3.spthy Freshness Reuse once N2 = N3
wpa3_reuse_once_3_3.spthy Freshness Reuse once N3 = N3
wpa3_reuse_always_0.spthy Freshness Reuse always N0
wpa3_reuse_always_1.spthy Freshness Reuse always N1
wpa3_reuse_always_2.spthy Freshness Reuse always N2
wpa3_reuse_always_3.spthy Freshness Reuse always N3