China
Africa
Explore chapters and articles related to this topic
Analytical Matrices and Tools
Published in Chintan Patel, Nishant Doshi, Internet of Things Security, 2018
A project led by Bruno Blanchet [Blanchet (2016)] developed abstract based cryptographic protocol verifier called ProVerif. ProVerif is an automatic protocol verifier that follows Dolev-Yao Model for the modeling of an attacker. ProVerif works in maximum cryptographic operations like key exchanges, MAC calculations, hash function calculations and cypher text generation and plain text verification. ProVerif supports two types of files: Horn clauses : Set of predicates combined by OR operation.Pi-Calculus
A blockchain-based lightweight authentication and key agreement scheme for internet of vehicles
Published in Connection Science, 2022
Jing Zheng, Xiaoliang Wang, Qing Yang, Wenhui Xiao, Yapeng Sun, Wei Liang
ProVerif is a formal automatic verification cryptographic protocol tool based on the Dolev–Yao model developed by Bruno Blanchet. It is implemented in Prolog language. It is able to describe a variety of cryptographic primifiers, including: shared key cryptography, public key cryptography (encryption and digital signature), Hash functions, the Deffie–Hellman key exchange protocol, specify rewrite rules and equations for the input language as applied PI calculus or Horn words. In order to verify the scheme proposed in this paper, we coded and tested the protocol with HLPSL. Figures 7 and 8 are the verification result of the Proverif. Proverif software verifies the experimental results of our scheme. It can be concluded that our scheme can guarantee the security of parameters such as vehicle password , , , and negotiated Key between vehicle and VS server, which cannot be captured by the opponent. All the authentication processes defined are also performed sequentially.
Blockchain-based Light-weight Authentication Approach for a Multiple Wireless Sensor Network
Published in IETE Journal of Research, 2022
In this part, we evaluate the important aspects of our measure using ProVerif, a widely known formal verification tool. ProVerif is a professional automatic analysis tool for verifying the safeguards of cryptographic protocols. It provides the majority of cryptographic primitives, including encryption, decryption, digital identity, and hash functions. Furthermore, equations are used to system important cryptographic difficulties such as the Diffie-Hellman problem, the Elliptic curve problem, and others. In ProVerif, the protocol is converted to Horn clauses, and inquiries are placed on such Horn clauses to test security features.