This is the repository for our S&P'22 paper (Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities).

The model folder contains the modular-design models implemented in ProVerif.

• model/ssp.pv contains the model of Secure Simple Pairing (SSP).

• model/provision.pv contains the model of Bluetooth Mesh provisioning protocol.

• model/dataTransmission.pv contains the model of the data transmission phase in BC/BLE/Mesh.

• model/sspDatatrans.pv contains the model of SSP and data transmission in BC/BLE as a whole.

• model/provisionDatatrans.pv contains the model of Mesh provisioning and data transmission as a whole.

• model/provision-def1.pv contains the model of Bluetooth Mesh provisioning protocol with the first defense proposed in the paper.

• model/provision-def2.pv contains the model of Bluetooth Mesh provisioning protocol with the second defense proposed in the paper.

The *.sh scripts under the root folder utilize the modules in the model and splice different modules to compose a complete protocol.

• verifySSP.sh verifies the SSP protocol under different modes and generates the results shown in Table II in the paper.

• verifyProvision.sh verifies the Mesh provisioning protocol under different authentication modes and generates the results shown in Table III in the paper. When the strong secrecy property can be violated ProVerif outputs "cannot be proved" instead of "false" (page 60 in the manual).

• verifyDatatrans.sh verifies different cases in the data transmission phase of BC/BLE/Mesh and generates the results shown in Table IV in the paper.

• verifySSPDatatrans.sh verifies the SSP together with the BC/BLE data transmission at once and generates the results shown in Table V in the paper.

• verifyProvisionDatatrans.sh verifies Mesh provisioning together with Mesh data transmission at once and generates the results shown in Table VI in the paper.

• verifyProvisionDef1.sh verifies the Mesh provisioning protocol with the first defense proposed in the paper.

• verifyProvisionDef2.sh verifies the Mesh provisioning protocol with the second defense proposed in the paper.

The attack_traces folder contains all the attack traces generated by ProVerif when detecting the violations.

The trace_explanation folder contains the explanatory documents of the attack traces under the attack_traces folder.

For each attack trace, we provide an explanatory document whose name is the same as the PDF attack trace file. For example, the explanatory document for attack trace tableIII_row5_columnC1_attack-provision-5--NoOOBpkOutputOOBAuth--C1.pdf is tableIII_row5_columnC1_attack-provision-5--NoOOBpkOutputOOBAuth--C1.md.

Please run the model using ProVerif v2.02 -- the version we have tested our model with. We did not test the model with other versions of ProfVerif

Simply execute each script (*.sh) to verify the corresponding protocol.

Or run the script run_all.sh to verify all protocols.

The runtime displayed during execution of the script is the total runtime when verifying several properties together. To display runtime for verifying a specific property, comment out the other properties in the model and only keep the property of interest.

For each entry in Table II, III, IV, V, VI, the script generates a folder whose name starts with results- for the result of the verification. Besides, for each table, the script generates a folder whose name starts with "tableX-attacks-" containing the PDF attack traces that ProVerif found when detecting corresponding property violations in this table.