From 96cf08e5a0f322ca0e7eed7abe1fe8b7623bba0a Mon Sep 17 00:00:00 2001 From: Gianluca Scopelliti Date: Thu, 23 Nov 2023 15:17:12 +0100 Subject: [PATCH] update references to paper, add simulation results --- README.md | 30 ++++++++++--------- prl/Makefile | 2 +- prl/README.md | 10 +++---- prl/main.py | 2 +- prl/probabilities.py | 10 +++---- prl/scripts/n-plot.sh | 2 +- prl/scripts/t-plot.sh | 2 +- proofs/README.md | 12 ++++---- simulation/README.md | 68 ++++++++++++++++++++++++++++++++++++++----- 9 files changed, 98 insertions(+), 40 deletions(-) diff --git a/README.md b/README.md index a10a32d..1ba0b0e 100644 --- a/README.md +++ b/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. diff --git a/prl/Makefile b/prl/Makefile index 3245ef3..24a2d33 100644 --- a/prl/Makefile +++ b/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 diff --git a/prl/README.md b/prl/README.md index a4211af..f93f35d 100644 --- a/prl/README.md +++ b/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,7 +169,7 @@ 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 @@ -177,7 +177,7 @@ Scenario 1: vehicles get revoked at least once a day with 1% probability 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 ``` diff --git a/prl/main.py b/prl/main.py index 6c4b86d..531d4e2 100644 --- a/prl/main.py +++ b/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( diff --git a/prl/probabilities.py b/prl/probabilities.py index 96e4560..acb1d8b 100644 --- a/prl/probabilities.py +++ b/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) diff --git a/prl/scripts/n-plot.sh b/prl/scripts/n-plot.sh index 6e477da..79dc1a3 100755 --- a/prl/scripts/n-plot.sh +++ b/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 "$@" diff --git a/prl/scripts/t-plot.sh b/prl/scripts/t-plot.sh index ebc7259..a9cf7c3 100755 --- a/prl/scripts/t-plot.sh +++ b/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 "$@" diff --git a/proofs/README.md b/proofs/README.md index a208038..9a52ab1 100644 --- a/proofs/README.md +++ b/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 ``` diff --git a/simulation/README.md b/simulation/README.md index 8eafa6a..fd40b36 100644 --- a/simulation/README.md +++ b/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)