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:
- DOI:
- 10.21227/1t59-de68
- Data Format:
- Links:
150 views
- Categories:
- Keywords:
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.
