Dialects for CoAP-like Messaging Protocols

TL;DR

This paper introduces a lightweight, formal dialect for the CoAP messaging protocol to enhance security in resource-constrained IoT systems, analyzing vulnerabilities and ensuring property preservation through formal methods.

Contribution

It defines a formal, modular dialect for CoAP, formalizes attack models, and proves property preservation, enabling systematic security analysis and attack search.

Findings

Dialect preserves LTL properties of CoAP applications.

Formal attack models identify specific vulnerabilities.

Case studies demonstrate attack detection and dialect effectiveness.

Abstract

Messaging protocols for resource limited systems such as distributed IoT systems are often vulnerable to attacks due to security choices made to conserve resources such as time, memory, or bandwidth. For example, use of secure layers such as DTLS are resource expensive and can sometimes cause service disruption. Protocol dialects are intended as a light weight, modular mechanism to provide selected security guarantees, such as authentication. In this report we study the CoAP messaging protocol and define two attack models formalizing different vulnerabilities. We propose a generic dialect for CoAP messaging. The CoAP protocol, dialect, and attack models are formalized in the rewriting logic system Maude. A number of case studies are reported illustrating vulnerabilities and effects of applying the dialect. We also prove (stuttering) bisimulations between CoAP messaging applications and dialected versions, thus ensuring that dialecting preserves LTL properties (without Next) of CoAP applications. To support search for attacks in complex messaging situations we specify a simple application layer to drive the CoAP messaging and generalize the attack model to support a form of symbolic search for attacks. Two case studies are presented to illustrate the more general attack search.