11institutetext:  SRI International, Menlo Park, USA, 11email:
<EMAIL_ADDRESS>
# Dialects for CoAP-like Messaging Protocols

Carolyn Talcott 11

###### 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.

###### Contents

  1. 1 Introduction
  2. 2 Background
    1. 2.1 The CoAP protocol
    2. 2.2 Dialects
    3. 2.3 Rewriting logic and Maude
  3. 3 Executable Specification of CoAP
    1. 3.1 Data types
    2. 3.2 Rules
    3. 3.3 Attack specification
    4. 3.4 CoAP Scenario Specification
    5. 3.5 Sample scenarios.
  4. 4 Attack Models
    1. 4.1 Active attacker
    2. 4.2 Reactive attacker
    3. 4.3 More possibilities
    4. 4.4 Attack-model specification.
  5. 5 Example reactive attacks
    1. 5.1 R1. Redo/revert an action
    2. 5.2 R2. Violating ordering or concurrency constraints
    3. 5.3 R3 Duplication of a process.
    4. 5.4 R4. Spoofing (Redirect GET request/response)
  6. 6 Dialect functions
  7. 7 Specification of a CoAP dialect wrapper
    1. 7.1 Dialect messages and configurations
    2. 7.2 Dialect Rules
    3. 7.3 CoAP dialect transform
    4. 7.4 Dialected CoAP Scenarios
  8. 8 Dialect properties
  9. 9 Related Work
  10. 10 Conclusions
  11. 0.A Characterization of reachable CoAP system configurations
  12. 0.B CoAP vulnerabilities
    1. 0.B.1 The Selective Blocking Attack.
    2. 0.B.2 The Request Delay Attack.
    3. 0.B.3 The Delay with Reordering Attack.
    4. 0.B.4 The Response Delay and Mismatch Attack.
    5. 0.B.5 Delaying and mismatching response to GET requests
    6. 0.B.6 Delaying and mismatching response from other resource
    7. 0.B.7 Delaying and mismatching response from other resource variant
  13. 0.C Bisimulation proofs

##  1 Introduction

There is a rapidly growing number of networks of IoT devices that impact our
daily lives. They enable smart homes, offices, factories, and infrastructure.
They are increasingly used in health care, precision agriculture, logistics,
supply chain management, and situation awareness. The IoT devices sense and
act on the physical environment and must operate using limited resources
(energy, bandwidth, memory, compute power, …). The vulnerabilities of small
inexpensive devices are magnified when deployed at scale. Security is crucial
for safe operation but security is typically resource intensive. Design of
such systems must balance balance resources used for messaging and for
security.

Protocol dialects are a light weight mechanism that can provide authentication
and possibly additional security services such as integrity. A dialect
transforms the underlying protocol to mutate messages before sending such that
only dialect partners can revert the mutation for delivery to the intended
receiver. A key feature of dialects is to rapidly change the mutation used to
prevent attackers from using any decoding information they might gain. This
_moving target defense_ means that the complexity of mutation processing can
be kept low without compromising the security guarantee. The need to change
mutations presents a significant challenge to synchronize change across
distributed network nodes.

Existing dialect works, for example [11, 3, 8], usually consider protocols
running over TCP or other reliable transport. In this case mutations can
reasonably be synchronized based on time. In the case of unreliable transport
where messages can be delayed, reordered, lost, or repeated, time-based
synchronization is problematic. Unreliable transport is mentioned in [2] as
one classification parameter, but synchronization mechanisms for this case are
not treated.

In this work we study dialects for protocols running over unreliable
transport, using the CoAP messaging protocol [9] as prototypical example. We
investigate the use of counters, analogous to those used to prevent replay in
security protocols. for synchronizing. We consider two methods of evaluating
the CoAP specification and dialect wrapper. One is based on the CoAP
vulnerabilities discussed in [4] and the other is based on properties a CoAP
enabled endpoint could assume when running over an unreliable transport layer
such as UDP.

For the vulnerability case, we formalize the attack scenarios presented in [4]
as motivation for strengthening the specification. These scenarios consider an
attacker that can only block/drop or delay messages. We use reachability
analysis to look for attacks. In some cases the Maude endpoints exhibit the
expected vulnerability. in some cases because the Maude specification
implements some of the stronger mechanisms, the attack fails, but there are
related attacks. In some cases an attacker that can redirect messages can
realize the attack, but dialecting mitigates such attacks.

For the CoAP properties case the goal is to identify guarantees provided by
CoAP messaging running on an unreliable transport, identify attack points, and
corresponding attack model, and prove that dialecting provides adequate
defense. This is formalized using stuttering bisimulation relations.

#### Contributions.

The main contributions of this report are:

  * •

Executable specification of the CoAP messaging protocol (Section 3).

  * •

Specification of two families of resource limited attack models (Section 4):
an active attacker that can modify messages in transit and a reactive attacker
that can observe messages in transit and transmit (modified) copies.

  * •

Specification of a generic dialect layer and transform for messaging protocols
(Section 7).

  * •

Reachability analysis demonstrating CoAP vulnerabilities identified in [4]
(Appendix 0.B). These require an active attacker.

  * •

Reachability analysis demonstrating diverse reactive attacks (Section 5).

  * •

An analysis of protection provided by the proposed dialect class in
unreliable/reliable networks (Section 8).

  * •

Proof of stuttering bisimilarity theorems characterizing effects of the
dialect transformation (Appendix 0.C).

#### Plan.

Section 2 provides background information on CoAP, dialects, and rewriting
logic/Maude. Section 3 describes the Maude specification of CoAP messaging.
Resource limited attack models are presented in Section 4 with examples
illustrating a variety of attacks presented in Section 5. In Section 6 we
present the abstract mutation functions of the proposed dialect scheme. The
Maude specification of the CoAP dialect is given in Section 7. In Section 8 we
discuss the properties of dialects such as the CoAP dialect. The relation to
[2] is discussed in Section 9. Concluding remarks are given in Section 10.

In Appendix 0.A we spell out key properties of CoAP system executions,
including characterizing the minimal time elapse function. In Appendix 0.B we
specify the scenarios illustrating CoAP vulnerabilities listed in [4] and do
reachability analysis to determine which vulnerabilities are realized by the
Maude specification. We also analyze the dialected versions of each scenario.
In Appendix 0.C we prove two bisimulation theorems for dialected CoAP systems,
verifying relations proposed in Section 8.

The Maude specification and case studies can be found at
https://github.com/SRI-CSL/VCPublic in the folder CoAPDialect.

##  2 Background

###  2.1 The CoAP protocol

The Constrained Application Protocol (CoAP) [9, 4] is an HTTP-like client-
server Protocol for use by resource-constrained devices (e.g. low power) and
networks (low bandwidth, lossy). CoAP provides a request/response RESTFUL
interaction model between application endpoints. Servers hold resources that
can be generated, updated, accessed by clients. An endpoint can be a client, a
server, or both. A design goal is to keep message overhead small, to limit
need for fragmentation. Note that server resources may be connected to
actuators having effects on the environment.

CoAP features include UDP binding (reliability supported at the protocol level
by a retry mechanism) and asynchronous two-way message exchange. A binding to
Datagram Transport Layer Security (DTLS) provides security, but with
substantial overhead. Expected applications include: smart buildings,
instrumented infrastructure, medical devices, etc.

RFC7252 specifies a binary format for CoAP messages. Here we present an
abstract data-type view. A CoAP message consists of four parts: Header, Token,
Options, and Payload. The header has four parts: Version, Type, Code, and
MsgId (we will ignore the version).

The header type is one of `{CON, NON, ACK, RST}`. A message of type CON is
confirmable. The receiver must acknowledge with a message of type ACK, in
addition to a response if appropriate. The sender should resend a CON message
if no ACK is received within ACK-TIMEOUT time. There is a bound on the number
of resends (a configuration parameter). A message of type NON is non-
confirmable. If received it may require that a response is sent, but no
separate acknowledgment is sent. A message of type RST is a reset message,
used to indicate receipt of message that can’t be handled, also use as a kind
of ping.

Code is an HTTP like code that determines if the message is a request or
response. In the case of a request the code also determines the method–one of
GET,POST,PUT,DELETE. In the case of a response, the code determines if the
result is a success (with value in the payload), a client error, or a server
error.

The MsgId header element is a string that uniquely identifies the message
(among messages from the sender). It is used to match acknowledgements to CON
messages. It also is used to provide limited replay protection. Message
identifiers have a limited lifetime (a configuration parameter) after which
they can be reused.

The token message component is a unique identifier generated by a requestor to
match request to response. Options is a list of name-value pairs used to
specify additional information, including: content-format, request Uri, and
response Uri (of a created resource). Payload contains additional request
information (for example the value to PUT) or response value (for example the
result of a GET).

The rules for handling requests with a given method are similar to those for
HTTP. A response can be _piggy backed_ on the acknowledgement of a CON
request. A separate response can be of type CON or NON. Servers are required
to respond to legitimate requests, but they should only process a request
once. Thus if a confirmable request is resent, for example because the
acknowledgement was lost or delayed, the server may just resend the ACK or it
may resend the actual response, but it should not repeat the actions needed to
carry out the response.

###  2.2 Dialects

A protocol dialect is a variation on protocol messages intended as a light
weight mechanism to provide some additional security properties such as forms
of authentication or message integrity.

A dialect uses a family of lingos to transform protocol messages. A lingo
provides a pair of functions that are inverse of one another, possibly modulo
parameters. Dialects provide moving target defense in the sense that lingo
parameters and choice of lingo change over time in a dialect specified manner.
This means weaker forms of message transformation can be used, because even if
a message transformation is determined, it doesn’t help as that transformation
will not be used on later messages. It also means that honest participants
must synchronize on the choice of lingo and lingo parameters.

A typical application of dialects is to networks where at least some nodes are
resource limited devices. An example would be smart infrastructure with
sensors and actuators running on battery power, and with limited memory and
cpu capability. Thus a dialect should not require substantial resources. In
addition to providing new security properties, a dialect should preserve
important properties of the underlying protocol. The protocol may be running
on a network with limited bandwith, thus a dialect should not generate
significant additional traffic, and should not significantly increase message
size.

The following are some examples of dialects and their application. Dialects to
improve SDN (Software defined network) security are defined and evaluated in
[10, 11]. Two transformations based on HMAC over the message data are
proposed. One places the HMAC in the session id slot. This limits the HMAC
size and thus the hash key is changed every second. For messages that use this
slot, a 512-bit HMAC tag is appended to data packets. Sequence numbers are
included in the hashed content to prevent replay. Keys are generated from pre-
shared symmetric keys, delivered out-of-band. Dialects are implemented using
proxies inserted into the communication path to carry out the message
transformations. One goal is to protect against TLS downgrade attacks by
providing authentication for initial TLS communications.

Dialects for FTP and MQTT protocols using bit shuffling or packet splitting
are studied in [3]. A self-synchronization mechanisms is propsed. In [5] the
authors propose a Deep Neural Network mechanism for synchronization. A dialect
is implemented by (conceptually) inserting a separate process between the
protocol and the network.

Dialecting is proposed in [8] to mitigate known exploitable vulnerabilities in
IoT devices deployed in large numbers thus enabling massive attacks. The idea
is to transform functions that construct and parse message data structures to
construct and parse mutated data structures. The message constructor/parser
functions are identified automatically and message mutations are typically per
message field. Specific mutations are designed using testing. Dialects are
implemented by modifying the identified message constructor and parser
functions of the protocol implementation. The method is evaluated on
implementations of MQTT, LwM2M, and DDS. In the experiments, the mutations
successfully blocked reproducible attacks corresponding to a selected set of
CVEs reported for the protocols

The above works propose dialects and evaluate them experimentally. In [2] a
formal framework for specifying and applying dialects is proposed. The ideas
are illustrated using the MQTT protocol. This work and its relation to the
current work is discussed in detail in section 9.

###  2.3 Rewriting logic and Maude

Rewriting logic [6] is a logic for specifying concurrent and distributed
systems. A rewrite theory has the form $(\Sigma,\mathcal{E},\mathcal{R})$
where $\Sigma$ is a signature specifying a partial order of sorts, and a set
of operators (the name, argument sorts and result sort).
$(\Sigma,\mathcal{E})$ is the equational sub-theory, where the equations
$\mathcal{E}$ define functions and properties declared in the signature.
$\mathcal{R}$ is the set of rewrite rules of the form $l:lhs\Longrightarrow
rhs~{}~{}\mathit{if}~{}c.$ Here $lhs,rhs$ are terms, possibly with variables,
and $c$ is a boolean term, the condition, which is optional. An important
feature of rewriting logic is that rules are applied locally, i.e. to matching
sub-terms of the term being rewritten. Given terms (of the language given by
$\Sigma$) $t$, $t^{\prime}$ we have $t\Longrightarrow t^{\prime}$ ($t$
rewrites to $t^{\prime}$) using rule $l$ just if there is a position $p$ of
$t$ and a substitution $\sigma$ matching $lhs$ to the subterm of $t$ at $p$
($\sigma(lhs)=_{\mathcal{E}}t\downarrow p$) such that $\sigma(c)$ holds and
$t^{\prime}$ is the result of replacing the subterm of $t$ at $p$ by
$\sigma(rhs)$.

Maude [1] is a language and tool implementing rewriting logic. Maude can be
downloaded from the Maude website [12]. Rewrite theories are represented by
Maude modules. Functional modules (declared using the keyword fmod at the
beginning and endfm at the end) represent equational theories (with no rules).
System modules (declared using the keyword mod at the beginning and endm at
the end) represent rewrite theories with rules. We introduce the main Maude
syntax elements with examples from the CoAP specification (discussed in detail
in Section 3). Sorts and their ordering are declared using the keywords sort
and subsort. For example, the following declares two sorts Msg (the message
sort) and MsgS (multisets of messages) with Msg (singleton sets) being a
subsort of MsgS.

        sort Msg MsgS .
        subsort Msg < MsgS .

Functions/operators are declared using the keyword op. For example, the
operator m constructs a message from two strings (the target and source) and a
term of sort Content. The attribute ctor says that m is a constructor and will
not be subject any equations. mtM is a constant (no arguments) denoting the
empty message set. The operator `__` has empty syntax, the blanks denoting
argument positions. It correspond to union of multi sets. That union is
associative and commutative with unit the empty set is expressed by the
attributes assoc, comm, and id: mtM. The ctor attribute says that no other
equations apply to elements of MsgS. Thus multisets are generated from the
empty set and singletons by union.

        op m : String String Content -> Msg [ctor] .
        op mtM : -> MsgS [ctor] .
        op __ : MsgS MsgS -> MsgS [ctor assoc comm id: mtM] .

This is a general pattern used to specify (multi)sets of a given sort. A
similar pattern is used to specify lists of elements, omitting the comm
attribute.

Equations are introduced with the key word eq (or ceq for conditional
equations). For example, the function getTgt, that gets the target of a
message, is defined by the following declaration and equation.

        op getTgt : Msg -> String .
        eq getTgt(m(tgt:String,src:String,c:Content)) = tgt:String .

Here we use inline variable declaration. For example, tgt:String declares tgt
to be a variable of sort String. Alternatively, we could declare the variable
globally.

        vars tgt src : String .
        var c : Content .
        eq getTgt(m(tgt,src,c)) = tgt .

Rewrite rules are signalled by the keyword rl (crl for conditional rules),
optionally followed by a label in []s. The rule labeled net applies to any
configuration that has a network element of the form net(dmsgs0 dmsg,dmsgs1),
and moves dmsg from the first to the second argument of the constructor net.
111A delayed message dmsg has the form msg @ d where d is a natural number
representing the amount of time it will take the message to traverse the
network.

        rl[net]:
        net(dmsgs0 dmsg,dmsgs1) => net(dmsgs0,dmsgs1 dmsg)
        [print "\n[net] "]  .

The rule attribute `[print "\n[net] "]` causes Maude to print to the terminal
“[net]” on a new line each time the rule is applied in an execution. This
print feature allows the user to define a model specific execution trace that
is useful for debugging or demonstrating features of an execution.

There are many Maude tools for static and dynamic analysis of a system
specification. In the present work we only need the rewrite command for
prototyping and the search command for reachability analysis. Assume you have
defined a module SCENARIO that includes all the modules defining rules and
data structures defining your model. Assume further that system configurations
are of sort Sys and the module SCENARIO defines a constant initSys of sort
Sys. Then we can use the command

        rew [n] initSys .

to find one way that initSys might evolve for n steps. If you omit [n] the
execution will run until a state is reached that has no successors (a terminal
state). This should be used with care as there may not be a reachable terminal
state! If a boolean function P(sys:Sys) is defined, one can use the search
command to carryout reachability analysis. The following search command will
return the first n distinct reachable states that satisfy the property P.

      search [n] initSys =>+ sys:Sys such that P(sys:Sys) .

If [n] is omitted Maude will search for all reachable states satisfying P.
Again caution is suggested as there may be infinitely many such states.

Example initial configurations and properties for our CoAP specification are
defined in section 3 and reachability analysis experiments for different
attack models are given in Sections 5 and Appendix 0.B.

##  3 Executable Specification of CoAP

The Maude specification of the CoAP messaging protocol consists of
specifications of data structures to represent execution state 3.1, rules
specifying the protocol behavior 3.2, and an attack specification framework
3.3. The data structures include a message data type and data structures
representing endpoint and network state. The basic CoAP rules model sending
and receiving messages, flow of messages in the network, and passing of time.
The attack model consists of a specification of attacker capabilities and a
rule for application of a capability to modify communications. The Maude
specification of the two families of attack models is given in Section 4.4 The
CoAP specification concludes with definitions of functions for generating
application message lists and scenario initial states ( Section 3.4) and some
small example scenarios and analyses to illustrate the ideas (Section 3.5).

###  3.1 Data types

#### Message data type.

The specification of the message data type is a direct formalization of the
(abstract) structure of messages as specified in [9]. Messages (sort Msg) are
constructed by the operation

        op m : String String Content -> Msg [ctor] .

thus a typical message term has the form m(tgt,src,content) with tgt, src
being strings identifying the receiver (target) and sender (source)
respectively.

The sort DMsg of delayed messages consists of terms of the form msg @ d where
msg is of sort Msg and d is the delay, a natural number (sort Nat). The delay
is used to model the time between sending and receiving a message (network
latency). It is also used to model the timer controlling resend of a
confirmable message.

As discussed in Section 2.1 message content (sort Content) is constructed from
sorts Head, multisets of Options, and Body (aka payload).

        op c : Head String Options Body -> Content [ctor] .

We define a constant mtBody of sort Body to stand for the empty payload, and
assume non empty payload is represented by strings: b(str). Elements of sort
Head are constructed by

        op h : String String String -> Head  [ctor] .

where in h(type,code,mid) the first string is the message type ("CON",
‘‘NON’’, "ACK" or "RST"), the second string is the HTTP-like code, and the
third string is the message unique identifier, generated by the sender, as
discussed in 2.1

The String element of a message content is the token used to match a response
to the corresponding request. Each request from a given source to a given
target should have a unique token generated for it.

Sort Options is a multiset of sort Option where mtO is the empty option set.
An individual option has the form o(oname,oval) where oname is a string naming
the option and oval is the option value of sort String or Nat. The current
specification supports options representing request URIs and URIs in a
response resulting from creation of a resource. For example the equation

        eq getPath(opts o("Uri-Path",path)) = path .

defines how to access the Uri-path of a request. Multisets of delayed messages
(sort DMsgS, id: mtDM) are defined similarly to multisets of messages shown
above.

Selectors are defined for each component of a message. For example the
selector for message type is defined as follows:

          op getType : Msg -> String .
          op getType : Content -> String .
          op getType : Head -> String .

          eq getType(m(dst:String,src:String,c:Content))
                    = getType(c:Content) .
          eq getType(c(h:Head,tok:String,opts:Options,body:Body))
                    = getType(h:Head) .
          eq getType(h(type,code,mid)) = type .

The CoAP protocol itself does not generate requests, rather it packages and
transmits application level messages. For testing and analysis purposes we
represent the application by a list of application level messages (requests)
(sorts AMsg, AMsgL) to be transmitted. An application message consists of six
strings and a message body. The strings specify: the application id, the
message target and type, the method, and the resource path and query
parameters if any.

       ****     appid    tgt   type   meth   path  qparams body
      op amsg : String String String String String String Body
              -> AMsg [ctor] .

The empty AMsgL is nilAM and list concatenation is `_;_`.

#### Endpoint state.

A CoAP network system consists of a set of endpoints (devices running CoAP)
and the network. The network is modeled as a pair of delayed message sets
net(dmsgs0,dmsgs1). Newly sent messages enter the first component, are moved
by the net (or an attacker) to the second component from which they are
delivered once the delay is zero.

An endpoint (also referred to as a device) is a term of sort Agent of the form

            [epid | attrs]

where epid is a string identifying the endpoint and attrs is a set of
attributes representing the endpoints current state. CoAP endpoint attributes
include attributes to track status of msgs sent and received in order to
implement the rules for reliability (confirmable messages) and deduplication.
They also include configuration parameters allowing each endpoint to be
configured differently if desired.

  * •

w4Ack(dmsgs): dmsgs is the set of confirmable messages sent and not yet
acknowledged. The delay part is the amount of time to wait before resending
the message;

  * •

w4Rsp(msgs): a message in msgs is either a non-confirmable request waiting for
a response, or a confirmable request for which an ACK has been received but
the response is still pending;

  * •

rspRcd(msgs): logs responses received to avoid reprocessing repeated
responses;

  * •

rspSntD(dmsgs): logs responses sent where the delay represents the message
id/token lifetime. It can be used to resend the response in case the original
is lost, and to detect replay attempts within the message id lifetime.

  * •

rsrcs(rmap): rmap is a map from resource paths to values, representing server
resources state;

  * •

ctr(n): n is a natural number used to model generating fresh/unique message Id
strings (genMid(prefix,n)) and unique tokens (genTok(prefix,n));

  * •

sendReqs(amsgl): a list of application messages to be transmitted

  * •

config(cbnds): a map from global parameter names to configured values,
examples include message send delay (abstracts time in transit,
cb("msgSD",n)), maximun number of resends (`cb("MAX_RETRANSMIT", n0)`),
backoff parameter for computing delay between resends (cb("msgQD",n1)),
congestion control parameters such as time to wait for an ACK before resending
a confirmable message (`cb("ACK_TIMEOUT", n2)`), etc..;

  * •

toSend(dmsg): an attribute used to store information returned by auxiliary
functions

A number of auxiliary functions on attributes are defined for use in
specifying rules. We discuss two examples. The function getMsgSndDelay looks
up the "msgSD" configuration parameter. This parameter models average network
transit time of a message.

        op getMsgSndDelay : Attrs -> Nat .
        op getMsgSndDelay : CBnds -> Nat .

        eq getMsgSndDelay(attrs config(cbnds)) =  getMsgSndDelay(cbnds) .
        eq getMsgSndDelay(cb("msgSD",n) cbnds) = n .

The function findRspRcd checks if a response message from dst has been
received in response to a request with identifier mid and token tok. It uses
the message selectors getSrc which would be the destination of the
corresponding request, and getTok to use to match the response to a request.
findRspRcd is used to avoid reprocessing responses and also to be able to
resend and ACK to a confirmable response.

        ****                    dst  mid     tok
        op findRspRcd : Attrs String String String -> Bool .
        op findRspRcd : MsgS String String String -> Bool .
        eq findRspRcd(devatts rspRcd(msgs), dst,mid,tok) =
              findRspRcd(msgs, dst,mid,tok) .
        ceq findRspRcd(msgs msg, dst,mid,tok) = true
          if getSrc(msg) == dst
          /\ getTok(msg) == tok .
        eq findRspRcd(msgs, dst,mid,tok) = false [owise] .

###  3.2 Rules

Five rules are used to specify CoAP executions. The rules labelled devsend and
rcv specify transmission and receipt of messages by an endpoint. The rule
labelled ackTimeout specifies when a confirmable message is resent. The rule
labelled net specifies the network action of moving a delayed message from the
input side to the output side. Finally, the rule labelled tick specifies the
passing of time. Rules devsend, rcv and ackTimeout operate on sub-
configurations consisting of an endpoint and the network, the rule net simply
transforms the network configuration element, while tick rule requires the
full system configuration `{conf}`, formed by encapsulating a configuration
term in curly braces. The net rule was discussed in Section 2.3. The remaining
rules are discussed in the remainder of this (sub)section.

#### Sending a message.

The rule devsend sends the first element, amsg, of the application message
list attribute. The variable devatts matches the remaining attributes of the
sending endpoint state. The rule can only fire if noW4Ack(devatts) is true and
sending is enabled (canSend(devatts)). These tests model the CoAP congestion
control. noW4Ack(devatts) holds if the number of confirmable messages awaiting
acknowledgements is not greater than the configuration parameter "w4AckBd" and
canSend checks that the sndCtr attribute of devatts is 0. The function sndAMsg
constructs the delayed message to send, dmsgs, and updates devatts. To
construct dmsgs, a message id and token are generated and the method string is
converted to a code, then the header, options and body are used to produce the
message content. The message delay is obtained from the configuration
parameter "msgSD". If the message is type CON it is added to the w4Ack
attribute of devatts with a delay given by the configuration parameter
`"ACK_TIMEOUT"`, otherwise the message is added to the w4Rsp attribute. The
ctr attribute is incremented by 2 (the two uses to generate a message id and a
token), and the sndCtr is reset using the configuration parameter "msgQD".

        crl[devsend]:
          [epid | sendReqs(amsg ; amsgl) devatts ]
          net(dmsgs0,dmsgs1)
          =>
          [epid | sendReqs(amsgl) devatts1]
          net(dmsgs0 dmsgs,dmsgs1)
        if noW4Ack(devatts)
        /\ canSend(devatts)
        /\ devatts1 toSend(dmsgs) := sndAMsg(epid,amsg, devatts) .

#### Receiving a message.

A message with 0 delay is received by the target endpoint using the rule
labelled rcv. The work is done by the function rcvMsg which uses the message
header code to classify the message as “Request”, “Response”, “Empty”, or
“UnKnown” and calls rcvRequest, rcvResponse, rcvEmpty, or sendReset (if
confirmable). Otherwise the message is dropped. An empty message is either an
acknowledgement or a reset. In the acknowledgement case, the corresponding
delayed message in the w4Ack attribute is removed if any, and the underlying
message is added to the w4Rsp attribute to be able to process the pending
response. In the reset case, if the message is confirmable an acknowledgement
is sent (this implements a “PING” functionality) otherwise the reset is
ignored.

        crl[rcv]:
          [epid | devatts] net(dmsgs0,dmsgs1 msg @ 0 )
          =>
          [epid | devatts1 ] net(dmsgs0 dmsgs,dmsgs1)
        if getTgt(msg) == epid
        /\ toSend(dmsgs) devatts1 := rcvMsg(epid, devatts, msg) .

The rules for handling requests are specified in [9] section 5.8. The function
rcvRequest implements these rules. It first checks whether it has already sent
a response to this request using matchingRsp(devatts,msg). If so, if the
request is confirmable, the ACK is resent, otherwise the message is ignored.
If the request is new the method is computed from the code and the appropriate
method specific function is called to process the message. As an example, if
the method is "GET", the function rcvGet is called. This function sends a
single message in response:

        msg = m(src,epid,c(h(rtype,code,rmid),tok,mtO,body) .

rmid is a new message id, src is the sender of the request, tok is the token
of the request message. The type, rtype, is "ACK" if the request in
confirmable. In this case, msg is a combined acknowledgement and response. The
type is "NON" if the request is nonconfirmable. In this case msg is a simple
response. body is the result of attempting to access the resource at the path
specified in the request message options using getResourceVal(devatts,path).
It is b(val) if a value val is found, and mtBody if the resource does not
exist. The message code is "2.05" if a resource value is found, indicating
successful GET. The message code is "4.04" if the resource is not found,
indicating an error. rcvGet updates the endpoint attribute by incrementing the
counter, ctr, and recording that the request has been processed by adding msg
to the rspSnt attribute.

The function rcvResponse checks if it is combined with an acknowledgement or a
simple response. In the former case, the matching request is removed from the
w4Ack attribute, if any, and adds the response message to the rspRcd if it has
not already been seen. This abstracts interaction with the application layer.
In the case of a simple response, if a response has already been received, an
acknowledgment is sent if the response is confirmable and otherwise the
message is ignored. If this is a new response, it is recorded in the rspRcd
attribute, any occurrence of the matching request is removed from the w4Ack
and w4Rsp attributes. If the response is confirmable an acknowledgement is
sent.

#### ReSending a message.

The rule ackTimeout can fire if a message in the w2Ack attribute has delay 0.
The option o("rcnt",n) records the number of resends of the message. If this
count is less than the max allowed (configuration parameter
`"MAX_RETRANSMIT"`) then the message is returned to the w4Ack attribute with a
new ack wait time, delay, computed using the backOff function that doubles the
delay for each resend. Finally, the message with normal sending delay is put
in the network input side.

      crl[ackTimeout]:
        [epid | w4Ack((msg @ 0) dmsgs) config(cbnds) attrs]
        net(dmsgs0,dmsgs1)
        =>
        [epid | w4Ack(dmsgs2 dmsgs) config(cbnds) attrs]
        net(dmsgs0 dmsg, dmsgs1)
      if  m(dst,epid,c(hd,tok,opts o("rcnt",n),body)) := msg
      /\ opts0 :=  o("rcnt",s n )
      /\ delay := backOff(getAckWait4(cbnds), s n)
      /\ dmsg :=  m(dst,epid,c(hd,tok,opts,body)) @
                    getMsgSndDelay(cbnds)
      /\ dmsgs2 :=  (if n < getMaxReSnd(cbnds)
                     then m(dst,epid,c(hd,tok,opts opts0,body)) @
                          delay
                     else mtDM  --- stop resending
                     fi)  .

#### Passing time.

For managing the passing of time, we follow the Real-time Maude approach [7].
The idea is that there is an earliest time at which some instantaneous rule
will be enabled to fire, called the minimal time elapse (mte). If the mte is
zero then the enabled rules should be applied until there are no more. If the
mte is greater than zero then time passes by this amount, reaching a situation
where some rules can fire at the current time (or the state is terminal). It
is the job of the specification designer to ensure that only a finitely many
rules can fire before time must pass. In the CoAP model, mte is greater than
zero if all delays of messages in the network, or an w4Ack attribute, are
greater than zero, or a message send is pending but the sndCtr is non-zero.
The rule labelled tick formalizes the above. Here nz has sort NzNat (non-zero
natural number). The function passTime decrements each message delay in the
network and w4Ack attributes and each sndCtr by nz. It also decrements delays
of messages in rspSntD attributes, modeling the decrease in lifetime of the
identifier and token.

        crl[tick]:
        {conf} => {passTime(conf,nz,mt)}
        if nz := mte({conf}) .

###  3.3 Attack specification

Our specification of attacks against CoAP messaging consists of a
specification of attack capabilities (sort Cap), a function doAttack, an
attacker agent, and a rule for executing attacks, that invokes doAttack on a
target message using an available capability. Attack models resulting from
different choices of capability sets, and corresponding doAttack clauses, are
discussed in Section 4. We note that the usual symbolic model matching
patterns representing attacker ability to construct messages doesn’t work
because there is no a priori expectation of what messages are expected.

An attacker agent has the same form as a device endpoint

          [aid  |  caps(acaps) attrs]

but with attacker specific attributes that include, caps(acaps), the
capabilities attribute specifying what the attacker can do. The rule labelled
attack specifies the semantics of an attack capability. It selects a target
delayed message, dmsg, from the network input component, and a capability from
the attackers capability set, and calls doAttack with the current attributes,
the target message and the capability. The result is a replacement, dmsgs for
dmsg and possibly updated attributes. For example, if the capability
corresponds to drop then dmsgs is the empty set, and if the capability
corresponds to replay after delay $n$ then dmsgs is dmsg dmsg1 where dmsg1 is
dmsg with $n$ added to its delay.

        crl[attack]:
          [aid  |  caps(acaps acap) attrs]
           net(dmsgs0 dmsg,dmsgs1)
         =>
          [aid  |  attrs1]
          net(dmsgs0,dmsgs1 dmsgs)
         if toSend(dmsgs) attrs1 :=
            doAttack(attrs caps(acaps),dmsg,acap) .

###  3.4 CoAP Scenario Specification

A scenario is specified by an _intial system configuration_. This together
with the CoAP rewrite theory determines a set of execution traces and the
reachable states of the scenario. To support systematic testing of CoAP
messaging and analysis of attacks we defined two functions to generate initial
configurations for scenarios tCS2C (test Client Server 2 endpoints) and tCS3C
(test Client Server 3 endpoints). These are used in the experiments validating
the vulnerabilities discussed in [4], described in Appendix 0.B. They were
also used in experiments testing various CoAP messaging patterns and effects
of dialecting.

In addition to having an empty network, initial configurations are
characterized by the initial attributes of the endpoints. The function
initDevAttrs defines the initial values of attributes that are the same for
all endpoints in the scenarios considered. It has two arguments that are
passed on to the function mkCoapConf the defines global configuration
parameters

        op mkInitDevAttrs : Nat Nat -> Attrs .
        eq mkInitDevAttrs(mqd:Nat,w4ab:Nat) =
          w4Ack(mtDM)
          w4Rsp(mtM)
          rspSntD(mtDM)
          rspRcd(mtM)
          ctr(0)
          config(mkCoapConf(mqd:Nat,w4ab:Nat)) .

To experiment with different delays for sending application requests
mkCoapConf has two arguments giving the values of the "msgQD" and "w4AckBd"
configuration parameters. Recall that "msgQD" is the delay between message
sends, and sending is blocked if there are more than "w4AckBd" confirmable
messages awaiting acknowledgement.

        op mkCoapConf : Nat Nat -> CBnds .
        eq mkCoapConf(mqd:Nat,w4ab:Nat) =
          cb("ACK_TIMEOUT", 5)
          cb("ACK_RANDOM_FACTOR", 2)
          cb("MAX_RETRANSMIT", 1)
          cb("msgSD",2)
          cb("msgQD",mqd:Nat)
          cb("w4AckBd",w4ab:Nat)
          cb("ttl", 10) .

We define initial system configurations as follows.

######  Definition 1 (Initial CoAP configuration)

An initial CoAP system configuration sysI contains one network configuration
element of the form

        net(mtDM,mtDM)

and a finite number of endpoint agents of the form

        [eid | sendReqs(amsgl:AMsgL) rsrcs(rbnds:RMap)  initDevAttrs(mqd:Nat,w4ab:Nat)]

An initial system configuration with attacker also has one attack agent of the
form

         [ "eve" | kb(dmsgs) caps(caps:Caps)]

which we omit if caps:Caps is empty.

#### Initial System Configuration Generators.

The scenario generators use auxiliary functions to generate endpoint agents
(mkDevC) and an optionally an attack agent (mkAtt).

The device agent generator mkDevC has arguments specifying its identifier (n),
initial delay before sending messages (j), its list of application messages to
send (amsgl), the initial state of any resources (rbnds), and two arguments
passed on to mkInitDevAttrs.

        op mkDevC : Nat Nat AMsgL RMap Nat Nat -> Agent .
        ceq mkDevC(n,j,amsgl,rbnds,mqd:Nat,w4ab:Nat) =
          [ epid | sendReqs(amsgl) rsrcs(rbnds)
                   sndCtr(j) mkInitDevAttrs(mqd:Nat,w4ab:Nat) ]
        if epid := "dev"  + string(n,10) .

The attack agent generator mkAtt has one argument, the capability set caps.

        op mkAtt : Caps -> Agent .
        eq mkAtt(caps) = ["eve" | kb(mtDM) caps(caps)] .

The function tCS2C has three groups of arguments, one group for each of two
devices and one (singleton) group for the attacker. The resul is a client
device, "dev0", with a list of application messages amsgl to send; a server
device, "dev1", with resources rmap; and an attacker, "eve", with capabilities
caps. The function simply applies the appropriate agent constructor to each
group of arguments and adds an initial empty network state. If there are no
attack capabilities (mtC), then no attack agent is generated.

    ****  2 endpoint configuration, with devconfig parameters
    **** w4ab = n requires w4Ack to have <= n dmsgs
    **** mqd = m requires delay of m before sending next request
        op tCS2C : Nat Nat AMsgL RMap Nat Nat
                   Nat Nat AMsgL RMap Nat Nat
                  Caps -> Conf .
        eq tCS2C(n0,j0,amsgl0,rbnds0,mqd0:Nat,w4ab0:Nat,
                 n1,j1,amsgl1,rbnds1,mqd1:Nat,w4ab1:Nat,
                caps) =
           net(mtDM,mtDM)
           mkDevC(n0,j0,amsgl0,rbnds0,mqd0:Nat,w4ab0:Nat)
           mkDevC(n1,j1,amsgl1,rbnds1,mqd1:Nat,w4ab1:Nat)
           (if caps == mtC
            then mt
            else mkAtt(caps)
            fi)  .

The definition of tCS3C is similar, it just has one more group of device
arguments and generates a third device.

A typical two endpoint scenario has one endpoint with some messages, amsgl0,
to send (a client role) and one with initial resources rbnds1 (a server role)
with message sending delay 5 and w4Ack bound of 0.

        op tCS : AMsgL RMap Caps -> Conf .
        eq tCS(amsgl0,rbnds1,caps) =
            tCS2C(0,0,amsgl0,mtR,5,0,
                  1,1,nilAM,rbnds1,5,0,
                 caps) .

A similar scenario but with two servers (with initial resources rbnds1 and
rbnds2) is created by the function tCSS.

        op tCSS : AMsgL RMap RMap Caps -> Conf .
        eq tCSS(amsgl0,rbnds1,rbnds2,caps) =
            tCS3C(0,0,amsgl0,mtR,5,0,
                  1,1,nilAM,rbnds1,5,0,
                  2,1,nilAM,rbnds2,5,0,
                 caps) .

Finally, we define application message constructors to use in creating
specific scenarios. The functions mkGetC / mkGetN construct confirmable/non-
confirmable GET messages. The arguments are a message identifier (id), the
receiver (tgt), and the resource path (path).

        ****         Id     Tgt   Resource
        op mkGetC : String String String -> AMsg .
        op mkGetN : String String String -> AMsg .
        eq mkGetC(id,tgt,path) =
             amsg(id,tgt,"CON","GET",path,"",mtBody) .
        eq mkGetN(id,tgt,path) =
             amsg(id,tgt,"NON","GET",path,"",mtBody) .

Similarly the functions mkPutC / mkPutN construct confirmable/non-confirmable
PUT messages with an additional argument, the value (val) to assign to the
resource.

        ****         Id    Tgt    Resource  Val
        op mkPutC : String String String  String -> AMsg .
        op mkPutN : String String String  String -> AMsg .

        eq mkPutC(id,tgt,path,val) =
             amsg(id,tgt,"CON","PUT",path,"",b(val)) .
        eq mkPutN(id,tgt,path,val) =
             amsg(id,tgt,"NON","PUT",path,"",b(val)) .

The function mkDelN creates a non-confirmable DELETE message with the same
arguments as the GET messages.

        ****         Id    Tgt    Resource
        op mkDelN : String String String -> AMsg .
        eq mkDelN(id,tgt,path) =
             amsg(id,tgt,"NON","DELETE",path,"",mtBody) .

In order to search for attacks based on order of events (for example, message
receives) we introduce a Log configuration element.

        sort Log .   subsort Log < ConfElt .

A log is a list of log items specified as follows

        sorts LogItem LogItemL .
        subsort LogItem < LogItemL .
        op nilLI : -> LogItemL [ctor] .  --- the empty list
        op _;_ : LogItemL LogItemL -> LogItemL
                [ctor assoc id: nilLI] .  --- list concatenation

    op log : LogItemL -> Log [ctor] .  --- the log entry

Receive of a request to PUT value val at resource path path by endpoint with
identifier epid is represented by the log item

            rcvP(epid,path,val) .

Logging is currently only used by the rcvPut function that adds the attribute

      toLog(rcvP(epid,path,val))

to the returned attribute set. The receive rule crl[rcv] is augmented with the
conditional clauses

        /\ conf1 := doLog(conf,devatts1)
        /\ devatts2 := clearToLog(devatts1)

to add any logitems from a toLog attribute to the log configuration element,
and remove any toLog attribute from the device attributes.

To support defining properties based on ordering of events we define a
function findRcvLI that given a log item list, a starting index, and a pattern
(three string variables) returns a pair (sort LogItemIx) consisting of the
first matching event on or after the starting index, together with the index
of the event in the list.

        sort LogItemIx .
        op ‘{_‘,_‘} : LogItem Nat -> LogItemIx [ctor] .

        op findRcvLI : LogItemL Nat String String String ->  [LogItemIx] .
        op findRcvLIX : LogItemL String String String  Nat ->  [LogItemIx] .

        eq  findRcvLI(lil:LogItemL,n,epat,ppat,vpat)
            = findRcvLIX(nthCdr(lil:LogItemL,n),epat,ppat,vpat,n) .

        eq findRcvLIX(li:LogItem ; lil:LogItemL,epat,ppat,vpat,n)
           =
          (if matchesLI(li:LogItem,epat,ppat,vpat)
           then {li:LogItem,n}
           else findRcvLIX(lil:LogItemL,epat,ppat,vpat,s n) fi) .

The nthCdr(lil:LogItemL,n) function returns the suffix of the logitem list
lil:LogItemL beginning at the nth element (counting from 0). The logitem
rcvP(epid,path,val) matches the pattern (epat,ppat,vpat) if corresponding
elements of the triple match. A string matches a pattern string if the two are
equal or the pattern is "". An error value results if no matching event is
found.

For example to check that a request to "dev1" to unlock its door resource was
followed by one locking that door we can use the property

        subLIL(c:Conf,rcvP("dev1","door","unlock") ;
                      rcvP("dev1","door","lock"))

where subLIL checks that there is a sublist of the configuration log element
that matches the second argument logitem pattern list. It is defined using the
findRcvLI function as follows.

        op subLIL : Conf LogItemL -> Bool .
        eq subLIL(c:Conf log(litl),plitl) = subLILX(litl,plitl,0) .
        op subLIXL : LogItemL LogItemL Nat -> Bool .
        ceq subLILX(litl,rcvP(epat,ppat,vpat) ; plitl,n) =
              subLILX(litl, plitl,n0) =
         if {rcvP(epid0,path0,val0), n0} :=
                 findRcvLI(litl,n,epat,ppat,vpat)
        eq subLILX(litl,nilLI,n) = true .
        eq subLILX(litl,plitl,n) = false [owise] .

###  3.5 Sample scenarios.

To illustrate the use of the CoAP specification, and introduce some of the
attacks of interest we define some small scenarios and show how to search for
attacks. Attack models are discussed in more detail and formalized in Section
4.

Consider a scenario with client, "dev0", that requests server, "dev1", to
unlock (PUTCDU), then lock the door (PUTCDL). In between the resource "sig" is
set to "go" (PUTNSG). After a normal execution of this protocol, the door is
locked at the end.

          dev0           dev1
          ----           lock
           o --PUTCDU-->  o
           o <--ack --    o
           o <--2.04--    o
           o --PUTNSG-->  o
           o <--2.01--    o
           o --PUTCDL-->  o
           o <--ack --    o
           O <--2.04--    o

We use the function tCS and the application message constructors described
above to create the initial configuration for this scenario:

        iSys0 = {tCS(mkPutC("putCDU","dev1","door","unlock") ;
                     mkPutN("putNSG","dev1","sig","go") ;
                     mkPutC("putCDL","dev1","door","lock"),
                     rb("door","lock"),mtC)} .

Now we ask: Can the scenario (with no attacker) end with the door unlocked if
the attacker has no capabilities? This is done by searching for a terminal
state reachable from iSys0 in which the "dev1" "door" resource has value
"unlock".

        search [1] iSys0 =>! {c:Conf} such that
           checkRsrc(c:Conf,"dev1","door","unlock") .

There is no solution. Next we ask if the attacker who can drop a message can
force the scenario end with the door unlocked? iSys1 adds the drop capability
to the configuration iSys0.

        iSys1 = {tCS(mkPutC("putNDU","dev1","door","unlock") ;
                     mkPutN("putNSG","dev1","sig","go") ;
                     mkPutC("putNDL","dev1","door","lock"),
                rb("door","lock"),drop)}

We search for a final state where the "door" resource of "dev1" has value
"unlock".

        search [1] iSys1 =>! {c:Conf} such that
            checkRsrc(c:Conf,"dev1","door","unlock") .

There is no solution because even if the attacker drops the lock request,
since the request is confirmable, the client will retry. If the attacker can
drop two messages then it can force termination with the door unlocked [not
shown].

Suppose the attacker can replay a message (i.e. make a copy and delay it) as
in scenario iSys2.

        iSys2 = {tCS(mkPutC("putNDU","dev1","door","unlock") ;
                     mkPutN("putNSG","dev1","sig","go") ;
                     mkPutC("putNDL","dev1","door","lock"),
                  rb("door","lock"),replay(10))}

Can the attacker cause an unlock to follow a lock request? We search for an
execution in which a door lock request precedes an unlock request. (We could
also require that the unlock request was the last door request.)

        search iSys2 =>! {c:Conf} such that
            subLIL(c:Conf, rcvP("dev1","door","lock") ;
                           rcvP("dev1","door","unlock") ) .

There are two solutions. The log from the second solution follows.

      log(rcvP("dev1","door","unlock") ; rcvP("dev1","sig","go") ;
          rcvP("dev1","door","lock") ; rcvP("dev1","door","unlock"))

Now, consider a situation where there are two servers ("dev1" and "dev2") with
door resources. The client wants the state of the door at "dev1". Can the
attacker reroute the "GET" request so that the client receives the state of
the door at "dev2" instead?

Here we use and instance of a general attack capability

       mc(tgt,src,b:Bool,act(tpat,spat,d:Nat))

This capability applies to messages to tgt from src. It changes the target and
source according to tpat and spat ("" means no change) and adds d:Nat to the
delay. If the flag b:Bool is true the edited message replaces the original,
while if the flag b:Bool is false the original message is unchanged and the
edit is a copy.

          dev0         eve           dev1        dev2
          ----         ---          unlock       lock
           o -GETN(1)-> @ [-GETN(1)->] ?
           |            o               -GETN(2)->o
           | <-lock(1)- @ <---lock(2)--            o
           |          [<--unlock(1)--] o
           o <-oneof{lock,unlock}-

iSys3a is the scenario for the case when the attacker modifies a message in
transit. Note that the attacker must redirect both the request (changing the
target) and the response (changing the source).

        iSys3a = tCSS(mkGetN("getN","dev1" ,"door"),
                      rb("door","unlock"),rb("door","lock"),
                     mc("dev1","dev0",true,act("dev2","dev0",0))
                     mc("dev0","dev2",true,act("dev0","dev1",0))) .

To check for an attack we search for a final state in which the door resource
of "dev1" is unlocked, but "dev0" receives a response (apparently) from "dev1"
with the value "lock".

        search iSys3a =>! {c:Conf} such that
            checkRsrc(c:Conf,"dev1","door","unlock") and
            hasGetRsp(c:Conf,"dev0","dev1","getN","lock") .

There are 4 solutions of 33 states visited. The log is empty because the model
currently does not currently log "GET" requests.

Suppose the attacker can not change messages in transit, but can make and edit
copies. This is modelled by setting the flag in the capabilities to false, as
in the scenario iSys3r.

        iSys3r = tCSS(mkGetN("getN","dev1" ,"door"),
                      rb("door","unlock"),rb("door","lock"),
                      mc("dev1","dev0",false,act("dev2","dev0",0))
                      mc("dev0","dev2",false,act("dev0","dev1",0))) .

We repeat the search for attacks starting with iSys3r using this more
restricted attack.

        search iSys3r =>! {c:Conf} such that
            checkRsrc(c:Conf,"dev1","door","unlock") and
            hasGetRsp(c:Conf,"dev0","dev1","getN","lock") .

There are also 4 solutions. In this case 109 states were visited, indicating
that the probability of attacker success is less when it can only make copies
and not change the original message in transit.

##  4 Attack Models

We consider two main classes of attacker: active and reactive. The active
attacker models the attacker envisioned in [4]. Using the formal
representation of an active attacker we replicated versions of the attacks
postulated in [4] (see Appendix 0.B). These attack capabilities (except for
the rerouting extension, A1, see below) simply amplify the effects of an
unreliable transport, dialecting can not mitigate such attacks, and
applications need to deal with the unreliability of the network independently
of attackers.

The reactive attacker can not modify messages in transit (can not drop or
delay these messages). But it can observe, make copies of messages in transit,
and transmit modified copies (redirecting, resending with delay). These
capabilities violate the expected network guarantee that if an endpoint, _ep1_
receives a message with source _ep0_ , then there is a unique previous event
in which endpoint _ep0_ sent that message. They are also capabilities that can
be mitigated by dialecting as we show in Section 8.

The drop capability of scenario iSys1 of Section 3.5 is an example of an
active attack. The replay capability of scenario iSys2 can be used by active
or reactive attackers. The flag in the redirection capability of scenarios
iSys3a and iSys3r determines whether the attack is active (flag is true) or
reactive (flag is false). This is formalized in Section 4.4

###  4.1 Active attacker

A simple active attacker (A0) has a finite set of single actions from the
capability set $\mathtt{CapsA0}=\\{\mathtt{drop},\mathtt{delay(n)}\\}$, where
drop (also called block) prevents a message from being delivered, and delay(n)
delays delivery of a message by $n$ time units. $\mathtt{CapsA1}$ extends
$\mathtt{CapsA1}$ with two additional capabilities
$\\{\mathtt{replay(n)},\mathtt{reroute(tpat,spat,n)}\\}$. Applying replay(n)
makes a copy of the message and transmits it with $n$ added to its delay,
while reroute(tpat,spat,n) modifies the message target and source according to
tpat and spat respectively and adds $n$ to the delay. The pattern tpat is
either a wild card (the empty identifier) which leaves the target unchanged,
or a specific endpoint identifier that replaces the original. Similarly for
the action of spat on the message source.

Informally, these attack capacities can be used to achieve the following basic
effects on CoAP messaging.

  * •

drop can be used to prevent a request (for some action) from being received,
or to prevent a response to some request. In the response case this leaves the
client is a state of not knowing the requested data value, or if the requested
action happened. Note that due to CoAPs reliability mechanism, if the target
message is confirmable, the drop attack will need to be applied to all retries
to succeed.

  * •

The delay of a request, say DM1 from a sequence DM1 ... DM2 until after DM2
can undo the effect of DM2 (door unlock after door lock), or could cause DM2
to happen in the wrong context, for example without lights turned on.

  * •

The delay of a response, say to DM1 delivered as response to a later (blocked)
request DM2 could cause the requesting client to receive out-of-date data, or
to think the action requested by DM2 happened, when only the action of DM1
happened. If DM1, DM2 are GET requests for different resources, say r1 and r2,
the client may interpret the response received as the value of r2 when it is
the value of r1. We note that this only happens with weak implementation of
the token mechanism used to link requests and responses.

  * •

Rerouting a request from ep0 to ep1 to a request from ep0 to ep2 and
(un)rerouting the response from ep2 to be from ep1 causes the client ep0 to
interpret the response as the value of requested resource at ep1 when it is
the value at ep2.

The capability set CapsA0 is sufficient to demonstrate all the vulnerabilities
studied in Appendix 0.B, except for the modified final example that uses
rerouting.

###  4.2 Reactive attacker

A reactive attacker can not modify or block a message in transit. It can
see/copy a message, change the source/target or the delay amount and transmit
the result.

A simple reactive attacker has capabilities in the set $\mathtt{CapsR0}$ that
allows the attacker to make (and edit) one copy of a target message. A given
attacker instance is limited to a finite number of attack attempts.

We also consider a multi action reactive attacker, with capabilities in the
set $\mathtt{CapsR1}$. Using a multi-action, an attacker can make multiple
copies per message, optionally adding to the delay and/or modifying the
message source or target. We allow the attacker to restrict attention to a
given target-source pattern. This mainly improves the attacker efficiency
(reduces the search space) but adds no power at the granularity we consider.
As for the simple reactive attacker, each attacker instance is limited to a
finite set of multi-action capabilities. In a little more detail a multi-
action capability consists of a condition match(tpat,spat) constraining the
set of messages to be attacked, and a finite set of attack actions
act(tpat,spat,n). As before, (tpat,spat) can be wild cards (represented by the
empty string) or specific endpoint identifiers. In the match case a wild card
matches any identifier, while specific identifiers require equality to match.
In the case of act, a wild card means the corresponding target or source is
not changed, while a specific identifier causes the corresponding target or
source to be replaced by the pattern element. The copy is further delayed by
the amount given by the number $n$.

The simple reactive attacker is a special case of the multi-action reactive
attacker, where the condition is restricted to match("","") and the capset
applied to a message is a singleton. Although a reactive attacker can’t block
or delay messages in transit, many of the active attack effects can be
achieved.

Here are examples of what a reactive attacker can do.

  * •

_R1. Undo/revert an action_. Suppose messages M1, M2 PUT different values for
the same resource. The attacker copies M1 and sends the copy with sufficient
delay to arrive after M2, thus overriding the effect of M2. This emulates some
of the reordering capability of the active attacker, leaving the resource in a
state other that what the client planned. It could for example leave a process
running that should have stopped. If the client then starts a process by
PUTting a different resource in the state "on" after sending M2, the new
process may run in an unexpected context.

  * •

_R2. Violate ordering or concurrency constraints._ The attacker observes a
message M1 from ep0 to ep1. It makes copies redirected to ep2 (ep3 …). A
compliant CoAP endpoint ep0 will ignore responses from ep2 (ep3 …). But in the
case of requests causing actions, there will be unexpected actions. For
example, if ep0 is activating ep1, ep2, …, in sequence then ep2, …, will be
acting out of sequence, concurrently with ep1, which could lead to undesired
consequences.

  * •

_R3. Duplication of a process._ Suppose as above ep0 is coordinating a process
by activating ep1, …, epk in sequence, using messages M1, …, Mk. Suppose also
that ep0x, ep1x, …, epkx are a functionally equivalent set of endpoints, say
in a different location. Then the attacker can copy each message and redirect
to ep1x, …epkx.

  * •

_R4. Spoofing (Redirect GET request/response)._ The attacker observes a
message M1 from ep0 to ep1. It makes a copy redirected to ep2. A compliant
CoAP endpoint will reject the response from ep2 (wrong server). If the
attacker also makes a copy of the response, rerouting it to appear to be from
ep1 then ep0 will accept which ever response arrives first. If M1 is a GET
request, then the client may receive the wrong value for the requested
resource.

R1 only needs one capability instance with one action. R2 only needs one
capability instance but with 2 or more actions. R3, R4 need multiple
capability instances, each one needs only a single action.

###  4.3 More possibilities

There are additional, stronger, attack models that could be considered in the
future. One is a reactive attacker with memory. Here the attacker sees all
messages and can remember some. Then at some point the attacker can make
edited copies of some of the messages in its knowledge base and transmit them,
for example to rerun an application sequence either with the original set of
endpoints at a later time, or a separate set (with the same behavior) at some
point. The attacker may use observation of a message occurrence to trigger
actions, or time elapse.

A creative reactive attacker can additionally create new messages and receive
responses, i.e. becoming a rogue endpoint.

###  4.4 Attack-model specification.

As part of the CoAP specification, we specified a general attack framework
where an attacker is endowed with a finite set of capabilities. In this
section we specify specific capabilities corresponding to the active and
reactive attack models discussed above. We define capability constructors and
define their semantics by giving equations for the doAttack function for each
capability. Different models are obtained by constraining the capability
attribute of the attacker agent.

We define a generic capability construction, mc(tpat,spat,active?,acaps).
tpat,spat are target, source patterns used to restrict the set of messages to
be ‘attacked’. acapsis a possibly empty set of actions. Each action,
act(tpat1,spat1,d), causes a copy of the matched message to be made,
transformed, and transmitted. tpat1,spat1 are target, source patterns used to
determine he target and source of the transformed message. If a pattern is ""
the original target or source is used, otherwise the pattern string is used.
The delay d is added to the delay of the original message. If the boolean
active? is true, this is an active capability, and the original message is
removed from the network, only the copies generated by the actions are
transmitted. If active? is false the capability is reactive and the original
message is left in the network to be transmitted as usual. This is formalized
by the following definitions.

        ****      tpat   spat  delay
        op act : String String Nat -> Cap .
        ****     tpat  spat  active? actions
        op mc : String String Bool Caps -> Cap .

The function doAttack defines the semantics of each attack capability. It is
given the attack agent attributes, including its knowledge base of messages
seen, the attack target message, dmsg, and a multi capability. If the target
message matches the selection pattern (using pmatch) then the toSend attribute
is computed and returned along with the knowledge base with the attacked
message added. The toSend attribute includes the attacked message iff the flag
b is false. It also includes the results of applyCaps(dmsg,acaps,mtDM), that
gives the semantics of each action.

        ****                tgt  act   result
        op doAttack : Attrs DMsg Cap -> Attrs .
        ceq doAttack(attrs kb(dmsgs),dmsg,mc(tpat,spat,b,acaps))
               = toSend(dmsgs1) kb(dmsgs dmsg) attrs
         if msg @ n := dmsg
         /\ pmatch(getTgt(msg),tpat)
         /\ pmatch(getSrc(msg),spat)
         /\ dmsgs0 := applyCaps(dmsg,acaps,mtDM)
         /\ dmsgs1 := dmsgs0 (if b then mtDM else dmsg fi) .

If the match fails doAttack returns a result that does not match the
expectation of the attack rule, and the rule does not fire.

The function applyCaps makes a transformed copy of the attacked message for
each action in acaps. The transformation sets the message target and source
according to the action patterns, and increments the delay,

    **** multi cap attack
        op applyCaps : DMsg Caps DMsgS -> DMsgS .
        eq applyCaps(dmsg,mtC,dmsgs) = dmsgs .
        eq applyCaps(msg @ n,act(tpat,spat,n0) acaps,dmsgs) =
              applyCaps(msg @ n,acaps, dmsgs
              (setTgtSrc(msg,tpat,spat) @ (n + n0)) ) .

For early experiments and readability we defined a number of specific (active)
attack capacities. We list them here with their definitions as instances of
the mc construction.

  * •

drop = mc("","",true,mtC) — drop the target message

  * •

delay(n) = mc("","",true,act("","",n)) — add n to the target message delay

  * •

divert(dst0,dst1) = mc(dst0,"",true,act(dst1,"")) — reroute a target message
with destination dst0 to dst1

  * •

undivert(src0,src1) = mc("",src0,true,act("",src1,0)) — make a target message
from src0 appear to be from src1

  * •

replay(n)= mc("","",false,act("","",n)) — replay the target message after
delay n (the original message is delivered as expected)

##  5 Example reactive attacks

This section describes experiments using scenarios illustrating the 4 classes
of reactive attack discussed in Section 4.

###  5.1 R1. Redo/revert an action

.

The R1 scenario is a variant of the attacks on CoAP vulnerabilities Figures
3,4,5,6 (see Section 0.B). The basic requirement is that the door remains
unlocked. The attacker aims for the door to be locked at the end, or before
the optional signal message.

            dev0        eve        dev1
            ----        ---        unlock
             o -PUTNDL-> ----------->
                        @ act("","",5/10)
             o <-------  <-2.04--    o
              ....
             o -PUTNDU-> ----------> o
             o <-------  <-2.04--    o
                        --- PUTNDL-> o  --- attack
        optional
             o -PUTNSO->  ------>    o
             o <-------  <-2.01--    o

The function raR1 generates instances of this scenario. It is parameterized by
the delay between application message sends (mqd:Nat), the bound on pending
acknowledgements that blocks sending an application message (w4b:Nat), the
delay to be added to an replayed message (d:Nat), and a boolean (nso:Bool)
specifying whether the optional "signal" message should be sent.

        op raR1 : Nat Nat Nat Bool -> Conf .
        eq raR1(mqd:Nat,w4b:Nat,d:Nat,nso:Bool) =
         tCS2C(0,0,mkPutN("putNDL","dev1","door","lock") ;
                   mkPutN("putNDU","dev1","door","unlock") ;
                 (if nso:Bool
                  then mkPutN("putNS","dev1","signal","on")
                  else nilAM fi) ,
                  mtR,mqd:Nat,w4b:Nat,
              1,1,nilAM,rb("door","unlock")rb("sig","off"),2,0,
              mc("dev1","dev0",false, act("","",d:Nat))) .

Can the attacker cause the execution to end with the door locked? To check,
search for a terminal state in which "dev1" has resource "door" with value
"lock".

        search {raR1(5,0,10,false)} =>! {c:Conf} such that
            checkRsrc(c:Conf,"dev1","door","lock") .

There are 2 solutions in 101 states visited.

To check that the attacker can shut the door before a later event, we turn on
the signal option and search for a final state where the lock event happened
before the signal event.

        search {raR1(5,0,10,true)} =>! {c:Conf} such that
            checkRsrc(c:Conf,"dev1","door","lock") and
            subLIL(c:Conf,rcvP("dev1","door","unlock") ;
                          rcvP("dev1","door","lock") ;
                          rcvP("dev1","signal","")) .

There are 2 solutions from 231 states visited. The log of the second solution
is the following.

        log(rcvP("dev1","door","lock") ;
            rcvP("dev1", "door", "unlock") ;
            rcvP("dev1", "door", "lock") ;
            rcvP("dev1", "signal", "on"))

If the attacker uses a delay smaller than 10 or larger than 10 there is no
attack (search yields no solution).

###  5.2 R2. Violating ordering or concurrency constraints

In this example, a sequence of $n$ tasks is to be executed one after the
other. The protocol consists of a controller (client endpoint) and n servers
that execute the tasks. A task is initiated when the server receives a PUT
"sig" "on" request and terminates when he server receives a PUT "sig" "off"
request.

        dev0        eve        dev1  ... devk
        ----        ---        off
         o -PUTNon  ----------> o
                     @(cc dev2)> ----->
         o <-------  <-2.04--   o
         ...
         o -PUTNoff  ----------> o
         o <-------  <-2.04--    o
          ....
          ....
         o -PUTNon-> ---------->         o
         o <-------  <-2.04---------     o
         o -PUTNoff-> -----------------> o
         o <-------  <-2.04---------     o

The function iSysX generates instances of the above scenario. n is the number
of servers, d the task duration, and caps the attacker capabilities.

        op iSysX : Nat Nat Caps -> Sys .
        eq iSysX(n,d,caps) = {CnS(n,mkSigAMs(n,d,nilAM),rb("sig","off"),5,0)
          mkAtt(caps) } .

It uses the function CnS(n,amsgl,rbnds,mqd,w4ab) that generates a
configuration with one client and n servers. The client’s application message
list is amsgl and each server has initial resources given by the RMap rbnds.
The client delay between message sends is mqd and it can only send a new
message if there are no more than w4ab confirmable messages awaiting an ACK.

The function mkSigAMs(n,d,nilAM) generates the list of application messages
for the client to send to control the execution. The list consists of pairs

       mkPutN("putN","dev" + string(j,10),"sig","on") ;
       mkPutN("putN","dev" + string(j,10),"sig","off") .

for $j\in[1,n]$ separated by a delay of d.

We consider three levels of attacker capability. Level $j$ (caps-j) looks for
messages from "dev0" to "dev1" and immediately (additional delay 0) sends a
copy to "dev2" … "dev1+j".

        ops caps-1 caps-2 caps-3 : -> Caps .
        eq caps-1 = mc("dev1","dev0",false,act("dev2","",0)) .
        eq caps-2 = mc("dev1","dev0",false,
                       act("dev2","",0) act("dev3","",0)) .
        eq caps-3 = mc("dev1","dev0",false,
                       act("dev2","",0) act("dev3","",0)
                       act("dev4","",0)) .

We consider two attacks that violate the property that the tasks do not
interleave, by starting a task on "dev-k+j" before the task on "dev-k"
completes. One check for violation is that the number of devices with resource
binding rb("sig","on") is great than 1. The function epswrb(conf,rbnds)
returns the number of servers with resource map containing a match for rbnds
is used for this check. Alternately we can check for executions in which
"devj" receives an "on" signal, and "devj+1" receives the "on" signal before
"devj" receives the "off" signal. This is done using the subLI function. Using
caps-1 can the attacker can cause at least 2 simultaneous tasks executions?

        search iSysX(3,0,caps-1) =>+ sys:Sys such that
            size(epswrb(sys:Sys,rb("sig","on"))) > 1 .

There are 132 solutions from 767 states visited.

Raising the bar we ask if using caps-2 can the attacker cause 3 or more tasks
to execution simultaneously.

        search  iSysX(3,0,caps-2) =>+ sys:Sys such that
            size(epswrb(sys:Sys,rb("sig","on"))) > 2 .

There are 182 solutions among 721 states visited.

We can also ask if the attacker can cause dev2 to start before dev1 finishes.

        **** attack 3 dev2 starts before dev1 finishes
        search iSysX(3,0,caps-2) =>+ {c:Conf} such that
            subLIL(c:Conf, rcvP("dev1","sig","on") ;
                           rcvP("dev2","sig","on") ;
                           rcvP("dev1","sig","off")) .

There are 342 solutions from 3598 states visited. The log for the last
solution is

       log(rcvP("dev3", "sig", "on") ; rcvP("dev1", "sig", "on") ;
        rcvP( "dev2", "sig", "on") ; rcvP("dev1", "sig", "off") ;
        rcvP("dev2", "sig", "on") ; rcvP("dev2", "sig", "off") ;
        rcvP("dev3", "sig", "on") ; rcvP( "dev3", "sig", "off")).

Finally, we ask if the attacker can cause dev2 to start before dev1 finishes
and dev3 to start before dev2 finishes.

        search iSysX(3,0,caps-2) =>+ {c:Conf} such that
            subLIL(c:Conf, rcvP("dev1","sig","on") ;
                           rcvP("dev2","sig","on") ;
                           rcvP("dev1","sig","off")) and
            subLIL(c:Conf,rcvP("dev2","sig","on") ;
                          rcvP("dev3","sig","on") ;
                          rcvP("dev2","sig","off")) .

There are 62 solutions among 3594 states visited. The log for the last
solution follows.

      log(rcvP("dev1", "sig", "on") ; rcvP("dev2", "sig", "on") ;
      rcvP( "dev3", "sig", "on") ; rcvP("dev1", "sig", "off") ;
      rcvP("dev2", "sig", "on") ; rcvP("dev2", "sig", "off") ;
      rcvP("dev3", "sig", "on") ; rcvP( "dev3", "sig", "off"))

###  5.3 R3 Duplication of a process.

IoT systems may be replicated, for example running the same protocol in
multiple smart rooms, or in a manufacturing setting multiple instances of a
manufacturing step.

        dev0        eve        dev1 dev2 dev3 dev4 dev5 dev6
        ----        ---        ---
         o -PUTNgo   @ ---------> o
                     o -(cc dev4)-------------> o
         o <-------  <-2.04--   o
                                     <-2.04--   o
         o -PUTNgo-> @-------------->  o
                     o -(cc dev5) ---------------->  o
         o <-------  <-2.04---------  o
                                           <-2.04--  o
         o -PUTNgo   @ -------------------> o
                     o -(cc dev6)----------------------> o
         o    <-------  <-2.04---------    o
                                                <-2.04-- o

Here the label (cc dev4) indicates the attacker coping a message to a
different device.

The function iSysY generates example scenarios with one client (controller)
and 2 sets of n servers. The client will send a PUT message to set the "sig"
resource "go" to each server in the first set of servers. Each server
initially has resource map rb("sig","off").

        op iSysY : Nat  Caps -> Sys .
        eq iSysY(n,caps) =
              {CnS(2 * n,mkGoAMs(n,nilAM),rb("sig","off"),5,0)
               mkAtt(caps)  log(nilLI)} .

We consider scenarios with $n=2$ and $n=3$ and ask whether the attacker can
drive a the second set of devices, either concurrently or following the first.
The attacker capabilities for the two scenario sizes are defined as follows,
parameterized by the amount to delay message copies.

        ops caps2-2 caps3-3 : Nat -> Caps .
        eq caps2-2(d) =
          mc("dev1","dev0",act("dev3","dev0",d))
          mc("dev2","dev0",act("dev4","dev0",d)) .
        eq caps3-3(d) =
          mc("dev1","dev0",act("dev4","dev0",d))
          mc("dev2","dev0",act("dev5","dev0",d))
          mc("dev3","dev0",act("dev6","dev0",d)) .

The four search commands, results (with witness log) are as follows.

         *** search for duplicate 2 server process running concurrently
        search iSysY(2,caps2-2(0)) =>! {c:Conf} such that
          subLIL(c:Conf, rcvP("dev3","sig","") ; rcvP("dev4","sig","")) and
           subLIL(c:Conf, rcvP("dev3","sig","") ; rcvP("dev2","sig","")) .

There are 16 solutions among 534 states visited.

        log(rcvP("dev3", "sig", "go") ; rcvP("dev1", "sig", "go") ;
            rcvP( "dev4", "sig", "go") ; rcvP("dev2", "sig", "go"))

        *** search for duplicate 2 server process the second after the first
        search iSysY(2,caps2-2(15)) =>! {c:Conf} such that
          subLIL(c:Conf,rcvP("dev3","sig","") ;  rcvP("dev4","sig",""))
          and subLIL(c:Conf,rcvP("dev2","sig","") ; rcvP("dev3","sig","")) .

There are 4 solutions among 179 states visited.

        log(rcvP("dev1", "sig", "go") ; rcvP("dev2", "sig", "go") ;
            rcvP( "dev3", "sig", "go") ; rcvP("dev4", "sig", "go"))

         **** search for duplicate 3 server process the second after the first
        search iSysY(3,caps3-3(0)) =>! {c:Conf} such that
          subLIL(c:Conf, rcvP("dev4","sig","") ;
            rcvP("dev5","sig","") ; rcvP("dev6","sig","")) and
          subLIL(c:Conf, rcvP("dev1","sig","") ;
            rcvP("dev4","sig","") ; rcvP("dev2","sig","")) and
          subLIL(c:Conf, rcvP("dev2","sig","") ;
            rcvP("dev5","sig","") ; rcvP("dev3","sig","") ;
            rcvP("dev6","sig","")) .

There are 8 solutions among 2845 states visited.

        log(rcvP("dev1", "sig", "go") ; rcvP("dev4", "sig", "go") ;
            rcvP( "dev2", "sig", "go") ; rcvP("dev5", "sig", "go") ;
            rcvP("dev3", "sig", "go") ; rcvP("dev6", "sig", "go"))

        **** search for duplicate 3 server process the second after the first
        search iSysY(3,caps3-3(15)) =>! {c:Conf} such that
            subLIL(c:Conf, rcvP("dev4","sig","") ;
                rcvP("dev5","sig","") ; rcvP("dev6","sig","")) and
            subLIL(c:Conf, rcvP("dev3","sig","") ; rcvP("dev4","sig","")) .

There are 8 solutions among 683 states visited. The log of the last solution
is the following.

       log(rcvP("dev1", "sig", "go") ; rcvP("dev2", "sig", "go") ;
           rcvP( "dev3", "sig", "go") ; rcvP("dev4", "sig", "go") ;
           rcvP("dev5", "sig", "go") ; rcvP("dev6", "sig", "go"))

###  5.4 R4. Spoofing (Redirect GET request/response)

Although a reactive attacker can not redirect a message in transit, as the
active attacker can (see Section 0.B.6), it can make a copy and direct it to a
different server. The reactive attacker also has to make a copy of the
response from that server to appear to come from the original server. Thus the
client will receive 3 responses. They can arrive in any order. The client will
ignore the one from the alternate server, and its a race between the two
messages apparently from the intended server.

            dev0      eve       dev1     dev2
            ----      ---      unlock    lock
          o -GETN(1)-->@------->  o
          |            o copy(cc dev2)  -> o
          o   <---unlock---      o
          o            @    <---lock---    o
          o <- (cc from dev1)

The function iSySZ(mqd:Nat,w4b:Nat) generates instances of the redirection
attack scenario. It is parameterized by the usual congestion control
arguments.

        op iSySZ : Nat  Nat -> Sys .
        eq iSySZ(mqd:Nat,w4b:Nat) =
             {tCS3C(0,0,mkGetN("getN0","dev1","door"),
                       mtR,mqd:Nat,w4b:Nat,
                  1,1,nilAM,rb("door","unlock"),5,0,
                  2,2,nilAM,rb("door","lock"),5,0,
                  mc("dev1","dev0",false,act("dev2","",0))
                  mc("dev0","dev2",false,act("","dev1",0)) )
                  log(nilLI) }  .

To demonstrate attacks we search for final states in which the client has
received a "lock" response to the GET request while "dev1" has the "door"
resource bound to "unlock".

        search iSySZ(5,0) =>! {c:Conf} such that
          hasGetRsp(c:Conf,"dev0","dev1","getN0","lock") and
          checkRsrc(c:Conf,"dev1","door","unlock") .

There are 4 solutions among 109 states visited.

##  6 Dialect functions

Dialects using a moving target strategy must synchronize on the choice of
lingo. In the case of reliable transport this is often done using time
synchronization. 222Even with reliable transport, attackers may drop or
reorder messages, which can complicate lingo synchronization.

For protocols, like CoAP, running on unreliable transport, the notion of
current lingo (or lingo parameters) or lingo (parameters) being no longer
valid, seems problematic. In principle there is no bound on the delay of a
message, and missing messages or out of order messages which are common, make
guaranteeing that a receiver can determine the correct lingo to decode a
dialected message a challenge. Failure would mean dropping a message that
should have been delivered.

We take inspiration from security protocol designs that use message counters
(one counter for each communication pair and direction) for replay prevention
and/or detection. These counters appear in the clear in messages making
synchronization simpler. We have to be careful that these counters don’t leak
enough information to be useful to an attacker.

For the CoAP dialect specification we propose a scheme of three functions:

  * •

$g:\mathtt{String}\times\mathtt{Nat}\times\mathtt{Nat}\longrightarrow\mathtt{String}$
– a generator of (pseudo) randomness. The first argument is a seed, the second
specifies the output length, and the third argument is the index into the
sequence generated by $g$. Thus $g(\mathtt{seed},\mathit{k},\mathit{ix})$ is
the _ix_ -th (pseudo) random string (of length _k_) initialized seed.

  * •

$f_{1}:\mathtt{String}\times\mathtt{Content}\times\mathtt{Nat}\longrightarrow\texttt{DCBits}$
– the obfuscator/encoder. The first argument is the source of randomness, the
second argument is a message content and the third an index (a natural
number).

  * •

$f_{2}:\mathtt{String}\times(\texttt{DCBits}\times\mathtt{Nat})\leadsto\texttt{ContentNat}$
– the de-obfuscator/decoder. The first argument is again the source of
randomness and the second argument is a pair consisting of the encoded message
content and the lingo index.

We can think of a dialect given by the above three functions as having a
single parameterized lingo, or as having a family of lingos indexed by the
third argument to $f1$.

There are two important properties of these functions. First, $f_{2}$ recovers
the original content encoded by $f_{1}$, using random generator $g$

$f_{2}(grand,\\{f_{1}(grand,\\{\mathtt{content},ix\\}\\}),ix)=\\{\mathtt{content},ix\\}.$

where _grand_ is generated independently by each endpoint in a communicating
pair as $g(\mathtt{seed},k,ix)$ where seed is a shared secret. Second, if the
encoded content or index are modified, decoding will fail. Letting
$f_{1}(\mathit{grand},\\{\mathit{content},\mathit{ix}\\})=\mathit{dcbits}$,
$\mathit{dcbits1}\neq\mathit{dcbits}$, and $\mathtt{ix1}\neq\mathtt{ix}$ then

$f_{2}(grand,\\{\mathtt{dcbits1},ix\\})=\\{\mathtt{content1},ix\\}.$

and

$f_{2}(grand,\\{\mathtt{dcbits},ix1\\})==\\{\mathtt{content1},ix1\\}.$

with $\mathtt{content}\neq\mathtt{content1}$ and $\mathtt{content1}$ is
recognized as ill-formed. Alternately, $f_{2}$ could directly return an
indication of failure, but only if the input is a correctly transformed
content.

Starting the enumeration of random strings with a secret seed is important. An
attacker may well know the three functions. If he can guess the message
content, then he can compute $f_{2}(g(ix,k),{\mathit{dcbits},ix}))$. We claim
that with a secret seed exposing _ix_ doesn’t really expose much useful
information and avoids the need for the receiving wrapper to guessing the
_ix_.

An alternative for generating the sequence of random strings is
$g^{ix(}seed,k)$ $seed_{0}=g(seed,k,0)$ and $seed_{j+1}=g(seed_{j},k,0)$. If
the attacker learns the value of $g(seed_{j},k,0)$ (for example if $f_{1}$
uses xor and the attacker can guess the content of some message) then the
attacker can compute $g(seed_{j+n},k,0)$.

What can the attacker learn given the method of generating a sequence of
pseudo random strings/bits? Suppose the attacker can derive
$g(\mathit{seed},k,ix)$, $g(\mathit{seed},k,ix+1)$, …,
$g(\mathit{seed},k,ix+n)$ from transmitted messages. It should be HARD to
predict the next value $g(\mathit{seed},k,ix+1)$ from $g(\mathit{seed},k,ix)$.

If the attacker knows $g$ but not the secret string $\mathit{seed}$ he can run
$g$ on sample seeds with the known indexes. If seed is 128 bits with non-0 in
the top 64 bits it can take a long time to check the seed. If he can do
$10^{12}$ samples per day it could take $10^{6}$ days to find the seed.

##  7 Specification of a CoAP dialect wrapper

To specify a dialect wrapper for CoAP messaging we need to specify the data
type of dialected messages, the three functions described in Section 6, the
structure of wrapped CoAP agents (subsection 7.1), and the rules for sending
and receiving messages by the wrapped agents (Subsection 7.2). Towards
dialects as a theory transformation, in subsection 7.3 we define operations D
and UD. D takes an inital system configuration and produces the corresponding
dialected configuration. UD extracts the underlying CoAP system configuration
from a dialected configuration. Using these functions, rewrite and search
commands for a CoAP scenario can be automatically transformed to rewrite and
search commands for the corresponding dialected scenario (Subsection 7.4).

###  7.1 Dialect messages and configurations

A dialected message has a target and a source (sort String as for normal
messages) and a dialect encoded content (sort DContent). The message
constructor is overloaded to construct dialected messages.

        op m : String String DContent -> Msg .

A term of sort DContent is a pair constructed by the operator dc

        op dc : DCBits Nat -> DContent [ctor] .

where the sort DCBits is an opaque sort whose structure is not further
specified. We also define the sort ContentNat to be pairs constructed from
ordinary content and a natural number.

        op ‘{_‘,_‘} : Content Nat -> ContentNat [ctor] .

The three dialect functions of Section 6 are specified as follows:

        op g : String Nat Nat -> String .
        op f1 : String ContentNat -> DCBits .
        op f2 : String DContent  ~> ContentNat .
        eq f2(g(rand,k,ix),dc(f1(g(rand,k,ix),{content,ix}),ix))
              = {content,ix} .

The partial arrow $\verb|~>|$ used in the declaration of f2 means that the
result of applying f2 to a modified encoding will be of kind ContentNat, but
not of sort ContentNat. This allows to detect modifications in the dialected
content.

As described in [2] we represent a dialect wrapper by a meta-agent that has
the same identifier as the wrapped agent, a conf attribute that encapsulates
the base agent and its network stub, and additional attributes for managing
dialect transformations.

        *** dialected endpoint
        [eid | conf([eid | devattrs] net), ddevattrs]

We refer to the encapsulated network as the internal network and the network
at the level of meta entities as the external network.

The additional attributes for a dialect meta endpoint include:

  * •

used(umap) — a map from endpoint ids to sets of lingo indices already received
from the identified endpoint.

  * •

toRcv(dmsgs) — holds the result of decoding– the original message or the empty
(delayed) message set, if decoding fails

  * •

seedTo(eid,str) – the shared secret seed for sending to eid

  * •

seedFr(eid,str) – the shared secret seed for receiving from eid

  * •

ixCtr(eid,nat) — the counter for generating lingo indices for messages to
endpoint named eid

  * •

randSize(k) – the size of generated (pseudo) random strings

###  7.2 Dialect Rules

There are two rules to specify dialect behavior. The rule labeled ddevsend
handles applying a dialect lingo to a message sent by an endpoint and putting
it in the global network. It selects a message in the internal network sent by
the wrapped entity, calls applyDialect, and puts the resulting dialected
message in the external network.

        crl[ddevsend]:
          [epid | conf([epid  | devatts ] net(dmsgs0,dmsgs1)) dattrs ]
          net(ddmsgs0,ddmsgs1)
        =>
          [epid | conf([epid  | devatts ] net(mtDM,dmsgs) ) dattrs1 ]
          net(ddmsgs0 ddmsg,ddmsgs1)
        if dmsgs (msg @ n) := dmsgs0 dmsgs1
        /\ getSrc(msg) = epid
        /\ toSend(ddmsg) dattrs1 := applyDialect(dattrs,msg @ n) .

The function applyDialect looks up seed, random size, and current index values
in the attribute set dattrs. It computes the generated string grand using the
dialect function g, and then applies the encoding function f1 to this string,
the message content and the index and constructs the dialected message msgd to
be sent on the external network. It also increments the index counter for the
message target

        ceq applyDialect(dattrs,msg @ n) =
             incIxCtr(dattrs,dst,1) toSend(msgd @ n)
        if m(dst,src,content) := msg
        /\ rand := getSeedTo(dattrs,dst)
        /\ rsize := getRandSize(dattrs)
        /\ ix := getIxCtr(dattrs,dst)
        /\ grand := g(rand,rsize,ix)
        /\ dcbits := f1(grand,{content,ix})
        /\ msgd := m(dst,src,dc(dcbits,ix)) .

The rule labeled ddevrcv handles receipt of a dialected message. It selects a
message with 0 delay and target the wrapped entity an calls decodeDialect. If
decoding produced a message, the rule calls the rcvMsg directly since the
result may include a logging attribute that needs the full configuration to
process, which the base CoAP receive rule would not have.

        crl[ddevrcv]:
        {[epid | conf([epid | devatts ] net(dmsgs0,dmsgs1))
                 dattrs ]
          net(ddmsgs0,ddmsgs1 msgd @ 0) conf}
        =>
        {[epid | conf([epid | devatts2 ]
                      net(dmsgs0 dmsgs2,dmsgs1))
                dattrs1 ]
          net(ddmsgs0,ddmsgs1)  conf1}
        if getTgt(msgd) == epid
        /\ toRcv(dmsgs) dattrs1 := decodeDialect(dattrs,msgd)

        /\ toSend(dmsgs2) devatts1 :=
            (if dmsgs :: DMsg
             then rcvMsg(epid, devatts, DMsg2Msg(dmsgs))
             else toSend(mtDM) devatts
             fi)
        /\ conf1 := doLog(conf,devatts1)
        /\ devatts2 := clearToLog(devatts1) } .

In addition to the dialect send and receive rules, the auxiliary functions mte
and passtime used by the rule labeled tick are extended to account for the
nesting of configurations. If there are messages in the local network then
they need to be processed before time can pass. These messages will be
messages from epid the should be dialected and placed in the global network.

      eq mte(atts conf([epid | devattrs] net(dmsgs0,dmsgs1)),ni)
       = (if dmsgs0 dmsgs1 =/= mtDM
          then 0
          else mte(atts, mte(devattrs,ni))
          fi) .

Similarly, the effect of passing time is simply propagated to the encapsulated
agent, ignoring the local network element.

      eq passTime(conf([epid | devattrs] net(dmsgs0,dmsgs1)),nz)
       =
      conf([epid | passTime(devattrs,nz,mtA)]  net(dmsgs0,dmsgs1)) .

###  7.3 CoAP dialect transform

As a step towards realizing the dialects as theory transformations, we define
a function D that maps a term representing an initial system configuration to
its dialected form. D calls the auxilliary function DX with the system term to
transform and the set of ids of non-attacker endpoints computed by getIds. The
function DX uses DAs to transform the individual agents of the configuration
aconf, and adds the initial network element. The argument "xxxx" of DAs is
used to construct abstract representations of the pairwise shared secrets. The
last argument of DAs is a configuration accumulator. We also define a partial
inverse, UD, to the dialect transform D. The partial inverse is only
meaningful when applied to systems with no dialected messages pending. It is
generally applied only to inital or terminal states, which have empty network
elements.

        op D : Sys -> Sys .
        op DX : Sys Strings -> Sys .

        eq D(sys) = DX(sys,getIds(sys)) .
        ceq DX({aconf net(mtDM,mtDM)},eids) =
           { daconf net(mtDM,mtDM) }
        if daconf := DAs(aconf,eids,"xxxx",mt) .

The function DAs applies the local agent transform DA to each agent with
identifier in the set eids and leaves any other agent (i.e. an attacker)
unchanged. The function DA does the actual wrapping of a protocol
role/endpoint producing a meta-agent with the same identifier and a conf
attribute containing the original agent with its local network stubb. The
attributes of the meta-agent wrapper consist of the attributes,
sharedDialectAttrs that are the same for all wrappers, a set of seed
attributes, a pair for each possible communication partner (network link) and
a set of index attributes, one for each possible communication partner.

        op DA : Agent Strings String -> Agent .
        ceq DA([eid | devatts],eids,str) =
            [eid | conf([eid | devatts]
                        net(mtDM,mtDM)) ddevatts]
        if ddevatts := sharedDialectAttrs
                       mkSeeds(eid,eids,str,mtA)
                       mkIxCtrs(eids,mtA) .

To accomodate general scenarios, we assume any pair of non-attacker agents
might communicate. When called from DX the str will be "xxxx" and result of
mkSeeds will be a set of attribute pairs seedFr(eid,"xxxx" + eid1 + eid) and
seedTo(eid,"xxxx" + eid + eid1) for each eid in eids. Similarly the function
mkIxCtrs produces an attribute ixCtr(eid,0) for each eid in eids.

As an example, consisder the initial system

    initSys =
     { net(mtDM, mtDM)
      ["dev0" | w4Ack(mtDM) w4Rsp(mtM) ...
                rsrcs(mtR) ctr(0)
                sendReqs(...)  config(...) sndCtr(0)]
      ["dev1" | w4Ack(mtDM) w4Rsp(mtM) ...
                rsrcs(rb("door", "unlocked")) ctr(0)
                sendReqs(nilAM) config(...) sndCtr(1)]
      ["eve" | kb(mtDM) caps(drop)]}

Its dialect transform, D(initSys) is

    { net(mtDM, mtDM)
      ["dev0" | conf(net(mtDM, mtDM)
              ["dev0" | w4Ack(mtDM) w4Rsp(mtM) ...
                        rsrcs(mtR) ctr(0)
                        sendReqs(...) config(...) sndCtr(0)])
        used(mtU) randSize(128)
            seedTo("dev1", "xxxxdev1dev0")
            seedFr("dev1", "xxxxdev0dev1") ixCtr("dev1", 0)]
      ["dev1" | conf(net(mtDM, mtDM)
                ["dev1" | w4Ack(mtDM) w4Rsp(mtM) ...
                         rsrcs(rb("door", "unlocked"))
                         ctr(0) sendReqs(nilAM) config(...) sndCtr(1)])
        used(mtU) randSize(128)
            seedTo("dev0", "xxxxdev0dev1")
            seedFr("dev0","xxxxdev1dev0") ixCtr("dev0", 0)]
      ["eve" | kb(mtDM) caps(drop)]}

The function UD extracts CoAP endpoints from conf attributes and passes other
configuration elements unchanged

    op UD : Sys -> Sys .
    op UDX : Conf Conf -> Conf .
    eq UD({conf}) = {UDX(conf,mt)} .
    eq UDX([eid | conf([eid | devatts] conf1) ddevatts] conf0,
                   uconf) =
          UDX(conf0, uconf [eid | devatts]) .
    eq UDX(conf0, uconf) = uconf conf0 [owise] .

    **** produce configurations by omitting the final system construction
    op UDC : Conf -> Conf .
    **** eq UDC(conf net(dmsgs0,dmsgs1)) = UDX(conf,mt) .
    eq UDC(conf) = UDX(conf,mt) .

######  Definition 2 (Initial dialected CoAP configuration)

An initial dialected CoAP system, dsysI, is the result of transforming an
initial CoAP system sysI

$\mathtt{dsysI}=\mathtt{D}(\mathtt{sysI}).$

###  7.4 Dialected CoAP Scenarios

As we prove in Appendix 0.C dialecting mitigates attacks of a reactive
attacker. To illustrate this claim we can lift the scenarios for reactive
attacks of Section refsec:reactive-attacks to dialected scenarios and lift the
search for attacks to the dialected situation. To do this we apply the
transform D to the initial system term and apply the inverse (on
configurations) UDC to uses of the search target pattern c:Conf in the search
condition. For example in the R1 attack (the attacker locks the door after the
client has unlocked it) example the search

        search({raR1(5,0,10,false)}) =>! {c:Conf} such that
            checkRsrc(c:Conf,"dev1","door","lock") .

when lifted to a dialected system becomes

        search D({raR1(5,0,10,false)}) =>! {c:Conf} such that
            checkRsrc(UDC(c:Conf),"dev1","door","lock") .

There are 2 solutions in 101 states visited in the original search while no
solution is found among 121 states visited in the search for the dialected
system.

As one more example recall the example of R2 type attacks, where a client is
invoking server proceses one at a time and the attacker manages to start some
servers early, thus having more than one server active concurrently. The
original search is

        search iSysX(3,0,caps-1) =>+ sys:Sys such that
              size(epswrb(sys:Sys,rb("sig","on"))) > 1 .

and its dialected form is

        search D(iSysX(3,0,caps-1)) =>+ sys:Sys such that
            size(epswrb(UD(sys:Sys),rb("sig","on"))) > 1 .

There are 132 solutions from 767 states visited in the undialected scenario
while in the dialected case no solution is found in 553 visited.

The remaining cases are similar.

##  8 Dialect properties

Here we consider the relation of traces of an initial system
$\mathtt{sysI}=\\{\mathtt{confI}\\}$ running the CoAP messaging protocol
specification to traces of the corresponding dialected system D(sysI) in the
presence of the different attack capabilities, including mtC (none). Although
CoAP is designed to run over UDP (unreliable transport) we also consider the
case of reliable transport. We note that the specified dialect wrapper (i)
drops messages that fail decoding, and (ii) has a notion of used lingo
parameter such that messages with previously used lingo parameters are
dropped. We consider instances of the following relation:

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))~{}\sim?~{}\mathtt{mkISys}(\mathsf{att}(c))$

where $\mathtt{mkISys}(\mathsf{att}(c))$ denotes an initial system
configuration with endpoints in their inital state, an empty network, and an
attacker with capabilities $c$. The question is what is $\sim?$. One candidate
is stuttering bisimulation ($\approx$). As a second candidate we say that a
dialect $\mathsf{D}$ is _strongly attack reducing_ for attack messages M iff
for any trace of $\mathtt{mkISys}(\mathsf{att}(c))$ if an attacker generated
message M is first delivered at step $j$ then there is a corresponding trace
of $\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))$ with M is delivered at the
corresponding step $j^{\prime}$ and is dropped. In some more detail we define

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))\precsim[rcv[M]]~{}\mathtt{mkISys}(\mathsf{att}(c))$

to mean any trace from the lhs without the an attacker event has a
corresponding trace from the rhs, and dually. If $\tau$ is a trace of either
side with an event $\mathtt{rcv}[M]$ the first occurrence of receive of an
attacker produced message, then the lhs trace drops the offending message and
any corresponding rhs trace processes the message and possibly diverges from
the lhs. In the cases considered this relation becomes

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{drop})).$

#### Dialect basic correctness.

In the absence of attacks in a reliable or unreliable network the dialect
wrapper simply encodes messages sent by an endpoint, and decodes them before
passing them to the receiver endpoint. Thus a dialected CoAP system is
stuttering bisimilar to the original system.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{mtC})))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{mtC}))$

For proof see Appendix 0.C Theorem 0.C.1.

#### Dialecting over unreliable transport.

Here we consider the question: running over an unreliable transport, how do
$\mathsf{D}(\mathtt{mkISys})$ in the presence of a given attack capability,
$\mathtt{cap}$, and $\mathtt{mkISys}(\mathsf{att}(c))$ relate?

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))~{}\sim?~{}\mathtt{mkISys}(\mathsf{att}(mtC))$

The following is an informal analysis giving the intuitions. For proof see
Appendix 0.C Theorem 0.C.2.

  * (i)

$c=\mathtt{drop}$ or $c==\mathtt{delay}(n)$. In this case $\sim?$ is
stuttering bisimilar since the network can drop or delay messages as well!
What the attacker can do is significantly change the probability profile of
drops/delays.333This suggests a stronger relation than bisimilarity might be
useful

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))\approx\mathtt{mkISys}(\mathsf{att}(mtC))$

  * (ii)

$c=\mathtt{divert}$ (edit source, or destination or both). Assuming each
communicating pair in the dialected system has a unique shared secret,
$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))$ will drop the diverted message,
thus making it look like a network drop. Without dialecting the new receiver
might handle the diverted message, possibly causing problems, for example the
temperature example (reading room vs oven temperature).

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{divert})))\approx\mathtt{mkISys}(\mathsf{att}(mtC))$

Note that if all three endpoints involved share the same secret (the initial
seed) then the dialect layer will not detect the redirection.

  * (iii)

$c=\mathtt{replay}(n)$. There are two cases: (a) the original message wasn’t
delivered—the replay appears as a delay or resend and won’t be dropped by the
wrapper and will correspond to a trace on the rhs where the original message
was delivered; (b) the original message was delivered—the replay is
dropped.444Note that if the lingo policy is to allow a parameter to be used 2
or more times before rejecting, then the second use of a parameter may be
rejected after a replay causing dialecting to be complicit in the attack. Thus
we chose a single-use policy.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{replay}(n))))\approx\mathtt{mkISys}(\mathsf{att}(mtC))$

  * (iv)

$c=\mathtt{edit}$ a message component (not implemented yet). There are two
cases:

    * (iv.a)

the message component is dialected, assuming the attacker can’t break the
dialecting, undialecting will fail and the message will be dropped.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(a))))\approx\mathtt{mkISys}\mathtt{mkISys}(\mathsf{att}(mtC))$

    * (iv.b)

the message component is not dialected, then dialecting doesn’t change
anything

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(b))))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(b)))$

  * (v)

$c=\mathtt{create}$ (message creation not implemented yet). Assuming the
attacker can’t break the dialecting, undialecting will fail and the message
will be dropped

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(\mathtt{create}))))\approx\mathtt{mkISys}(\mathsf{att}(mtC))$

#### Dialecting over reliable transport.

Now we consider the question: In the presence of given attack capability, $c$,
running over a _reliable_ transport, how do
$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))$ and
$\mathtt{mkISys}(\mathsf{att}(c))$ relate?

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(c)))~{}\sim?~{}\mathtt{mkISys}(\mathsf{att}(c))$

  * (i)

$c=\mathtt{drop}$ or $c==\mathtt{delay}(n)$. Dialecting doesn’t affect drop or
delay attacks.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{drop},\mathtt{delay}(n))))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{drop},\mathtt{delay}(n)))$

  * (ii)

$c=\mathtt{divert}$ (edit source, or destination or both of message M. The
dialect wrapper will drop a diverted message, as it is coded with the wrong
secret. The base CoAP receiver may process the message.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{divert})))~{}\precsim[rcv(M)]~{}\mathtt{mkISys}(\mathsf{att}(\mathtt{divert}))$

  * (iii)

$c=\mathtt{replay}(n)$ of M. Note that with reliable transport, the original
message will have been delivered. The dialect wrapper will drop the message,
as its lingo (parameter) is already used.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{replay}(n))))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{mtC}))$

    * (iii.a)

$n$ is small enough that $M$ is delivered within the original message’s
(identifier) lifetime , the CoAP receiver may repeat the original response,
but will not process any message requested actions.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{replay}(na))))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{replay}(na)))$

    * (iii.b)

$M$ is delivered after the original message’s lifetime expires. In this case
the CoAP receiver will process the replay.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{replay}(nb))))\precsim[\mathtt{rcv}(M)]~{}\mathtt{mkISys}(\mathsf{att}(\mathtt{replay}(nb)))$

  * (iv)

$c=\mathtt{edit}$ a component if message M (not implemented yet). event =
rcv(M), There are two cases:

    * (iv.a)

the edited message component is dialected. Assuming the attacker can’t break
the dialecting, undialecting will fail and the message will be dropped, while
the undialected system will attempt to process the message.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(a))))\precsim[rcv[M]]~{}\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(a)))$

    * (iv.b)

the message component edited is not dialected, then dialecting doesn’t change
anything.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathsf{att}(\mathtt{edit}(b)))))\approx\mathtt{mkISys}(\mathsf{att}(\mathtt{edit}(b)))$

  * (v)

$c=\mathtt{create}$ message M. Assuming the attacker can’t break the
dialecting, the dialect wrapper will drop the message, but
$\mathtt{mkISys}(\mathsf{att}(\mathtt{create}))$ will attempt to process it.

$\mathsf{D}(\mathtt{mkISys}(\mathsf{att}(\mathsf{att}(\mathtt{create}))))\precsim[rcv[M]]~{}\mathtt{mkISys}(\mathsf{att}(\mathtt{create}))$

##  9 Related Work

The work most closely related to the present work is [2], which we will refer
to as ESORICS23 in the following. Complimentary work on dialects is discussed
briefly in Section 2. We refer to ESORICS23 for a more complete review of
previous work on dialects.

ESORICS23 addresses three key aspects of dialects: synchronization mechanisms;
protocol and lingo genericity; and attack model vs dialect choice. It also
defines taxonomies for key dimensions of a dialect.

A general framework is proposed defining notions of dialect and lingo as
(parameterized) transformations on protocol theories, where a protocol theory
is a generalized actor theory with a sort Configuration and a constant
initConf of sort Configuration, representing the initial protocol system
state. A lingo defines a pair $f,g$ of parameterically inverse functions for
obfuscating and deobfuscating protocol messages: $g(f(m,p),p)=m$. A lingo
transforms a protocol theory to a new protocol theory by adding the function
definitions. The dialect transform operates on the protocol theory together
with the lingo transformed theories. In the resulting theory, protocol objects
are wrapped with dialect meta objects with the same identifier and rules are
provided for sending/receiving messages at the dialect level.

