ProVerif codes for "Ultra-Lightweight and Secure Blockchain-Assisted Charging Scheduling Scheme For Vehicular Edge Networks By Utilization of NanoPi NEO" (10.1109/TVT.2022.3173076)

Citation Author(s):
Ali
Shahidinejad
School of Information Technology, Deakin University, Geelong, VIC 3220, Australia
Submitted by:
Ali Shahidinejad
Last updated:
Mon, 05/09/2022 - 20:49
DOI:
10.21227/1t59-de68
Data Format:
.pv
Links:
Ultra-Lightweight and Secure Blockchain-Assisted Charging Scheduling Scheme For Vehicular Edge Networks By Utilization of NanoPi
License:
Creative Commons Attribution
141 Views
Categories:
Security
Keywords:
authentication, proverif, Scheduling
0
0 ratings - Please login to submit your rating.
ACCESS DATASET CITE SHARE/EMBED

Abstract 

“ProVerif” is a powerful utility designed to examine “reachability properties,” “correspondence assertions,” and “observational equivalences.” Our protocol modelling addresses both the elemental security requirements, like “impersonation” or “replay” attack, and the most advanced ones, like “perfect forward secrecy” or “password guessing attack.”

Because we had a limited space in our published paper, the program source codes are provided here. The codes can be tested online at "http://proverif16.paris.inria.fr/".

Instructions: 

We have presented automatic software formal verification by one of the best existing tools called ProVerif. We have simulated our protocol under miscellaneous attack scenarios, something which is done rarely in the literature. The source codes of our implementation are presented as follows and can be tested online at ProVerif website.

Common.pv is for checking common attacks.

PFS.pv is for checking the perfect forward secrecy feature.

KSSTIA.pv is for checking the ephemeral secret leakage attack.

Dataset Files

LOGIN TO ACCESS DATASET FILES

 

QUESTIONS?