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.

翻译：面向资源受限系统（如分布式物联网系统）的消息协议，常因出于节省时间、内存或带宽等资源而做出的安全选择，易受攻击。例如，采用DTLS等安全层会消耗大量资源，有时甚至可能导致服务中断。协议方言旨在作为一种轻量级、模块化的机制，以提供特定的安全保证（如身份验证）。本报告研究了CoAP消息协议，并定义了两个形式化不同漏洞的攻击模型。我们提出了一种通用的CoAP消息协议方言。CoAP协议、方言及攻击模型均在重写逻辑系统Maude中进行了形式化。通过多个案例研究，报告展示了漏洞情况以及应用方言后的效果。我们还证明了CoAP消息应用程序与其方言化版本之间的（停滞）互模拟关系，从而确保方言化能够保持CoAP应用程序的LTL属性（不含Next算子）。