Runner

wpa2.spthy

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

Opt: StaticKey

File : wpa2_basic.spthy

cli : tamarin-prover wpa2_basic.spthy --prove

Results : wpa2_basic_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_leak_always_0.spthy

cli : tamarin-prover wpa2_leak_always_0.spthy --prove

Results : wpa2_leak_always_0_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_leak_always_1.spthy

cli : tamarin-prover wpa2_leak_always_1.spthy --prove

Results : wpa2_leak_always_1_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_once_0_0.spthy

cli : tamarin-prover wpa2_reuse_once_0_0.spthy --prove

Results : wpa2_reuse_once_0_0_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_once_0_1.spthy

cli : tamarin-prover wpa2_reuse_once_0_1.spthy --prove

Results : wpa2_reuse_once_0_1_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_once_1_1.spthy

cli : tamarin-prover wpa2_reuse_once_1_1.spthy --prove

Results : wpa2_reuse_once_1_1_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_always_0.spthy

cli : tamarin-prover wpa2_reuse_always_0.spthy --prove

Results : wpa2_reuse_always_0_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_always_1.spthy

cli : tamarin-prover wpa2_reuse_always_1.spthy --prove

Results : wpa2_reuse_always_1_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

Opt: FreshKey

File : wpa2_basic.spthy

cli : tamarin-prover -DFreshKey wpa2_basic.spthy --prove

Results : wpa2_basic_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_leak_always_0.spthy

cli : tamarin-prover -DFreshKey wpa2_leak_always_0.spthy --prove

Results : wpa2_leak_always_0_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_leak_always_1.spthy

cli : tamarin-prover -DFreshKey wpa2_leak_always_1.spthy --prove

Results : wpa2_leak_always_1_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_once_0_0.spthy

cli : tamarin-prover -DFreshKey wpa2_reuse_once_0_0.spthy --prove

Results : wpa2_reuse_once_0_0_results.spthy

IA_AP:
IA_C:
NIA_AP:
NIA_C:
IAK_AP:
IAK_C:
NIAK_AP:
NIAK_C:
S_AP:
S_C:
KF_C:
KF_AP:

File : wpa2_reuse_once_0_1.spthy

cli : tamarin-prover -DFreshKey wpa2_reuse_once_0_1.spthy --prove