Formal unlinkability analysis of message authentication protocols based on authentic channels.

In today's technological world, low-cost devices have become a mainstream technology in the Internet-of-Thing (IoT) systems. Short-distance communication methods, such as Bluetooth and ZigBee, are prevalent among IoT users and devices. The lack of a confidential channel, even in the initialization phase of communication between devices, causes growing security and privacy concerns. As a result, many authentic-channel-based protocols, which only use a one-time authenticated but not a confidential channel, have been designed to tackle this problem. Message authentication, recognition, classification, linking, and association protocols are the major categories of the authentic-channel-based ones. This paper formally defines different types of authentic-channel-based protocols and discusses their respective authenticity and privacy assurances. We propose a new formal model to consider the notion of unlinkability and classify the protocols designed based on one-time and authentic channels that only resist active adversaries. We prove the unlinkability level of the abstract constructions and some seminal instances. Finally, we propose two new and improved versions of a recently published linking message protocol. [ABSTRACT FROM AUTHOR]