Runner

bluetooth_nc.spthy

Lemma legend

Opt: Standard

File : bluetooth_nc_basic.spthy

cli : tamarin-prover bluetooth_nc_basic.spthy --prove

Results : bluetooth_nc_basic_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_leak_always_0.spthy

cli : tamarin-prover bluetooth_nc_leak_always_0.spthy --prove

Results : bluetooth_nc_leak_always_0_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_leak_always_1.spthy

cli : tamarin-prover bluetooth_nc_leak_always_1.spthy --prove

Results : bluetooth_nc_leak_always_1_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_reuse_once_0_0.spthy

cli : tamarin-prover bluetooth_nc_reuse_once_0_0.spthy --prove

Results : bluetooth_nc_reuse_once_0_0_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_reuse_once_0_1.spthy

cli : tamarin-prover bluetooth_nc_reuse_once_0_1.spthy --prove

Results : bluetooth_nc_reuse_once_0_1_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_reuse_once_1_1.spthy

cli : tamarin-prover bluetooth_nc_reuse_once_1_1.spthy --prove

Results : bluetooth_nc_reuse_once_1_1_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_reuse_always_0.spthy

cli : tamarin-prover bluetooth_nc_reuse_always_0.spthy --prove

Results : bluetooth_nc_reuse_always_0_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R:

File : bluetooth_nc_reuse_always_1.spthy

cli : tamarin-prover bluetooth_nc_reuse_always_1.spthy --prove

Results : bluetooth_nc_reuse_always_1_results.spthy

  • NIA_I:
  • NIA_R:
  • IA_I:
  • IA_R:
  • NIAK_I:
  • NIAK_R:
  • IAK_I:
  • IAK_R:
  • S_I:
  • S_R:
  • KF_I:
  • KF_R: