Skip to content

Latest commit

 

History

History
451 lines (418 loc) · 49.1 KB

README.md

File metadata and controls

451 lines (418 loc) · 49.1 KB
Raw

Tamarin models of Bluetooth

This project contains Tamarin models of the different Bluetooth technologies: BR/EDR, BLE and BM.

The models represent the different key agreements of each Bluetooth technologies.

All variants of key agreements are represented.

For the analysis, the interaction of each key agreement with each other is studied. In the models, different known cryptographic problems affecting Bluetooth have been represented. Some proposed patches have also been modeled to test for their efficiency.

This way, the analysis of Tamarin of those models gives an up-to-date view of the security of Bluetooth key agreements.

Configuration of the models

In addition of running all key agreement interactions, it is possible to study Bluetooth key agreements in some configuration.

A configuration is defined as a set of cryptographic problems that are represented and a set of patches that are applied.

In BR/EDR, the following configuration macros are defined:

  • NoLowEntropyLegacy: Disables the ability for an attacker to brute-force the PIN used in Legacy PIN Pairing
  • NoLowEntropySecure: Disables the ability for an attacker to brute-force the passkey used in Secure Passkey Entry
  • InitECDHUnpatched: Represents the fact that the Initiator does not verify the validity of the Responder's public key
  • RespECDHUnpatched: Represents the fact that the Responder does not verify the validity of the Initiator's public key

In BLE, the following configuration macros are defined:

  • NoLowEntropyLegacy: Disables the ability for an attacker to brute-force the passkey used in Legacy Passkey Entry
  • NoLowEntropySecure: Disables the ability for an attacker to brute-force the passkey used in Secure Passkey Entry
  • NoMalleableC1: Disables the malleability of the $c1$ commitment function in BLE Legacy Pairing
  • InitECDHUnpatched: Represents the fact that the Initiator does not verify the validity of the Responder's public key
  • RespECDHUnpatched: Represents the fact that the Responder does not verify the validity of the Initiator's public key
  • LowEntropyKeysize: Enables the ability for an attacker to brute-force a key which size had been downgraded

In BM, the following configuration macros are defined:

  • NoLowEntropyAuthValue: Disables the ability for an attacker to brute-force AuthValue used in the Provisioning protocol
  • NoMalleableCMAC: Disables the malleability of the $CMAC$ commitment function Provisioning
  • ProvECDHUnpatched: Represents the fact that the Provisioner does not verify the validity of the Device's public key
  • DevECDHUnpatched: Represents the fact that the Device does not verify the validity of the Provisioner's public key
  • PatchProvisioning1: Represents a proposed patch of Provisioning: the Provisioner should not accept a reflected confirmation value
  • PatchProvisioning2: Represents a proposed patch of Provisioning: the Device computes the commitment value using an inversion of parameters.

Tamarin outputs warnings

For some models, Tamarin will output well-formedness warnings. This is because the models heavily rely on macros, hence when generating a submodel about half of the file is not copied.

However, restrictions are usually copied, and some may rely on action facts that are never generated by this submodel. This only means this restriction is not used by the model, but does not alter the validity of the results.

Command lines

The command lines to run all model in a default configuration are given. Running them from the CLI will not save the output file and parse the results. The default configuration considers that :

  • all imperfections exist
  • but devices have patched ECDH implementations (this is mandated in the specification)
  • 7-bytes keys cannot be brute-forced

Number of properties analysed

In BR/EDR, there are 11 modeled kind of key agreements. This makes 121 possible interactions because the interaction of each key agreement with each one is studied. For each interaction, there are 6 properties studied (5 security properties and 1 functional property). Therefore, running all the commands will prove 726 lemmas (including 605 security properties).

In BLE, there are 13 modeled kind of key agreements. This makes 169 possible interactions because the interaction of each key agreement with each one is studied. For each interaction, there are 6 properties studied (5 security properties and 1 functional property). Therefore, running all the commands will prove 1014 lemmas (including 845 security properties).

In Mesh, there are 8 modeled kind of key agreements. This makes 64 possible interactions because the interaction of each key agreement with each one is studied. For each interaction, there are 10 properties studied (9 security properties and 1 functional property). Therefore, running all the commands will prove 640 lemmas (including 576 security properties).

BR/EDR

tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespLeg -DRespLegPINi -DLegPINiLegPINi -DInputInput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespLeg -DRespLegPINo -DLegPINiLegPINo -DInputOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespLeg -DRespLegPINio -DLegPINiLegPINio -DInputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespLeg -DRespLegPINi -DLegPINoLegPINi -DOutputInput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespLeg -DRespLegPINo -DLegPINoLegPINo -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespLeg -DRespLegPINio -DLegPINoLegPINio -DOutputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespLeg -DRespLegPINi -DLegPINioLegPINi -DInoutInput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespLeg -DRespLegPINo -DLegPINioLegPINo -DInoutOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespLeg -DRespLegPINio -DLegPINioLegPINio -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecJW -DSecJWSecJW --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecPE -DRespSecPEi -DSecJWSecPEi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecPE -DRespSecPEo -DSecJWSecPEo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecPE -DRespSecPEio -DSecJWSecPEio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecNC -DSecJWSecNC --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecOOB -DRespSecOOBi -DSecJWSecOOBi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecOOB -DRespSecOOBo -DSecJWSecOOBo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecOOB -DRespSecOOBio -DSecJWSecOOBio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecJW -DSecPEiSecJW -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecPE -DRespSecPEi -DSecPEiSecPEi -DInputInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecPE -DRespSecPEo -DSecPEiSecPEo -DInputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecPE -DRespSecPEio -DSecPEiSecPEio -DInputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecNC -DSecPEiSecNC -DInputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecOOB -DRespSecOOBi -DSecPEiSecOOBi -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecOOB -DRespSecOOBo -DSecPEiSecOOBo -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecOOB -DRespSecOOBio -DSecPEiSecOOBio -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecJW -DSecPEoSecJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecPE -DRespSecPEi -DSecPEoSecPEi -DOutputInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecPE -DRespSecPEo -DSecPEoSecPEo -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecPE -DRespSecPEio -DSecPEoSecPEio -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecNC -DSecPEoSecNC -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecOOB -DRespSecOOBi -DSecPEoSecOOBi -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecOOB -DRespSecOOBo -DSecPEoSecOOBo -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecOOB -DRespSecOOBio -DSecPEoSecOOBio -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecJW -DSecPEioSecJW -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecPE -DRespSecPEi -DSecPEioSecPEi -DInoutInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecPE -DRespSecPEo -DSecPEioSecPEo -DInoutOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecPE -DRespSecPEio -DSecPEioSecPEio -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecNC -DSecPEioSecNC -DInoutOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecOOB -DRespSecOOBi -DSecPEioSecOOBi -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecOOB -DRespSecOOBo -DSecPEioSecOOBo -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecOOB -DRespSecOOBio -DSecPEioSecOOBio -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecJW -DSecNCSecJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecPE -DRespSecPEi -DSecNCSecPEi -DOutputInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecPE -DRespSecPEo -DSecNCSecPEo -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecPE -DRespSecPEio -DSecNCSecPEio -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecNC -DSecNCSecNC -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecOOB -DRespSecOOBi -DSecNCSecOOBi -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecOOB -DRespSecOOBo -DSecNCSecOOBo -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecOOB -DRespSecOOBio -DSecNCSecOOBio -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecJW -DSecOOBiSecJW --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecPE -DRespSecPEi -DSecOOBiSecPEi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecPE -DRespSecPEo -DSecOOBiSecPEo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecPE -DRespSecPEio -DSecOOBiSecPEio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecNC -DSecOOBiSecNC --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecOOB -DRespSecOOBi -DSecOOBiSecOOBi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecOOB -DRespSecOOBo -DSecOOBiSecOOBo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecOOB -DRespSecOOBio -DSecOOBiSecOOBio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecJW -DSecOOBoSecJW --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecPE -DRespSecPEi -DSecOOBoSecPEi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecPE -DRespSecPEo -DSecOOBoSecPEo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecPE -DRespSecPEio -DSecOOBoSecPEio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecNC -DSecOOBoSecNC --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecOOB -DRespSecOOBi -DSecOOBoSecOOBi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecOOB -DRespSecOOBo -DSecOOBoSecOOBo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecOOB -DRespSecOOBio -DSecOOBoSecOOBio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecJW -DSecOOBioSecJW --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecPE -DRespSecPEi -DSecOOBioSecPEi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecPE -DRespSecPEo -DSecOOBioSecPEo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecPE -DRespSecPEio -DSecOOBioSecPEio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecNC -DSecOOBioSecNC --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecOOB -DRespSecOOBi -DSecOOBioSecOOBi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecOOB -DRespSecOOBo -DSecOOBioSecOOBo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecOOB -DRespSecOOBio -DSecOOBioSecOOBio --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecJW -DLegPINiSecJW -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecPE -DRespSecPEi -DLegPINiSecPEi -DInputInput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecPE -DRespSecPEo -DLegPINiSecPEo -DInputOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecPE -DRespSecPEio -DLegPINiSecPEio -DInputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecNC -DLegPINiSecNC -DInputOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecOOB -DRespSecOOBi -DLegPINiSecOOBi -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecOOB -DRespSecOOBo -DLegPINiSecOOBo -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINi -DRespSec -DRespSecOOB -DRespSecOOBio -DLegPINiSecOOBio -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecJW -DLegPINoSecJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecPE -DRespSecPEi -DLegPINoSecPEi -DOutputInput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecPE -DRespSecPEo -DLegPINoSecPEo -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecPE -DRespSecPEio -DLegPINoSecPEio -DOutputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecNC -DLegPINoSecNC -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecOOB -DRespSecOOBi -DLegPINoSecOOBi -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecOOB -DRespSecOOBo -DLegPINoSecOOBo -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINo -DRespSec -DRespSecOOB -DRespSecOOBio -DLegPINoSecOOBio -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecJW -DLegPINioSecJW -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecPE -DRespSecPEi -DLegPINioSecPEi -DInoutInput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecPE -DRespSecPEo -DLegPINioSecPEo -DInoutOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecPE -DRespSecPEio -DLegPINioSecPEio -DInoutInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecNC -DLegPINioSecNC -DInoutOutput --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecOOB -DRespSecOOBi -DLegPINioSecOOBi -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecOOB -DRespSecOOBo -DLegPINioSecOOBo -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitLeg -DInitLegPINio -DRespSec -DRespSecOOB -DRespSecOOBio -DLegPINioSecOOBio -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegPINi -DSecJWLegPINi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegPINo -DSecJWLegPINo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegPINio -DSecJWLegPINio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegPINi -DSecPEiLegPINi -DInputInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegPINo -DSecPEiLegPINo -DInputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegPINio -DSecPEiLegPINio -DInputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegPINi -DSecPEoLegPINi -DOutputInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegPINo -DSecPEoLegPINo -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegPINio -DSecPEoLegPINio -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegPINi -DSecPEioLegPINi -DInoutInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegPINo -DSecPEioLegPINo -DInoutOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegPINio -DSecPEioLegPINio -DInoutInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegPINi -DSecNCLegPINi -DOutputInput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegPINo -DSecNCLegPINo -DOutputOutput --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegPINio -DSecNCLegPINio -DOutputInout --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegPINi -DSecOOBiLegPINi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegPINo -DSecOOBiLegPINo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegPINio -DSecOOBiLegPINio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegPINi -DSecOOBoLegPINi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegPINo -DSecOOBoLegPINo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegPINio -DSecOOBoLegPINio --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegPINi -DSecOOBioLegPINi --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegPINo -DSecOOBioLegPINo --prove
tamarin-prover bredr.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegPINio -DSecOOBioLegPINio --prove

BLE

tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespLeg -DRespLegJW -DLegJWLegJW --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespLeg -DRespLegPE -DRespLegPEi -DLegJWLegPEi --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespLeg -DRespLegPE -DRespLegPEo -DLegJWLegPEo --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespLeg -DRespLegPE -DRespLegPEio -DLegJWLegPEio --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespLeg -DRespLegOOB -DLegJWLegOOB --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespLeg -DRespLegJW -DLegPEiLegJW -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespLeg -DRespLegPE -DRespLegPEi -DLegPEiLegPEi -DInputInput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespLeg -DRespLegPE -DRespLegPEo -DLegPEiLegPEo -DInputOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespLeg -DRespLegPE -DRespLegPEio -DLegPEiLegPEio -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespLeg -DRespLegOOB -DLegPEiLegOOB -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespLeg -DRespLegJW -DLegPEoLegJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespLeg -DRespLegPE -DRespLegPEi -DLegPEoLegPEi -DOutputInput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespLeg -DRespLegPE -DRespLegPEo -DLegPEoLegPEo -DOutputOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespLeg -DRespLegPE -DRespLegPEio -DLegPEoLegPEio -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespLeg -DRespLegOOB -DLegPEoLegOOB -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespLeg -DRespLegJW -DLegPEioLegJW -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespLeg -DRespLegPE -DRespLegPEi -DLegPEioLegPEi -DInoutInput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespLeg -DRespLegPE -DRespLegPEo -DLegPEioLegPEo -DInoutOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespLeg -DRespLegPE -DRespLegPEio -DLegPEioLegPEio -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespLeg -DRespLegOOB -DLegPEioLegOOB -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespLeg -DRespLegJW -DLegOOBLegJW --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespLeg -DRespLegPE -DRespLegPEi -DLegOOBLegPEi --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespLeg -DRespLegPE -DRespLegPEo -DLegOOBLegPEo --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespLeg -DRespLegPE -DRespLegPEio -DLegOOBLegPEio --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespLeg -DRespLegOOB -DLegOOBLegOOB --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecJW -DSecJWSecJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecPE -DRespSecPEi -DSecJWSecPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecPE -DRespSecPEo -DSecJWSecPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecPE -DRespSecPEio -DSecJWSecPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecNC -DSecJWSecNC --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecOOB -DRespSecOOBi -DSecJWSecOOBi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecOOB -DRespSecOOBo -DSecJWSecOOBo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespSec -DRespSecOOB -DRespSecOOBio -DSecJWSecOOBio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecJW -DSecPEiSecJW -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecPE -DRespSecPEi -DSecPEiSecPEi -DInputInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecPE -DRespSecPEo -DSecPEiSecPEo -DInputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecPE -DRespSecPEio -DSecPEiSecPEio -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecNC -DSecPEiSecNC -DInputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecOOB -DRespSecOOBi -DSecPEiSecOOBi -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecOOB -DRespSecOOBo -DSecPEiSecOOBo -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespSec -DRespSecOOB -DRespSecOOBio -DSecPEiSecOOBio -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecJW -DSecPEoSecJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecPE -DRespSecPEi -DSecPEoSecPEi -DOutputInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecPE -DRespSecPEo -DSecPEoSecPEo -DOutputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecPE -DRespSecPEio -DSecPEoSecPEio -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecNC -DSecPEoSecNC -DOutputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecOOB -DRespSecOOBi -DSecPEoSecOOBi -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecOOB -DRespSecOOBo -DSecPEoSecOOBo -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespSec -DRespSecOOB -DRespSecOOBio -DSecPEoSecOOBio -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecJW -DSecPEioSecJW -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecPE -DRespSecPEi -DSecPEioSecPEi -DInoutInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecPE -DRespSecPEo -DSecPEioSecPEo -DInoutOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecPE -DRespSecPEio -DSecPEioSecPEio -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecNC -DSecPEioSecNC -DInoutOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecOOB -DRespSecOOBi -DSecPEioSecOOBi -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecOOB -DRespSecOOBo -DSecPEioSecOOBo -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespSec -DRespSecOOB -DRespSecOOBio -DSecPEioSecOOBio -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecJW -DSecNCSecJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecPE -DRespSecPEi -DSecNCSecPEi -DOutputInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecPE -DRespSecPEo -DSecNCSecPEo -DOutputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecPE -DRespSecPEio -DSecNCSecPEio -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecNC -DSecNCSecNC -DOutputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecOOB -DRespSecOOBi -DSecNCSecOOBi -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecOOB -DRespSecOOBo -DSecNCSecOOBo -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespSec -DRespSecOOB -DRespSecOOBio -DSecNCSecOOBio -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecJW -DSecOOBiSecJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecPE -DRespSecPEi -DSecOOBiSecPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecPE -DRespSecPEo -DSecOOBiSecPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecPE -DRespSecPEio -DSecOOBiSecPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecNC -DSecOOBiSecNC --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecOOB -DRespSecOOBi -DSecOOBiSecOOBi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecOOB -DRespSecOOBo -DSecOOBiSecOOBo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespSec -DRespSecOOB -DRespSecOOBio -DSecOOBiSecOOBio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecJW -DSecOOBoSecJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecPE -DRespSecPEi -DSecOOBoSecPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecPE -DRespSecPEo -DSecOOBoSecPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecPE -DRespSecPEio -DSecOOBoSecPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecNC -DSecOOBoSecNC --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecOOB -DRespSecOOBi -DSecOOBoSecOOBi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecOOB -DRespSecOOBo -DSecOOBoSecOOBo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespSec -DRespSecOOB -DRespSecOOBio -DSecOOBoSecOOBio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecJW -DSecOOBioSecJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecPE -DRespSecPEi -DSecOOBioSecPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecPE -DRespSecPEo -DSecOOBioSecPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecPE -DRespSecPEio -DSecOOBioSecPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecNC -DSecOOBioSecNC --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecOOB -DRespSecOOBi -DSecOOBioSecOOBi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecOOB -DRespSecOOBo -DSecOOBioSecOOBo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespSec -DRespSecOOB -DRespSecOOBio -DSecOOBioSecOOBio --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecJW -DLegJWSecJW --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecPE -DRespSecPEi -DLegJWSecPEi --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecPE -DRespSecPEo -DLegJWSecPEo --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecPE -DRespSecPEio -DLegJWSecPEio --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecNC -DLegJWSecNC --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecOOB -DRespSecOOBi -DLegJWSecOOBi --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecOOB -DRespSecOOBo -DLegJWSecOOBo --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegJW -DRespSec -DRespSecOOB -DRespSecOOBio -DLegJWSecOOBio --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecJW -DLegPEiSecJW -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecPE -DRespSecPEi -DLegPEiSecPEi -DInputInput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecPE -DRespSecPEo -DLegPEiSecPEo -DInputOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecPE -DRespSecPEio -DLegPEiSecPEio -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecNC -DLegPEiSecNC -DInputOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecOOB -DRespSecOOBi -DLegPEiSecOOBi -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecOOB -DRespSecOOBo -DLegPEiSecOOBo -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEi -DRespSec -DRespSecOOB -DRespSecOOBio -DLegPEiSecOOBio -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecJW -DLegPEoSecJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecPE -DRespSecPEi -DLegPEoSecPEi -DOutputInput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecPE -DRespSecPEo -DLegPEoSecPEo -DOutputOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecPE -DRespSecPEio -DLegPEoSecPEio -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecNC -DLegPEoSecNC -DOutputOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecOOB -DRespSecOOBi -DLegPEoSecOOBi -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecOOB -DRespSecOOBo -DLegPEoSecOOBo -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEo -DRespSec -DRespSecOOB -DRespSecOOBio -DLegPEoSecOOBio -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecJW -DLegPEioSecJW -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecPE -DRespSecPEi -DLegPEioSecPEi -DInoutInput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecPE -DRespSecPEo -DLegPEioSecPEo -DInoutOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecPE -DRespSecPEio -DLegPEioSecPEio -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecNC -DLegPEioSecNC -DInoutOutput --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecOOB -DRespSecOOBi -DLegPEioSecOOBi -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecOOB -DRespSecOOBo -DLegPEioSecOOBo -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegPE -DInitLegPEio -DRespSec -DRespSecOOB -DRespSecOOBio -DLegPEioSecOOBio -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecJW -DLegOOBSecJW --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecPE -DRespSecPEi -DLegOOBSecPEi --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecPE -DRespSecPEo -DLegOOBSecPEo --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecPE -DRespSecPEio -DLegOOBSecPEio --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecNC -DLegOOBSecNC --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecOOB -DRespSecOOBi -DLegOOBSecOOBi --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecOOB -DRespSecOOBo -DLegOOBSecOOBo --prove
tamarin-prover ble.spthy -DInitLeg -DInitLegOOB -DRespSec -DRespSecOOB -DRespSecOOBio -DLegOOBSecOOBio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegJW -DSecJWLegJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegPE -DRespLegPEi -DSecJWLegPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegPE -DRespLegPEo -DSecJWLegPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegPE -DRespLegPEio -DSecJWLegPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecJW -DRespLeg -DRespLegOOB -DSecJWLegOOB --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegJW -DSecPEiLegJW -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegPE -DRespLegPEi -DSecPEiLegPEi -DInputInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegPE -DRespLegPEo -DSecPEiLegPEo -DInputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegPE -DRespLegPEio -DSecPEiLegPEio -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEi -DRespLeg -DRespLegOOB -DSecPEiLegOOB -DInputInput -DInputOutput -DInputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegJW -DSecPEoLegJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegPE -DRespLegPEi -DSecPEoLegPEi -DOutputInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegPE -DRespLegPEo -DSecPEoLegPEo -DOutputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegPE -DRespLegPEio -DSecPEoLegPEio -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEo -DRespLeg -DRespLegOOB -DSecPEoLegOOB -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegJW -DSecPEioLegJW -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegPE -DRespLegPEi -DSecPEioLegPEi -DInoutInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegPE -DRespLegPEo -DSecPEioLegPEo -DInoutOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegPE -DRespLegPEio -DSecPEioLegPEio -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecPE -DInitSecPEio -DRespLeg -DRespLegOOB -DSecPEioLegOOB -DInoutInput -DInoutOutput -DInoutInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegJW -DSecNCLegJW -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegPE -DRespLegPEi -DSecNCLegPEi -DOutputInput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegPE -DRespLegPEo -DSecNCLegPEo -DOutputOutput --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegPE -DRespLegPEio -DSecNCLegPEio -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecNC -DRespLeg -DRespLegOOB -DSecNCLegOOB -DOutputInput -DOutputOutput -DOutputInout --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegJW -DSecOOBiLegJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegPE -DRespLegPEi -DSecOOBiLegPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegPE -DRespLegPEo -DSecOOBiLegPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegPE -DRespLegPEio -DSecOOBiLegPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBi -DRespLeg -DRespLegOOB -DSecOOBiLegOOB --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegJW -DSecOOBoLegJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegPE -DRespLegPEi -DSecOOBoLegPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegPE -DRespLegPEo -DSecOOBoLegPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegPE -DRespLegPEio -DSecOOBoLegPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBo -DRespLeg -DRespLegOOB -DSecOOBoLegOOB --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegJW -DSecOOBioLegJW --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegPE -DRespLegPEi -DSecOOBioLegPEi --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegPE -DRespLegPEo -DSecOOBioLegPEo --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegPE -DRespLegPEio -DSecOOBioLegPEio --prove
tamarin-prover ble.spthy -DInitSec -DInitSecOOB -DInitSecOOBio -DRespLeg -DRespLegOOB -DSecOOBioLegOOB --prove

