A Formal Model for Delegated Authorization of IoT Devices Using ACE-OAuth

As our daily lives become ever more connected, the need for security becomes more important. This need is, however, in conflict with the way most Internet of Things (IoT) devices are designed. These devices often have limited computing power, memory, and security mechanisms to defend against a range of attacks. The protocol designer must therefore take all these constraints into consideration when making IoT security design decisions. To bring authentication and authorization solutions to constrained IoT devices, the Internet Engineering Task Force (IETF) Authentication and Authorization for Constrained Environments (ACE) working group formed and profiled the OAuth protocol suite. Reusing already existing security protocols offers many benefits, since designing security protocols is a complicated task. Over the years, several technologies for automated verification, such as Tamarin [6] and Easycrypt [1], have been developed by researchers. Given a protocol design and a set of security properties (such as secrecy and authentication), these tools can help prove that these properties hold for any potential scenario, under a given threat model. These tools have become popular as researchers find prominent internet security protocols vulnerable. In this paper, we use the formal analysis tool Tamarin to analyze the ACE-OAuth protocol, and illustrate how protocol designers can analyze their own extensions.