  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.
