Runner

NSLPK3.spthy

Lemma legend

types = types (all-traces) ----- NOT displayed
S_Ni_I = nonce_secrecy_I_Ni (all-traces) ----- NOT displayed
S_Nr_I = nonce_secrecy_I_Nr (all-traces) ----- NOT displayed
S_Ni_R = nonce_secrecy_R_Ni (all-traces) ----- NOT displayed
S_Nr_R = nonce_secrecy_R_Nr (all-traces) ----- NOT displayed
IA_I = injective_agreeI (all-traces) ----- displayed
IA_R = injective_agreeR (all-traces) ----- displayed
NIA_I = non_injective_agreeI (all-traces) ----- displayed
NIA_R = non_injective_agreeR (all-traces) ----- displayed
session_key_setup_possible = session_key_setup_possible (exists-trace) ----- NOT displayed

Opt: Standard

File : NSLPK3_basic.spthy

cli : tamarin-prover NSLPK3_basic.spthy --prove

Results : NSLPK3_basic_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_leak_always_0.spthy

cli : tamarin-prover NSLPK3_leak_always_0.spthy --prove

Results : NSLPK3_leak_always_0_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_leak_always_1.spthy

cli : tamarin-prover NSLPK3_leak_always_1.spthy --prove

Results : NSLPK3_leak_always_1_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_reuse_once_0_0.spthy

cli : tamarin-prover NSLPK3_reuse_once_0_0.spthy --prove

Results : NSLPK3_reuse_once_0_0_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_reuse_once_0_1.spthy

cli : tamarin-prover NSLPK3_reuse_once_0_1.spthy --prove

Results : NSLPK3_reuse_once_0_1_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_reuse_once_1_1.spthy

cli : tamarin-prover NSLPK3_reuse_once_1_1.spthy --prove

Results : NSLPK3_reuse_once_1_1_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_reuse_always_0.spthy

cli : tamarin-prover NSLPK3_reuse_always_0.spthy --prove

Results : NSLPK3_reuse_always_0_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R:

File : NSLPK3_reuse_always_1.spthy

cli : tamarin-prover NSLPK3_reuse_always_1.spthy --prove

Results : NSLPK3_reuse_always_1_results.spthy

IA_I:
IA_R:
NIA_I:
NIA_R: