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

Luca Arnaboldi, Hannes Tschofenig

Research output: Contribution to conferencePaperpeer-review

Abstract / Description of output

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.
Original languageEnglish
Number of pages13
Publication statusPublished - 20 Mar 2019
Event4th OAuth Security Workshop 2019 - Stuttgart, Germany
Duration: 20 Mar 201922 Mar 2019


Workshop4th OAuth Security Workshop 2019
Abbreviated titleOSW 2019
Internet address

Keywords / Materials (for Non-textual outputs)

  • IETF
  • OAuth
  • ACE-OAuth
  • protocol verification
  • security
  • standardization


Dive into the research topics of 'A Formal Model for Delegated Authorization of IoT Devices Using ACE-OAuth'. Together they form a unique fingerprint.

Cite this