update references to paper, add simulation results

README.md

@@ -47,13 +47,13 @@ The repository contains the following sub-artifacts:
 
 - `proofs`
    contains the Tamarin models used to formally verify our revocation scheme 
-   (Sec. VI / Appendix B)
+   (Sect. VI / Appendix A)
 - `simulation`
    Containing the code used for our evaluation 
-   (Sec. VII-A / Appendix C)
+   (Sect. VII-A)
 - `prl`
    contains scripts to generate and plot the markov matrices 
-   (Sec. VII-B / Appendix D)
+   (Sect. VII-B / Appendix B)
 
 A README is also included on each individual folder containing instructions to
 run the artifacts.
@@ -223,8 +223,8 @@ cd ..
 
 | Artifact     | Paper references    | Description                            |
 |--------------|---------------------|----------------------------------------|
-| `centralized-time` Tamarin model | Sect. VI, Appendix B, Table I | Model and proofs that verify the properties defined in Sect. V-A, for the main design of Sect. V |
-| `distributed-time` Tamarin model | Appendix B, Table II | Variant of the model that assumes a trusted time source in TCs, as discussed in Sect. V-B, and proofs |
+| `centralized-time` Tamarin model | Sect. VI, Appendix A, Table I | Model and proofs that verify the properties defined in Sect. V-A, for the main design of Sect. V |
+| `distributed-time` Tamarin model | Appendix A, Table II | Variant of the model that assumes a trusted time source in TCs, as discussed in Sect. V-B, and proofs |
 
 The steps for reproducing our results are the same as done in kick-the-tires
 stage, but this time we will ask Tamarin to verify _all_ lemmas.
@@ -262,10 +262,14 @@ cd ..
 
 | Artifact        | Paper references        | Description                            |
 |-----------------|-------------------------|----------------------------------------|
-| `scenario-a1`   | Sect. VII-A, Fig. 5,11  | Box plots showing distributions of revocation times under different attacker classes, for T_v = 30 seconds and no trusted time in TCs |
-| `scenario-a2`   | Appendix C, Fig. 12     | Box plots showing distributions of revocation times under different attacker classes, for T_v = 150 seconds and no trusted time in TCs |
-| `scenario-b1`   | Appendix C, Fig. 13     | Box plots showing distributions of revocation times under different attacker classes, for T_v = 30 seconds and assuming a trusted time in TCs |
-| `scenario-b2`   | Appendix C, Fig. 14     | Box plots showing distributions of revocation times under different attacker classes, for T_v = 150 seconds and assuming a trusted time in TCs |
+| `scenario-a1`   | Sect. VII-A, Fig. 5     | Box plots showing distributions of revocation times under different attacker classes, for T_v = 30 seconds and no trusted time in TCs |
+| `scenario-a2`   | Not in the paper        | Box plots showing distributions of revocation times under different attacker classes, for T_v = 150 seconds and no trusted time in TCs |
+| `scenario-b1`   | Not in the paper        | Box plots showing distributions of revocation times under different attacker classes, for T_v = 30 seconds and assuming a trusted time in TCs |
+| `scenario-b2`   | Not in the paper        | Box plots showing distributions of revocation times under different attacker classes, for T_v = 150 seconds and assuming a trusted time in TCs |
+
+Scenarios A2, B1 and B2 and corresponding plots have been removed from the paper
+due to page limits. However, we discuss them in the simulations'
+[README](./simulation/README.md#extended-discussion-of-our-results).
 
 In order to run the simulations locally and within a few hours, we provide a
 scaled-down configuration that spawns 50 vehicles and runs all simulations in
@@ -331,12 +335,12 @@ cd ..
 
 | Artifact              | Paper references    | Description                            |
 |-----------------------|---------------------|----------------------------------------|
-| `probabilities`       | Sect. VII-B, Appendix D | Probabilities used for each scenario, and expected number of revocations |
+| `probabilities`       | Sect. VII-B, Appendix B | Probabilities used for each scenario, and expected number of revocations |
 | `p-plot`              | Sect. VII-B, Fig. 6 | Plots percentiles for maximum PRL sizes under different scenarios and shares of attackers, with fixed `T_prl` and number of pseudonyms |
 | `tv-distribution`     | Sect. VII-B, Fig. 7 | Evaluates `T_eff`, heartbeat frequency, heartbeat size, and required bandwidth under different values for `T_v` |
-| `tikz-graph`          | Appendix D, Fig. 15 | Simple transition graph |
-| `n-plot`              | Appendix D, Fig. 16 | Plots 99th percentile for maximum PRL sizes under different number of pseudonyms, in four different scenarios |
-| `t-plot`              | Appendix D, Fig. 17 | Plots 99th percentile for maximum PRL sizes under different values for `T_prl`, in four different scenarios |
+| `tikz-graph`          | Appendix B, Fig. 9  | Simple transition graph |
+| `n-plot`              | Appendix B, Fig. 10 | Plots 99th percentile for maximum PRL sizes under different number of pseudonyms, in four different scenarios |
+| `t-plot`              | Appendix B, Fig. 11 | Plots 99th percentile for maximum PRL sizes under different values for `T_prl`, in four different scenarios |
 
 In total, this evaluation should take between **2.5 and 3.5 compute-hours**,
 depending on your hardware.

prl/Makefile

@@ -25,7 +25,7 @@ single: init_dirs
 	$(DOCKER_CMD) python3 main.py -n 800 -p 0.000000116323325 -e 30 --cache-dir=$(CACHE_DIR) --allow-cached
 
 tikz: init_dirs
-	@echo "Generating transition graph (Fig. 15)."
+	@echo "Generating transition graph (Fig. 9)."
 	$(DOCKER_CMD) python3 main.py -n 3 -p 0.1 -e 2 -f $(PLOT_DIR)/tikz-graph.tex
 
 p-plot: init_dirs

prl/README.md

@@ -110,7 +110,7 @@ make all
 
 ### Simple tikz plot
 
-The appendix lists a simple transition graph (Fig. 15). The LaTeX Tikz code for
+The appendix lists a simple transition graph (Fig. 9). The LaTeX Tikz code for
 this can be generated with:
 
 ```bash
@@ -169,15 +169,15 @@ revocations for each scenario, as discussed in Section VII-B. The script should
 give as output the following probabilities:
 
 ```text
-Scenario 1: vehicles get revoked at least once a day with 1% probability
+Scenario 1: pseudonyms get revoked at least once a day with 1% probability
 0.000000116323325
 0.000007813830433
 0.000015511337541
 0.000038603858866
 0.000077091394407
 0.000154066465489
 
-Scenario 2: vehicles get revoked at least once a day with 99% probability
+Scenario 2: pseudonyms get revoked at least once a day with 99% probability
 0.000053299160406
 0.000060464839143
 0.000067630517880
@@ -228,10 +228,10 @@ For the appendix plots we used the [n-plot.sh](./scripts/n-plot.sh) and
 [t-plot.sh](./scripts/t-plot.sh) scripts.
 
 ```bash
-# n (number of vehicles) plot (Fig. 17)
+# n (number of pseudonyms) plot (Fig. 11)
 ./scripts/n-plot.sh
 
-# T_PRL plot (Fig. 16)
+# T_PRL plot (Fig. 10)
 ./scripts/t-plot.sh
 ```
 

prl/main.py

@@ -66,7 +66,7 @@ def main(
             help="Probability of a certificate being revoked.",
         ),
         tikz_file: Path = typer.Option(
-            None, "-f", help="Give a path to write the transition graph to a tikz file (Fig. 15 in paper).",
+            None, "-f", help="Give a path to write the transition graph to a tikz file (Fig. 9 in paper).",
                 exists=False, dir_okay=False, readable=True,
         ),
         plot: bool = typer.Option(

prl/probabilities.py

@@ -36,7 +36,7 @@ def print_scenario(scenario, attackers):
 print("Computing per-second revocation probabilities for each vehicle class and share of attackers..")
 probabilities = {}
 for vc in vehicle_classes:
-    # computing the per-second probability via geometric series (See Appendix D-D)
+    # computing the per-second probability via geometric series (See Appendix B-D)
     p =  1 - (1 - vehicle_classes[vc]["p"]) ** (1 / vehicle_classes[vc]["duration"])
 
     probabilities[vc] = {
@@ -55,15 +55,15 @@ def print_scenario(scenario, attackers):
 print("Computing total (honest + malicious) probabilities for each scenario..")
 
 # h1 <-> Scenario 1: 
-# honest vehicles get revoked at least once a day with 1% probability
-# malicious vehicles get revoked every 30 minutes with 75% probabiity
+# honest pseudonyms get revoked at least once a day with 1% probability
+# malicious pseudonyms get revoked every 30 minutes with 75% probabiity
 h1 = np.add(probabilities["honest_1"]["attackers"], probabilities["malicious"]["attackers"])
 print(f"Probabilities Scenario 1")
 print_scenario(h1, attackers)
 
 # h2 <-> Scenario 2: 
-# honest vehicles get revoked at least once a day with 99% probability
-# malicious vehicles get revoked every 30 minutes with 75% probabiity
+# honest pseudonyms get revoked at least once a day with 99% probability
+# malicious pseudonyms get revoked every 30 minutes with 75% probabiity
 h2 = np.add(probabilities["honest_2"]["attackers"], probabilities["malicious"]["attackers"])
 print(f"Probabilities Scenario 2")
 print_scenario(h2, attackers)

prl/scripts/n-plot.sh

@@ -2,7 +2,7 @@
 
 set -e
 
-echo "Generating n (number of vehicles) plot (Fig. 17)."
+echo "Generating n (number of pseudonyms) plot (Fig. 11)."
 for value in `seq 400 100 1000`
 do
 python3 generate_plots.py -e 30 -n $value -p 0.000000116323325 -p 0.000053299160406 -p 0.000154066465489 -p 0.000196612735153 "$@"

prl/scripts/t-plot.sh

@@ -2,7 +2,7 @@
 
 set -e
 
-echo "Generating T_PRL plot (Fig. 16)."
+echo "Generating T_PRL plot (Fig. 10)."
 for value in `seq 10 10 200`
 do
 python3 generate_plots.py -e $value -n 800 -p 0.000000116323325 -p 0.000053299160406 -p 0.000154066465489 -p 0.000196612735153 "$@"

proofs/README.md

@@ -1,7 +1,7 @@
 # Tamarin models
 
 This folder contains instructions to run our formal verification artifacts with
-Tamarin Prover, to reproduce the results of Section VI and Appendix B of our
+Tamarin Prover, to reproduce the results of Section VI and Appendix A of our
 paper.
 
 ## Overview
@@ -28,7 +28,7 @@ some proofs. See the [Tamarin
 guide](https://tamarin-prover.github.io/manual/master/book/011_advanced-features.html)
 for more information.
 
-More details can be found in the paper (Sect. 5.1 and Appendix B).
+More details can be found in the paper (Sect. VI and Appendix A).
 
 ## Prerequisites
 
@@ -66,7 +66,7 @@ used by the targets is `v1.6.1`. Each of the models should verify within 5
 minutes.
 
 ```bash
-# run container to verify the main design (discussed in Sections V, VI and Appendix B)
+# run container to verify the main design (discussed in Sections V, VI and Appendix A)
 make prove MODEL=centralized-time
 
 # *grab a coffee* -- make sure you do not close the current shell!
@@ -81,7 +81,7 @@ docker rm tamarin
 After the container terminates, the complete proof generated by Tamarin can be
 found under `out/output.spthy`.
 
-To verify the alternative design discussed in Section V-B and Appendix B, simply
+To verify the alternative design discussed in Section V-B and Appendix A, simply
 replace `MODEL=centralized-time` with `MODEL=distributed-time` in the `make
 prove` above. Make sure that the previous container has completed before running
 the new one.
@@ -161,10 +161,10 @@ For best results, we recommend using 4 threads. Each of the models should
 complete within 5-10 minutes.
 
 ```bash
-# Verify the main design (discussed in Sections V, VI and Appendix B)
+# Verify the main design (discussed in Sections V, VI and Appendix A)
 tamarin-prover --prove --output=output_centralized.spthy centralized-time/theory.spthy +RTS -N4 -RTS
 
-# Verify the alternative design (discussed in Section V-B and Appendix B)
+# Verify the alternative design (discussed in Section V-B and Appendix A)
 tamarin-prover --prove --output=output_distributed.spthy distributed-time/theory.spthy +RTS -N4 -RTS
 ```
 

simulation/README.md

@@ -1,8 +1,7 @@
 # Simulation of a V2X scenario with self-revocation
 
 This folder contains instructions to run our simulation artifacts with
-Kubernets, to reproduce the results of Section VII and Appendix C of our
-paper.
+Kubernets, to reproduce the results of Section VII of our paper.
 
 ## Short description of the application
 
@@ -282,20 +281,23 @@ simulation ran for ~2 hours and spawned 360 "honest" vehicles and 40 "malicious"
 vehicles, and each used a different set of parameters for `T_V`, and
 `TRUSTED_TIME` (see [below](#parameters) for more info on these parameters).
 
-The table below, analogously to Table III in Appendix C, summarizes the setup of
-each scenario of the simulation:
+The table below summarizes the setup of each scenario of the simulation:
 
 | Scenario     | Link to paper       | Parameters                   |
 |--------------|---------------------|------------------------------|
 | Scenario A1  | Fig. 5, Sect. VII-A | `T_V=30`, `TRUSTED_TIME=0`   |
-| Scenario A2  | Fig. 12, Appendix C | `T_V=150`, `TRUSTED_TIME=0`  |
-| Scenario A1  | Fig. 13, Appendix C | `T_V=30`, `TRUSTED_TIME=1`   |
-| Scenario A1  | Fig. 14, Appendix C | `T_V=150`, `TRUSTED_TIME=1`  |
+| Scenario A2  | Not in the paper    | `T_V=150`, `TRUSTED_TIME=0`  |
+| Scenario B1  | Not in the paper    | `T_V=30`, `TRUSTED_TIME=1`   |
+| Scenario B2  | Not in the paper    | `T_V=150`, `TRUSTED_TIME=1`  |
 
 Additionally, each scenario ran four different simulations, each using a
 different attacker level. See Sect VII-A of our paper for more information on
 attacker levels.
 
+Scenarios A2, B1 and B2 and corresponding plots have been removed from the paper
+due to page limits. See [below](#extended-discussion-of-our-results) for a
+description of these results.
+
 ### Configure simulations
 
 We provide scripts to completely automate the simulations. The desired setup can
@@ -429,6 +431,58 @@ the command below.
 make plot_all SIM_DIR=reference-outputs/
 ```
 
+## Extended discussion of our results
+
+This section extends Sect. VII-A of the paper with results from additional
+scenarios.
+
+### Plots
+
+**Scenario A1**
+
+![](reference-outputs/figs/scenario-a1_verify.svg)
+
+**Scenario A2**
+
+![](reference-outputs/figs/scenario-a2_verify.svg)
+
+**Scenario B1**
+
+![](reference-outputs/figs/scenario-b1_verify.svg)
+
+**Scenario B2**
+
+![](reference-outputs/figs/scenario-b2_verify.svg)
+
+
+### Discussion
+
+Recall from Sect. VII-A of the paper that each value of the boxes represents the
+time between the revocation of a pseudonym `ps` (`REVOKE` event) and the last
+V2V message signed with `ps` that was verified by a non-malicious TC
+(`VERIFY` event). The latter time represents the *effective revocation
+time* for that particular pseudonym `ps`. The box plots give the distribution of
+such values, obtained aggregating more than 600 revocations, filtering out
+negative values.
+
+The figures show one significant difference between the main design (A1 and A2)
+and the extension with a local trusted time source (B1 and B2): While in the
+former most revocations are effective around or before `T_v`, in the latter
+attackers are able to postpone revocation up until `T_eff` in some cases,
+i.e., it appears easier to reach the upper bound, especially for powerful
+attackers such as the `smart` one. This is due to the fact that, while
+in the main design revoked TCs cannot synchronize their time since
+`t_rev`, with a local time source TCs can still advance their internal
+time up until `t_rev + T_v`, before triggering the automatic
+revocation logic. That is, in the latter case a revoked TC is able to
+generate ''more fresh'' V2V messages, which can be processed by other
+TCs later in time.
+
+This peculiarity suggests that a local trusted time source negatively affects
+the revocation time. While this may be true in the average case, it still does
+not affect the worst-case effective revocation time `T_eff`, as shown in the
+figures.
+
 ## Parameters
 
 Note: booleans must be represented with either `0` (false) or `1` (true)