The CoAP Dialect presented in Section 7 has one lingo, defined in the module
COAP-DIALECT-LINGOS which extends the functional part of the CoAP
specification. The CoAP dialect is specified as the result of the transform,
by including the lingo and protocol modules and adding rules for receiving and
sending messages. The initial configurations are defined in protocol and
dialect test modules, where dialected configurations are obtained as in the
ESORICS23 case by wrapping protocol objects by meta objects.

We note that the definition of protocol theory with a fixed initial
configuration doesn’t quite work if you want it to support a variety of
scenarios. For example MQTT and CoAP support networks of almost arbitrary size
and topology. One can define a protocol theory for each scenario of interest,
with a dialect being generic with respect to the initial configuration. But
this looses the information that all the scenarios use the same rules and data
types thus seems not quite satisfactory. Perhaps a notion of scenario
constructor parameterized by a network topology and a means of specifying
initial shared secrets could be useful. Also, configurations are ‘open’ in the
sense that each actor or subset of actors and messages is a configuration and
a configuration is a subconfiguration of infinitely many larger
configurations. In most cases rewrite rules apply to a subconfiguration, for
example an actor and a message, independent of what configuration it is part
of. However, some rules need to know that they are seeing the full
configuration. This can be achieved by introducing the notion of system as an
encapsulated configuration. The question is whether the notion of system
should be a first class concept for protocols and dialect transformations.

#### Synchronization mechanisms.

Synchronization can happen on different time scales: when the set of lingos in
use changes, and when current lingo parameters change. The latter is likely to
be more frequent than the former, although these are not necessarily distinct,
since a lingo parameter could be use to switch between lingo functions say xor
versus shuffle.

Two classes of synchronization mechanism are identified in ESORICS23:
_periodic_ –that uses synchronized clocks and fixed time intervals for
changing to the next phase and its lingo set) or next parameter values; and
_aperiodic_ –using information in the local history to determine when/what to
change.

In the CoAP dialect studied here, there is one (abstract) lingo with a
changing parameter that selects the next pseudo random string in a practically
unpredictable (i.e. hard to predict) sequence. The CoAP dialect uses aperiodic
synchronization for reasons discussed in Section 6. The relevant history is a
set of counters one for each communication partner that is incremented upon
each use.

#### Genericity.

In the framework proposed in ESORICS23, dialects are parametric in a list of
lingos and thus can be applied to any protocol theory for which the lingos are
applicable. Assuming that message content is of type string enables a wide
choice of lingos independent of the meaning of the strings. The CoAP lingo
functions assume an abstract message content type Content and thus the CoAP
dialect could be applied to any protocol specification with this content type
(and suitable configuration sort). We note that the example used in ESORICS23
suggests that the behavior of the dialect depends on the message type and even
uses information from the CONNECT messages, while the CoAP dialect does not
look inside message content. Presumably some dependence on message structure
could be made a parameter to the dialect in addition to the lingo parameters.

#### Attack model.

The ESORICS23 attack model starts with two models proposed in [8]: the _off-
path_ attacker that can send and receive messages, but can not see messages
exchanged between its targets; and the _on-path_ attacker with all the
capabilities of the off-path attacker, plus the ability to observe
communications between honest endpoints. ESORICS23 adds a third model: _active
on-path_ attacker with the capabilities of the on-path attacker plus the
ability to block, redirect, and alter message content. A refinement is also
introduced– _(m, n, t) attacker_ that in time t can observe _m_ messages and
block _n_ messages (and send/receive, block, …). The goal of a dialect is low
probability that an “attacked” message will be accepted by intended receiver.

In this paper we define two attack models for CoAP messaging systems: _active_
and _reactive_. In either case, an attacker is allowed a bounded set of
actions from a set of capabilities (depending on the model). The bound on
number of actions is an alternative to the bounds in the _(m,n,t)_ attack
model as a means to limit the attacker strength. The active attacker is based
on vulnerabilities identified in [4]. The capabilities are: block/drop, delay,
replay, or redirect messages. Our _active_ attack model differs from the
_active on-path_ model in that attackers don’t receive or create messages.
Like [4] we assume communications may be encrypted, so focuses on attacks that
don’t involve parsing messages – all the attacker learns from a message is the
target, source and a content blob.

The ESORICS23 paper is focused on understanding the structure of dialects and
attack models and gives some examples and informal statements about the
security guarantees of lingos and dialects. In the present paper we formally
specify an attack model and carry out reachability analyses concerning
specific undesired states of simple applications using the CoAP protocol
(inspired by [4]). We also prove properties relating executions of dialected
and undialected scenarios with and without attacks.

#### Taxonomies.

ESORICS23 proposes a taxonomy of dialects with four classes: Protocol
Specific; Protocol Generic; Protocol Modifying; Protocol Wrapping. The CoAP
dialect is essentially generic for single lingo case (the lingo needs to be
suitable for the protocol message structure) and it is Wrapping.

A lingo taxonomy is proposed with classes Shuffle/permutation (assumes
messages are bit strings); Split; Flow (via customized messages); Crypto
(HMAC, XOR, …); and Use of unused/random field. The CoAP lingo is abstract,
the functions could be realized using (combinations of) shuffle, xor, or
crypto. We did not consider Splitting as one of the aims of CoAP is to avoid
packet fragmentation. With an unreliable transport, the dialect/lingo itself
would have to do some extra work to avoid additional dropped messages.

#### Other points.

It appears that in the ESORICS23 framework all honest actors (protocol actors)
share the same secrets. Examples only consider two actor systems, so its not
completely clear. In section 8 we show examples of systems with 3 or more
endpoints where its important to have distinct pairwise shared secrets.

ESORICS23 also proposed notions of (generic) vertical and horizontal
composition. That is beyond the scope of the present work, but certainly an
interesting future direction along with partial evaluation transformations to
eliminate extra overhead where resources are very limited.

Complimentary to ESORICS23, the current paper carried out the dialect theory
transformation by hand, formalizing only the wrapping (and unwrapping) of
system configurations, and focused effort on formalizing attack models and
carrying out formal reachability analyses for a variety of scenarios.

##  10 Conclusions

Dialects such as ESORIC23 or the CoAP dialect can protect against replay,
editing message source and/or target, and message forging. They can not
protect against _interference_ attacks such as dropping or delaying. These
dialects also don’t protect against _piggy back attack_. In this attack there
are two attackers X,Y where X wants to send signals to Y. When A sends M to B,
X intercepts and sends to Y (on port j). Y learns the signal represented by j
and forwards M to B.

This suggested the reactive attacker model for dialects–a non-interference
model. The attacker can observe (copy), construct/edit, transmit (no
block/drop, delay) thus can replay, redirect, spoof. We showed that dialects
satisfying minimal conditions provide security against non-interference
attacks in the sense that a dialected protocol in the presence of such attacks
is bisimilar to the protocol alone.

We conclude with so ideas for future work. It could be interesting to consider
dialects that emit apparently random messages between themselves? These could
be versions of previously sent messages or made up messages of suitable size.
They should be similar to ordinary traffic and not sent too often. Can this
obfuscate patterns the attacker relies on? Another alternative is deploying
intermediate nodes with a dialect layer only. These would be used to obfuscate
where the message is actually going. There is still work to be done to capture
a generic attack model for messaging protocols: what are the properties that
applications care about? how to represent them generally? what attack
capabilities are needed to succeed in violating critical properties? is there
a notion of complexity of property that corresponds to a minimal bound on
successful attacker capability?

#### Acknowledgments.

Talcott thanks Dr. Catherine Meadows for many insightful discussions that lead
to some of the attack model ideas and other results. This material is based
upon work supported by the Naval Research Laboratory under Contract No.
N00173-23-C-2001. Any opinions, findings and conclusions or recommendations
expressed in this material are those of the author(s) and do not necessarily
reflect the views of the Naval Research Laboratory.

## References

  * [1] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott.  All About Maude: A High-Performance Logical Framework, volume 4350 of LNCS.  Springer, 2007.
  * [2] D. Galán, V. García, S. Escobar, C. Meadows, and J. Meseguer.  Protocol dialects as formal patterns.  In G. Tsudik, M. Conti, K. Liang, and G. Smaragdakis, editors, Computer Security – ESORICS 2023, pages 42–61. Springer Nature Switzerland, 2024.
  * [3] K. Gogineni, Y. Mei, G. Venkataramani, and T. Lan.  Can you speak my dialect?: A framework for server authentication using communication protocol dialects.  CoRR, abs/2202.00500, 2022.
  * [4] J. P. Mattsson, J. Fornehed, G. Selander, F. Palombini, and C. Amsuss.  Attacks on the constrained application protocol (CoAP), 2023.  Internet Draft, Network working group, 13 December 2023.
  * [5] Y. Mei, K. G. T. Lan, and G. Venkataramani.  MPD: Moving target defense through communication protocol dialects.  In J. Garcia-Alfaro, S. Li, R. Poovendran, H. Debar, and M. Yung, editors, Security and Privacy in Communication Networks, volume 398 of Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, page 100–119. Springer International Publishing, Cham, 2021.
  * [6] J. Meseguer.  Conditional Rewriting Logic as a unified model of concurrency.  Theoretical Computer Science, 96(1):73–155, 1992.
  * [7] P. C. Ölveczky and J. Meseguer.  The real-time maude tool.  In TACAS 2008, pages 332–336, 2008.
  * [8] T. Ren, R. Williams, S. Ganguly, L. D. Carli, and L. Lu.  Breaking embedded software homogeneity with protocol mutations.  In 18th EAI International Conference on Security and Privacy in Communication Networks (SecureComm 2022), pages 770–790. Springer, 2023.
  * [9] Z. Shelby, K. Hartke, and C. Bormann.  Rfc 7252: The constrained application protocol (CoAP), June 2014.
  * [10] M. Sjoholmsierchio.  Software-defined networks: Protocol dialects.  Master’s thesis, Naval Postgraduate School, Monterey, California, 2019\.
  * [11] M. Sjoholmsierchio, B. Hale, D. Lukaszewski, and G. Xie.  Strengthening sdn security: Protocol dialecting and downgrade attacks.  In 7th International Conference on Network Softwarization, page 321–329. IEEE, 2021.
  * [12] M. Team.  https://maude.csl.sri.com, 2024.

##  Appendix 0.A Characterization of reachable CoAP system configurations

As for real-time Maude specifications [7] the rewrite rules for the CoAP
specification (and it dialected form) are either instantaneous rules or the
tick rule that models passing of time. The minimum time to elapse function,
mte(sys), determines when time can pass. The following propositions give
essential properties of reachable CoAP and dialected CoAP system
configurations according to the value mte(sys).

######  Proposition 1 (Mte based characterization of reachable CoAP
configurations)

Let sysI be an initial configuration and let sysC be a CoAP system
configuration reachable from sysI. Then mte(sysC) is either 0, nz a non-zero
natural number, or the constant infty (representing infinity) and one of the
following holds.

  * 1.

mte(sysC) = nz:NzNat. In this case the tick rule is enabled (and no other rule
is enabled (except possibly net which commutes with and is independent of
tick). Further more

    * –

for all msg @ d in the network, $\mathtt{d}>0$ (ow mte is 0).

    * –

for all msg @ d in some w4Ack attribute $\mathtt{d}>0$ (ow mte is 0).

    * –

if the sendReq attribute of some endpoint is not empty (nilAM) then either
there are more than the w4Ack limit of requests waiting for acknowledgement
(and hence rule devsnd is not enabled), or the corresponding sndCtr attribute
is non-zero.

  * 2.

mte(sysC) = 0 In this case some rule is enabled according to one of the
following cases.

    * –

there is a message with zero delay in the net, then the rule rcv is enabled
(possibly preceeded by net) to move the message from network input to network
output;

    * –

there is a w4Ack attribute of some endpoint with a zero delay message, then
the ackTimeout rule is enabled;

    * –

there is a sendReqs attribute of some endpoint that is not empty and sending
is enabled, so the rule devsnd is enabled.

  * 3.

mte(sysC) = infty. In this case sysC is a terminal configuration, no rules
apply since the net is empty, all w4Ack attributes are empty, and all sendReqs
are empty buy definition of mte.

The definition of mte is extended to dialected CoAP configurations by adding
the rule that mte is 0 if any local nets are non-empty. Thus messages in local
nets must be delivered or dialected and put in the global net before time can
pass. The consequences are captured in the next proposition.

######  Proposition 2 (Mte based characterization of reachable dialected CoAP
configurations.)

As for the non-dialected case there are three cases.

  * 1.

$\mathtt{mte(dsysC)}=\mathtt{nz:NzNat}$. In this case the value of mte is
determined by the global network and the sysC level attributes and only the
tick rule (and possibly net) is enabled.

  * 2.

$\mathtt{mte(dsysC)}=\mathtt{0}$. In this case, if there is a message some
local net the either ddevsnd or rcv is enabled. Otherwise either ddevrcv is
enabled or some rule at the sysC level as shown in Proposition 1.

  * 3.

$\mathtt{mte(dsysC)}=\mathtt{infty}$. In this case dsysC is terminal. As for
sysC the net is empty (global and local), w4Ack attributes are empty, and
sendReq attribues are empty so no rule is enabled.

##  Appendix 0.B CoAP vulnerabilities

The paper [4] motivates an extension to the CoAP standard by describing
several vulnerabilities where attacks do not depend on being able to see
message content, i.e. these attacks can in principle be carried out against
CoAP running over DTLS or other transport providing encryption.

Four classes of vulnerability are discussed using message diagrams to
illustrate attack scenarios. Three of the classes rely only on the ability to
drop or delay messages. In some cases the vulnerability is due to reuse of
tokens resulting in requests connected to multiple responses. These scenarios
do not exhibit vulnerabilities in the Maude specification, but in some cases
we give alternative scenarios that realize a similar vulnerability. With the
execption of the example that relys on mismatching responses to GETs of
different resources on one server, dialecting does not change the success of
attacks as it can not detect blocking/dropping or delay. Our modified version
of the mismatch case uses two servers and in this case dialecting prevents the
attack becuase lingos are pairwise disjoint. The fourth class concerns message
fragmentation in the network. This is not modeled in the current Maude CoAP
specification.

In the following we show how the three relevant vulnerabilities can be
formally modeled and analyzed using the Maude specification. In the diagrams,
the vertical lines are participant send/receive event timelines. The client is
labelled dev0, the server labelled dev1 and the attacker labelled eve. The
state of the server resource "door" is indicated at the beginning and end of
the server timeline. In a timeline, os mark normal send or receive events, X