Mesh

tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBnoEiOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBnoEiOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBnoEiOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBnoEiOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBiEiOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBiEiOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBiEiOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBiEiOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBoEiOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBoEiOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBoEiOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBoEiOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBsEiOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBsEiOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBsEiOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBsEiOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBnoEoOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBnoEoOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBnoEoOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBno -DProvOOBno -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBnoEoOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBiEoOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBiEoOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBiEoOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBi -DProvOOBi -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBiEoOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBoEoOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBoEoOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBoEoOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBo -DProvOOBo -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBoEoOOBs --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEiOOBsEoOOBno --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEiOOBsEoOOBi --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEiOOBsEoOOBo --prove
tamarin-prover mesh.spthy -DProvEi -DProvEiOOBs -DProvOOBs -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEiOOBsEoOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBnoEiOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBnoEiOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBnoEiOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBnoEiOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBiEiOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBiEiOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBiEiOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBiEiOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBoEiOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBoEiOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBoEiOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBoEiOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEi -DDevEiOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBsEiOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEi -DDevEiOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBsEiOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEi -DDevEiOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBsEiOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEi -DDevEiOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBsEiOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBnoEoOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBnoEoOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBnoEoOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBno -DProvOOBno -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBnoEoOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBiEoOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBiEoOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBiEoOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBi -DProvOOBi -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBiEoOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBoEoOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBoEoOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBoEoOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBo -DProvOOBo -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBoEoOOBs --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEo -DDevEoOOBno -DDevOOBno -DProvECDH -DDevECDH -DEoOOBsEoOOBno --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEo -DDevEoOOBi -DDevOOBi -DProvECDH -DDevECDH -DEoOOBsEoOOBi --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEo -DDevEoOOBo -DDevOOBo -DProvECDH -DDevECDH -DEoOOBsEoOOBo --prove
tamarin-prover mesh.spthy -DProvEo -DProvEoOOBs -DProvOOBs -DDevEo -DDevEoOOBs -DDevOOBs -DProvECDH -DDevECDH -DEoOOBsEoOOBs --prove