This repository presents a formal model of BRSKI, DPP, and EAP-TLS in HLPSL and applied pi-calculus.
In this work, we use two automated symbolic protocol verification tools, ProVerif and Automated Validation of Internet Security Protocols and Applications (AVISPA) tool, to formally verify the security property of prominent IoT secure device onboarding protocols. These tools analyze the protocols to find the attacks from the point of view of a network adversary. Formal verification tools have already been used to analyze prominent protocols like TlS, SSH, IKE, OAuth, etc. Over time they are becoming an effective way of finding vulnerabilities of the protocol constructions.
Proverif was developed by Bruno Blanchet in 2001. Proverif is a cryptographic protocol verification tool that facilitates protocol analysis for an unbounded number of sessions by using over-approximation. ProVerif uses applied pi-calculus to formally model a protocol and automatically verifies the security properties of the formal model.
AVISPA was developed by Armando et al. in the year 2005. AVISPA is a push-button verification tool developed as a collaboration between the Artificial Intelligence Laboratory at DIST (University of Genova, Genova, Italy), the CASSIS group at INRIA Lorraine (LORIA, Nancy, France), the Information Security group at ETHZ (Zurich, Switzerland), and Siemens AG (Munich, Germany). AVISPA comprises four distinct formal verification approaches that can formally validate the security property of a protocol (i.e., On-the-fly Model-Checker, Constraint-Logic-based Attack Searcher, SAT-based Model-Checker, and Tree Automata-based Protocol Analyser). It uses the High-LevelProtocol Specification Language (HLPSL) to specify the protocol and its security properties in order to use all four analysis techniques.