Bezerra Wesley R, Martina Jean E, Westphall Carlos B
Campus Universitário-Trindade, UFSC-Federal University of Santa Catarina, Florianópolis 88040-380, SC, Brazil.
Sensors (Basel). 2023 Aug 3;23(15):6933. doi: 10.3390/s23156933.
There are many security challenges in IoT, especially related to the authentication of restricted devices in long-distance and low-throughput networks. Problems such as impersonation, privacy issues, and excessive battery usage are some of the existing problems evaluated through the threat modeling of this work. A formal assessment of security solutions for their compliance in addressing such threats is desirable. Although several works address the verification of security protocols, verifying the security of components and their non-locking has been little explored. This work proposes to analyze the design-time security of the components of a multi-factor authentication mechanism with a reputation regarding security requirements that go beyond encryption or secrecy in data transmission. As a result, it was observed through temporal logic that the mechanism is deadlock-free and meets the requirements established in this work. Although it is not a work aimed at modeling the security mechanism, this document provides the necessary details for a better understanding of the mechanism and, consequently, the process of formal verification of its security properties.
物联网存在许多安全挑战，特别是与长距离和低吞吐量网络中受限设备的认证相关。诸如假冒、隐私问题和电池过度使用等问题是通过本工作的威胁建模评估的一些现有问题。对安全解决方案在应对此类威胁方面的合规性进行正式评估是很有必要的。尽管有几项工作涉及安全协议的验证，但对组件的安全性及其无锁定性的验证却很少有人探索。本工作建议分析一种多因素认证机制组件的设计时安全性，该机制具有超越数据传输中的加密或保密性的安全要求声誉。结果，通过时态逻辑观察到该机制无死锁且符合本工作中确立的要求。虽然这不是一项旨在对安全机制进行建模的工作，但本文档提供了必要的细节，以便更好地理解该机制，从而理解其安全属性的形式验证过程。
