Runner

wpa3.spthy

Lemma legend

Opt: Standard

File : wpa3_basic.spthy

cli : tamarin-prover wpa3_basic.spthy --prove

Results : wpa3_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 : wpa3_leak_always_0.spthy

cli : tamarin-prover wpa3_leak_always_0.spthy --prove

Results : wpa3_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:

File : wpa3_leak_always_1.spthy

cli : tamarin-prover wpa3_leak_always_1.spthy --prove

Results : wpa3_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:

File : wpa3_leak_always_2.spthy

cli : tamarin-prover wpa3_leak_always_2.spthy --prove

Results : wpa3_leak_always_2_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 : wpa3_leak_always_3.spthy

cli : tamarin-prover wpa3_leak_always_3.spthy --prove

Results : wpa3_leak_always_3_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 : wpa3_reuse_once_0_0.spthy

cli : tamarin-prover wpa3_reuse_once_0_0.spthy --prove

Results : wpa3_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 : wpa3_reuse_once_0_1.spthy

cli : tamarin-prover wpa3_reuse_once_0_1.spthy --prove

Results : wpa3_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 : wpa3_reuse_once_0_2.spthy

cli : tamarin-prover wpa3_reuse_once_0_2.spthy --prove

Results : wpa3_reuse_once_0_2_results.spthy

  • IA_AP:
  • IA_C:
  • NIA_AP:
  • NIA_C:
  • IAK_AP:
  • IAK_C:
  • NIAK_AP:
  • NIAK_C:
  • S_AP:
  • S_C:

File : wpa3_reuse_once_0_3.spthy

cli : tamarin-prover wpa3_reuse_once_0_3.spthy --prove

Results : wpa3_reuse_once_0_3_results.spthy

  • IA_AP:
  • IA_C:
  • NIA_AP:
  • NIA_C:
  • IAK_AP:
  • IAK_C:
  • NIAK_AP:
  • NIAK_C:
  • S_AP:
  • S_C:

File : wpa3_reuse_once_1_1.spthy

cli : tamarin-prover wpa3_reuse_once_1_1.spthy --prove

Results : wpa3_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 : wpa3_reuse_once_1_2.spthy

cli : tamarin-prover wpa3_reuse_once_1_2.spthy --prove

Results : wpa3_reuse_once_1_2_results.spthy

  • IA_AP:
  • IA_C:
  • NIA_AP:
  • NIA_C:
  • IAK_AP:
  • IAK_C:
  • NIAK_AP:
  • NIAK_C:
  • S_AP:
  • S_C:

File : wpa3_reuse_once_1_3.spthy

cli : tamarin-prover wpa3_reuse_once_1_3.spthy --prove

Results : wpa3_reuse_once_1_3_results.spthy

  • IA_AP:
  • IA_C:
  • NIA_AP:
  • NIA_C:
  • IAK_AP:
  • IAK_C:
  • NIAK_AP:
  • NIAK_C:
  • S_AP:
  • S_C:

File : wpa3_reuse_once_2_2.spthy

cli : tamarin-prover wpa3_reuse_once_2_2.spthy --prove

Results : wpa3_reuse_once_2_2_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 : wpa3_reuse_once_2_3.spthy

cli : tamarin-prover wpa3_reuse_once_2_3.spthy --prove

Results : wpa3_reuse_once_2_3_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 : wpa3_reuse_once_3_3.spthy

cli : tamarin-prover wpa3_reuse_once_3_3.spthy --prove

Results : wpa3_reuse_once_3_3_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 : wpa3_reuse_always_0.spthy

cli : tamarin-prover wpa3_reuse_always_0.spthy --prove

Results : wpa3_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 : wpa3_reuse_always_1.spthy

cli : tamarin-prover wpa3_reuse_always_1.spthy --prove

Results : wpa3_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:

File : wpa3_reuse_always_2.spthy

cli : tamarin-prover wpa3_reuse_always_2.spthy --prove

Results : wpa3_reuse_always_2_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 : wpa3_reuse_always_3.spthy

cli : tamarin-prover wpa3_reuse_always_3.spthy --prove

Results : wpa3_reuse_always_3_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: Freshness

File : wpa3_basic.spthy

cli : tamarin-prover -DFreshness wpa3_basic.spthy --prove

Results : wpa3_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 : wpa3_leak_always_0.spthy

cli : tamarin-prover -DFreshness wpa3_leak_always_0.spthy --prove

Results : wpa3_leak_always_0_results.spthy

  • KF_C:
  • KF_AP:

File : wpa3_leak_always_1.spthy

cli : tamarin-prover -DFreshness wpa3_leak_always_1.spthy --prove

Results : wpa3_leak_always_1_results.spthy

  • KF_C:
  • KF_AP:

File : wpa3_leak_always_2.spthy

cli : tamarin-prover -DFreshness wpa3_leak_always_2.spthy --prove

Results : wpa3_leak_always_2_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 : wpa3_leak_always_3.spthy

cli : tamarin-prover -DFreshness wpa3_leak_always_3.spthy --prove

Results : wpa3_leak_always_3_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 : wpa3_reuse_once_0_0.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_0_0.spthy --prove

Results : wpa3_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 : wpa3_reuse_once_0_1.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_0_1.spthy --prove

Results : wpa3_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 : wpa3_reuse_once_0_2.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_0_2.spthy --prove

Results : wpa3_reuse_once_0_2_results.spthy

  • KF_C:
  • KF_AP:

File : wpa3_reuse_once_0_3.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_0_3.spthy --prove

Results : wpa3_reuse_once_0_3_results.spthy

  • KF_C:
  • KF_AP:

File : wpa3_reuse_once_1_1.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_1_1.spthy --prove

Results : wpa3_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 : wpa3_reuse_once_1_2.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_1_2.spthy --prove

Results : wpa3_reuse_once_1_2_results.spthy

  • KF_C:
  • KF_AP:

File : wpa3_reuse_once_1_3.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_1_3.spthy --prove

Results : wpa3_reuse_once_1_3_results.spthy

  • KF_C:
  • KF_AP:

File : wpa3_reuse_once_2_2.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_2_2.spthy --prove

Results : wpa3_reuse_once_2_2_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 : wpa3_reuse_once_2_3.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_2_3.spthy --prove

Results : wpa3_reuse_once_2_3_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 : wpa3_reuse_once_3_3.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_once_3_3.spthy --prove

Results : wpa3_reuse_once_3_3_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 : wpa3_reuse_always_0.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_always_0.spthy --prove

Results : wpa3_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 : wpa3_reuse_always_1.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_always_1.spthy --prove

Results : wpa3_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:

File : wpa3_reuse_always_2.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_always_2.spthy --prove

Results : wpa3_reuse_always_2_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 : wpa3_reuse_always_3.spthy

cli : tamarin-prover -DFreshness wpa3_reuse_always_3.spthy --prove

Results : wpa3_reuse_always_3_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: