RESUMO
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.
RESUMO
Mimblewimble (MW) is a privacy-oriented cryptocurrency technology that provides security and scalability properties that distinguish it from other protocols of its kind. We present and discuss those properties and outline the basis of a model-driven verification approach to address the certification of the correctness of the protocol implementations. In particular, we propose an idealized model that is key in the described verification process, and identify and precisely state the conditions for our model to ensure the verification of the relevant security properties of MW. Since MW is built on top of a consensus protocol, we develop a Z specification of one such protocol and present an excerpt of the {log} prototype after its Z specification. This {log} prototype can be used as an executable model. This allows us to analyze the behavior of the protocol without having to implement it in a low level programming language. Finally, we analyze the Grin and Beam implementations of MW in their current state of development.