A Formal Verification of a Reputation Multi-Factor Authentication Mechanism for Constrained Devices and Low-Power...

Area of Science:

• Computer Science
• Cybersecurity
• Network Engineering

Background:

• Internet of Things (IoT) devices face significant security challenges, particularly in authenticating restricted devices within long-distance, low-throughput networks.
• Existing issues include device impersonation, privacy breaches, and high battery consumption, necessitating robust security solutions.
• Formal verification of security components and their non-locking properties remains an underexplored area.

Purpose of the Study:

• To analyze the design-time security of a multi-factor authentication mechanism for IoT devices.
• To evaluate security requirements beyond traditional encryption and data secrecy.
• To formally assess the mechanism's compliance with identified security threats.

Main Methods:

• Threat modeling was employed to identify and evaluate security vulnerabilities.
• A multi-factor authentication mechanism with a reputation system was designed and analyzed.
• Temporal logic was utilized for formal verification of security properties and deadlock detection.

Main Results:

• The formal verification confirmed that the proposed authentication mechanism is deadlock-free.
• The mechanism was demonstrated to meet the established security requirements for IoT authentication.
• Design-time security analysis provided detailed insights into the mechanism's properties.

Conclusions:

• The formal verification approach is effective for assessing the security of IoT authentication components.
• The analyzed multi-factor authentication mechanism offers a secure and deadlock-free solution for restricted IoT devices.
• This work contributes to a deeper understanding of formal verification for complex IoT security systems.