Dialects for CoAP-like Messaging Protocols

TL;DR

This report proposes a generic dialect for CoAP messaging and proves (stuttering) bisimulations between CoAP messaging applications and dialected versions, thus ensuring that dialecting preserves LTL properties (without Next) of CoAP applications.

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.

Figures (2)

• Figure 1: Summary of bridge application attacks. The column nRnd is the number of rounds, mcX is delay argument to the mcX attack capability, and msg is the message identifier of the attacked message.
• Figure 2: Summary of attacks on PnP. The column nRnd is the number of rounds, mcX is delay argument to the mcX attack capability, and msg is the message identifier of the attacked message.

Theorems & Definitions (15)

• definition thmcounterdefinition: Initial CoAP configuration
• definition thmcounterdefinition: Initial dialected CoAP configuration
• proposition thmcounterproposition: Mte based characterization of reachable CoAP configurations
• proposition thmcounterproposition: Mte based characterization of reachable dialected CoAP configurations.
• definition thmcounterdefinition: $\sim$-bisimulation
• definition thmcounterdefinition: UDX and simulation
• lemma thmcounterlemma: Inverse relation
• theorem 1: Stuttering bisimulation in the absence of attacks.
• proof
• corollary thmcountercorollary