
\section{The MimbleWimble protocol} \label{sec:background}
\label{MW}
Transactions are at the core of the Mimblewimble protocol and they constitute a derivation of what are known as confidential transactions \cite{GMaxwell:conftransac,AGibson:conftransac}. 

A confidential transaction allows a sender to encrypt the amount of bitcoins he wants to send by using blinding factors, which are values chosen by the sender that are  used to encrypt bitcoin amounts in a transaction. In a confidential transaction only the two parties involved know the amount of bitcoins being transacted. However, onlookers can still ensure that the transaction is valid by comparing the number of inputs and outputs; if both are the same, then the transaction will be considered valid. Such a procedure ensures that no bitcoins have been created from nothing and is key in preserving the integrity of the system.

Mimblewimble transactions function in a similar way, except  the recipient of a transaction randomly selects a range of blinding factors provided by the sender. This blinding factor is then used as proof of ownership by the receiver, thus, permitting him to spend the bitcoins.

The MimbleWimble protocol aims at providing the following properties \cite{mimbleimble-wp,mimbleimble-doc}:
\begin{inparaenum}[i)] 
\item verification of zero sums without revealing the actual amounts involved in a transaction, which implies anonymity;
\item authentication of transaction outputs without signing the transaction; and 
\item good scalability, while preserving security, by generating blocks of smaller sizes---or better, the size of old blocks can be reduced thus producing a blockchain whose size does not grow in time as much as, for instance, Bitcoin's.
\end{inparaenum} 



The first two properties are achieved by resting, in the end, on Elliptic Curves Cryptography (ECC) operations and properties.
The third one is a consequence of the first two.

\paragraph{{\bf Verification of transactions}}
If $v$ is the value of a transaction (either input or output) and $H$ is a point over an elliptic curve,
then $vH$ encrypts $v$ because it is assumed to be computationally hard to get $v$ from $vH$ if we only know $H$. However, if $w$ and $z$ are other values such that $v + w = z$, then if we only have the result of encrypting each of them with $H$ we are still able to verify that equation. Indeed:
$
v + w = z \iff vH + wH = zH,
$
due to simple properties of scalar multiplication over groups. Therefore, with this simple operations, we can check sums of transactions amounts without knowing the actual amounts. 

Nevertheless, say some time ago we have encrypted $v$ with $H$ and now we see $vH$, then we know that it is the result of encrypting $v$. In the context of blockchain transactions this is a problem because once a block holding $vH$ is saved in the chain it will reveal all the transactions of $v$ coins. For such problems, MimbleWimble encrypts $v$ as $rG + vH$ where $r$ is an scalar and $G$ is another point in $H$'s elliptic curve. $r$ is called \emph{blinding factor} and $rG + vH$ is called \emph{Pedersen Commitment}. By using Pedersen Commitments, MimbleWimble allows for verification of expressions such as $v + w = z$ providing more privacy than with the standard scheme. In effect, if $v + w = z$ then we chose $r_v$, $r_w$ and $r_z$ such that $r_vG + r_wG = r_zG$ and so the expression is recorded as:
$$
\overbrace{(r_vG + vH)}^v + \overbrace{(r_wG + wH)}^w = 
\overbrace{r_zG + zH}^z
$$
making it possible for every one to verify the transaction without knowing the true values.

\paragraph{{\bf Authentication of transactions}}
Consider that Alice has received $v$ coins and this was recorded somewhere in the blockchain as $rG + vH$, where $r$ was chosen by her to keep it private. Now she wants to transfer these $v$ coins to Bob. As a consequence, Alice looses $v$ coins and Bob receives the very same amount, which means that the transaction adds to zero: $rG + vH - (rG + vH) = 0G - 0H$. However, Alice now knows Bob's blinding factor because it must be the same chosen by her (so the transaction is balanced). In order to protect Bob from being stolen by Alice, MimbleWimble allows Bob to add his blinding factor, $r_B$, in such a way that the transaction is recorded as:
$
(r + r_B)G + vH - (rG + vH) = r_BG - 0H,
$
although now it does not sum zero. However, this \emph{excess value} is used as part of an authentication scheme. Indeed, Bob uses $r_B$ as a private key to sing, say, the empty string ($\epsilon$). This signed document is attached to the transaction so in the blockchain we have:
\begin{inparaenum}[1)] 
\item Input: $I$; 
\item Output: $O$; and 
\item Bob's signed document: $S$.
\end{inparaenum} 
In this way, in order to verify the transaction one has to see whether the result of decrypting $S$ with $I - O$ (in the group generated by $G$) yields $\epsilon$. If $I - O$ does not yield something of the form $r_BG - 0H$, then $\epsilon$ will not be recovered and so we know there is an attempt to create money from thin air or there is an attempt to still Bob's money.

\section{Source code verification}
\label{sec:source-verification}


Verification of the correctness of the source code is the ultimate goal of the entire verification process. We shall take as reference implementation the code available at Grin's GitHub repository.

In what follows we shall illustrate, by means of a simple example, the verification process we have in mind.
For that we consider the Rust code shown in Figure \ref{partialeq} which corresponds to function \verb+PartialEq+ located in \verb+grin/core/src/core/transaction.rs+ of the mentioned repository.

This example is not intended to produce 
a final specification of \verb+PartialEq+; in particular, the specification shown below does not necessarily corresponds to a correct semantics of a Rust program. The idea is to give an approximation of the technique that should be used. In particular, the semantics model is a little bit more abstract than it should be.

\begin{figure*}
\footnotesize
\begin{verbatim}
/// A transaction
#[derive(Serialize, Deserialize, Debug, Clone)]
pub struct Transaction {
    /// List of inputs spent by the transaction.
    pub inputs: Vec<Input>,
    /// List of outputs the transaction produces.
    pub outputs: Vec<Output>,
    /// List of kernels that make up this transaction (usually a single kernel).
    pub kernels: Vec<TxKernel>,
    /// The kernel "offset" k2
    /// excess is k1G after splitting the key k = k1 + k2
    pub offset: BlindingFactor,
}

/// PartialEq
impl PartialEq for Transaction {
    fn eq(&self, tx: &Transaction) -> bool {
        self.inputs     == tx.inputs
        && self.outputs == tx.outputs
        && self.kernels == tx.kernels
        && self.offset  == tx.offset
    }
}
\end{verbatim}
\normalsize
\caption{\label{partialeq}MimbleWinble code snipet (\texttt{PartialEq::grin/core/src/core/transaction.rs})}
\end{figure*}


\subsection{From code to specification}

In this section we will derive a formal specification (of part) of the implementation code. This specification coincides with the specification named $S_2$ in Section \ref{r2sc2s}.

The first step in the process of deriving a formal specification of a portion of code is the choice of the mathematical setting in which shall be expressed the (abstract) semantics of the code. In the case of the Rust code we are presenting as the example one obvious first choice is to adopt, and possibly extend, an already existing formulation of the semantics of that programming language (see \cite{DBLP:journals/corr/abs-1804-07608,Reed2015PatinaA}). 
 An alternative approach would be to write down from scratch the model using the  mathematical and tool setting that better suit the skills of the specification team. Clearly, both approaches have the corresponding pros and cons.


For the present example we shall opt for the second alternative
We specify just the elements we need for the present example. As specification language we use set theory and first-order logic.
We are thinking of providing two specifications: one using the Z language \cite{Spivey} and the other one using \texttt{Coq}.

\verb+Transaction+ is a \verb+struct+. We will formalize this type as records. Then the semantics of \verb+Transaction+ is:
\begin{equation}
\begin{split}
Tran&saction \triangleq \\
[ & inputs:List(Input); \\
  & outpus:List(Output); \\
  & kernels:List(\mathit{TxKernel}); \\
  & \mathit{offset}: \mathit{BlindingFactor}]
\end{split}
\end{equation}
where, for instance, $List(Input)$ is the semantics assigned to \verb+Vec<Input>+ given that the latter is a {\it contiguous growable array type} (\url{https://doc.rust-lang.org/std/vec/struct.Vec.html})
while the former is the type of lists\footnote{In set theory a list is an element of the set of partial functions, which in turn is a subset of the type of binary relations, which in turn is a synonym for the powerset of a given Cartesian product.}  of type $Input$.

Now \verb+PartialEq+ is function taking two arguments and returning a Boolean. In a first attempt we can model it as a binary relation, $\mathit{PartialEq}$, as follows:
\begin{equation}\label{partialeqdef}
\begin{split}
\texttt{PartialEq} & \texttt{(a,b) = true} \\
   & \iff (\llbracket a \rrbracket,\llbracket b \rrbracket) \in \mathit{PartialEq}
\end{split}
\end{equation}
where $\llbracket \cdot \rrbracket$ for any Rust construct means the semantics of that construct. In turn, $PartialEq$ can be defined as:
\begin{equation}
\begin{split}
\textit{Par}&\textit{tialEq} = \\
 & \{(x, y) \in Transaction \times Transaction \\
 &\quad\mid x.inputs = y.inputs \\
 &\qquad\land x.outputs = y.ouputs \\
 &\qquad\land x.kernels = y.kernels \\
 &\qquad\land x.\mathit{offset} = y.\mathit{offset}\}
\end{split}
\end{equation}


In this case both parameters are references to objects (of type \verb+Transaction+) in memory. Then, the semantics model should include a representation of objects in memory. We will model the memory as a partial function, $mem$, from memory addresses, $ADDR$, onto their contents. Besides we will model the notion embodied in the \verb+self+ construct by the $\mathit{self}$ variable. With these elements we can refine the predicate given in \eqref{partialeqdef} as follows:
\begin{equation}
\begin{split}
\texttt{Par} & \texttt{tialEq(\&self,tx:\&Transaction) = true} \\
   & \iff \mathit{self} \in Transaction \\
   &\hspace{9mm}\land mem(tx) \in Transaction \\
   &\hspace{9mm}\land (\mathit{self},mem(tx)) \in \mathit{PartialEq}
\end{split}
\end{equation}


\hly{At this point we are inclined to illustrate the various possible uses of the model, showing how it can be translated to \{setlog\} and a simple proof can be carried out as well as some simulation of code execution.}

\subsection{Code verification}
\hly{TBC}


\section{Final remarks}
\label{sec:conclusion}
We have put forward elements that constitute essential steps towards the development of an exhaustive formalization  of the MimbleWimble cryptocurrency protocol, the analysis of its properties  and the verification of its implementations. In particular, the proposed idealized model is key in the described verification process.


\section{Approaches to formal software verification}
\label{sec:afsv}

Formal techniques can be applied in distinct phases of a software development project to different artifacts and aiming at different goals. Before choosing a formal technique to be applied it is necessary to define what artifacts need to be verified and the nature of the properties to be proved.

The universally accepted definition of program correctness is: \emph{a program is correct if it verifies its specification}. Usually, this specification is meant to be the \emph{functional specification} of the program. Given that in this work we are interested also in assessing the security of a software implementation we will take {\it program specification} as the functional and security specification of a program. Hence, in this context, \emph{a program is correct if it verifies its functional and security specifications}. 

We shall discuss in what follows two approaches to assess whether a program verifies its specification.

\subsection{From requirements to specification to code}
This is the classic approach proposed by the Software Engineering community when a brand new system is going to be developed. In this approach:
\begin{enumerate}
\item The development team writes down the \emph{requirements} of the system from the stakeholders' needs. The requirements of the system is typically a document written in natural language (sometimes accompanied by tables, illustrations, diagrams, etc.); i.e. it is an \emph{informal} description of the system. We will refer to this document as $R$.
\item From $R$ the development team elaborates a second document called software \emph{specification}. If a high degree of assurance of the final system is required this specification should be written using a \emph{formal notation}. We will refer to this document as $S$. Although formal, usually the specification is not executable, and if it does, it is usually very inefficient.
\item From $S$ the development team: a) elaborates a series of progressively more concrete specifications in such a way that the last document is an efficient program of $S$; or b) it directly writes a program. In any case, at least one new document is written: the program. We will refer to this document as $P$.
\item A number of \emph{verification activities} are carried out during the execution of the first three stages: 
\begin{itemize}
\item Properties of $S$ are proposed, \emph{formalized} and \emph{proved}. In this sense, $S$ is taken as an axiomatic theory and theorems of this theory are proved. A typical class of properties of a much used class of specifications are \emph{state invariants}. The more theorems are proved the more confidence on the soundness and completeness of the theory (i.e., $S$) is gained. 

Failing to prove an expected property is a strong indication of some error in the specification. Usually these errors remain unnoticed until the final deployment of the system. Removing those errors as soon as possible usually implies significant cost reductions and avoid schedule overruns.
\item If a series of specifications ending in a program is written, $S_1,\dots,S_n,P$, each specification $S_{i+1}$ is proved to be an implementation (or a \emph{refinement}) of $S_i$, and $P$ is proved to be an implementation of $S_n$. This \emph{guarantees} or \emph{certifies} that $P$ is a correct implementation of $S$ (${}=S_1$).

If $P$ is written directly from $S$ then the above chain of transformation verifications is reduced to a single, usually more complex, proof.

In any case, a prerequisite for this activity is to have a \emph{formal} semantics of the implementation technology (essentially of the programming language).
\item Extensive testing is performed.
\end{itemize}
\end{enumerate}


\subsection{\label{r2sc2s}From requirements to specification and from code to specification}
This approach can be seen as an adaptation of the first approach that can be used when at least a  substantial part of the system has already been implemented. Clearly, in this situation no formal $S$ is present (and in most cases no rigorous $R$ exists either) and, given that the there is an implementation, it is worthless to ask for a new implementation to be derived from the specification. Instead, the development team needs to check whether the existing implementation is correct or not, and in this last case to reveal all the errors. However, according to the definition of program correctness, checking the correctness of a given implementation can be done only w.r.t. a specification. Therefore, in this situation the following steps might be carried out:

\begin{enumerate}
\item\label{r} $R$ is written but usually from the existing project's documentation.
\item\label{s1} From $R$ a formal specification is generated; we will call it $S_1$.
\item\label{s1proof} Properties of $S_1$ are proved.
\item\label{s2} Another formal specification, called $S_2$, is derived from $P$. In this case, the structure (or design) of $P$ is considered. That is, each method, procedure, function, module, etc. in which $P$ has been divided or structured is formally specified. $S_2$ is the combination of the specification of all the elements of the design. Note that $S_2$ will predicate over the data structures and functions implemented by $P$, while $S_1$ will be more abstract.
\item\label{s2proof} Properties of $S_2$ are proved.
\item\label{s1s2} It is proved that $S_2$ is an implementation of $S_1$. If this proof fails, it should be analyzed whether the error is in $S_1$ or $S_2$. In general, $S_1$ should be considered more autoritative given that the correctness of the code is being assessed.
\item Extensive testing is performed.
\end{enumerate}

Like in the previous approach, having a formal semantics of the implementation technology is a prerequisite. All steps from \ref{s2} to \ref{s1s2} can reveal errors in $P$. Steps \ref{r}-\ref{s1proof} can be executed at the same time than steps \ref{s2}-\ref{s2proof}, by two independent teams.


\subsection{Discussion}
As the main objective of this work is to provide certified guarantees of the correctness of an existing implementation of the protocol we propose to follow the second verification approach.
Therefore, $S_1$ and $S_2$ can be used to formalize issues or features that surface at two different levels of abstraction. For example, buffer overflows would be expressible only in $S_2$ because otherwise $S_1$ would be too concrete or detailed (note that buffer overflows depend strongly on the implementation technology; for instance, they are impossible in a Haskell program but they are common in C programs) so it makes no sense to mention them in $S_1$. On the other hand, the formalization of a property such as access control is easier to specify at the level of $S_1$ because abstract data structures (such as sets, binary relations or partial functions) can be used. Specifying the same property in $S_2$ would require to use implementation-level data structures such as singly-linked lists which would require to formalize references, dereferencing, pointer arithmetics, etc. That is, it would require to fill the specification with concepts that obscure its true goal: make it evident the access control property.

Different verification technologies enable or facilitate some of the activities mentioned above, while others will disable or complicate others. We would like to mention two examples:
\begin{itemize}
\item The proof-assistant \texttt{Coq} \cite{coq-manual} can automatically provide certified implementations. Indeed, under mild assumptions, after proving that some specification verifies a given property a computable version of that property can be automatically extracted from the proof. This implementation can be used as a prototype or as a first, bug-free, low-performance implementation.
\item Usually, formal specifications are not executable. However, state-based, set-based specifications can be easily (and most of the times automatically) translated into $\{log\}$\xspace \cite{DBLP:conf/sefm/CristiaRF13}. This implies that, after writing a specification, a prototype is available for free. 
\end{itemize}


\subsection{Subtleties and traps with security properties}
In the present context, a formal definition of the security properties the system must verify is one of the most complex tasks. Security properties have proved to be unexpectedly complex to grasp and formalize. One of the fundamental reasons for this is that security properties are not safety properties (w.r.t. the Alper-Schneider framework). Most of the verification methods, results and tools developed for almost half a century by the Software Engineering community have been aimed at safety properties. Then, most of them fall short when dealing with security properties. Only very recently some of these methods and tools have been adapted for the problem of security properties.

For instance, safety properties enjoy, what is some times called, the \emph{refinement property}. This means that, if $S$ is the description of a system verifying safety property $F$ and $S'$ is a more deterministic refinement of $S$, then $S'$ (automatically) verifies $F$. However, in general, security properties do not enjoy the refinement property. This means that even if you have proved that $S$ verifies security property $F$ and that $S'$ is a refinement of $S$, then you cannot assert that $S'$ verifies $F$. The problem is that there are implementation decisions that in spite of generating a more deterministic system, they might introduce security issues. A typical example is the specification of the values stored in the memory cells delivered by the operating system to a process. At a certain level of abstraction these values might be underspecified which implies that, potentially, any value can be stored. Assume you can prove that this is secure. Afterwards, programmers decide to deliver the cells with the values left by the last process that used that buffer. Although this is an implementation of the first specification it is blatantly insecure.


On the other hand, reasoning about implementations provides the ultimate guarantee that
deployed mechanisms behave as expected. However, due to the issues mentioned above, formally proving non-trivial security properties of code might be an overwhelming task in terms
of the effort required, especially compared w.r.t. proving functional correctness (i.e. a safety property). In addition,
many implementation details are orthogonal to the security properties
to be established. This implies that slight changes in the implementation technology might have devastating consequences as concerns the security of the implementation. Therefore, complementary approaches are needed when non-trivial security properties are at stake:
\begin{enumerate}
\item Verification is performed on idealized models that abstract away the specifics of any particular implementation, and yet provide a realistic setting in which to explore the security issues that pertain to the realm of those (critical) mechanisms.
\item Additionally, verification is performed on more concrete models where low level mechanisms (such as pointer arithmetic) are specified. 
\item Finally, the low level model is proved to be a correct implementation of the idealized model.
\end{enumerate}

Note the similarities of this methodology w.r.t. the second approach outlined above.


A particular class of the idealized models mentioned above are those called \emph{security models}. These models have played an important role in the design and evaluation of high assurance security systems. Their importance was already pointed out in the Anderson report~\cite{1296905}. The
paradigmatic Bell-LaPadula model~\cite{Bell:LaPadula}, conceived in 1973, constituted the first big effort on providing a formal setting in which to study and reason on confidentiality properties of data in time-sharing mainframe systems. 

\emph{State machines}, in turn, are a powerful tool that can be used for modeling many aspects of computing systems. In particular, they can be employed as the building block of
a security model. The basic features of a state machine model are the
concepts of state and state change. A \emph{state} is a representation
of the system under study at a given time, which should capture those
aspects of the system that are relevant to the analyzed problem. State
changes are modeled by a state transition function that defines the
next state based on the current state and input. If one wants to
analyze a specific safety property of a system using a state machine
model, one must first specify what it means for a state to satisfy the
property, and then check if all state transitions \emph{preserve} it.
Thus, state machines can be used to model the enforcement of a
security policy on a system.











\section{Introduction}
\label{sec:intro}


Cryptocurrency protocols deal with virtual money so they are a valuable target of highly skilled attackers. Some attacks have already been mounted against cryptocurrency systems causing irreparable loses of money and credibility (e.g. \cite{dao}). For this reason the cryptocurrency community is seeking for approaches, methods, techniques and development practices that can reduce the chances of successful attacks. One such approach is the application of formal methods to software implementation. In particular, the cryptocurrency community is showing interest in formal proof and formally certified implementations. 

MimbleWimble is a privacy-oriented cryptocurrency technology encompassing  security and scalability properties that distinguish it from other technologies of the kind. Mimblewimble differs from Bitcoin \cite{bitcoin}, for  instance, in key areas: there is no concept of address and all the transactions are confidential. In this (short) paper we outline an approach based on formal software verification aimed at formally verifying the basic mechanisms of MimbleWimble and (one of) its implementations \cite{mimbleimble-doc}.


Reasoning about implementations provides the ultimate guarantee that deployed critical systems provide the expected properties. There are however significant hurdles with this approach.
Formally proving non-trivial security properties of code might be an overwhelming task in terms of the effort required, especially compared with proving functional correctness. In addition, many implementation details are orthogonal to the security properties to be established. This implies that slight changes in the implementation technology might have devastating consequences as concerns the security of the implementation. Therefore, complementary approaches are needed when non-trivial security properties are at stake. In this paper we put forward a model-driven verification approach where in the first place security issues that pertain to the realm of critical mechanisms are explored on an idealized model of the system under study. One such model abstracts away the specifics of any particular implementation and yet provides a realistic setting. Then verification is performed on more concrete models where low level mechanisms (such as pointer arithmetic) are specified; and finally the low level model is proved to be a correct implementation of the idealized model.



\paragraph{{\bf Organization of the paper}}
Section~\ref{sec:background} provides a very brief description of the MimbleWimble cryptocurrency protocol. 
Section \ref{sec:model} describes the building blocks of a formal idealized model (abstract state machine) of the computational behaviour of MimbleWimble and Section~\ref{sec:verification-MW} provides a brief account of the verification activities we are putting in place in order to verify the protocol and its implementation.
Final remarks are presented in Section \ref{sec:conclusion}.


\section{Verified implementation}
\section{Idealized model of a Mimblewimble-based blockchain}
\label{sec:model}








The basic elements in our model are transactions, blocks and chains. Each node in the blockchain maintains a local state. The main components are the local copy of the chain and the set of transactions waiting to be validated and added to a new block. Properties as zero-sum and the absence of double spending in blocks and chains must be proved for local states. 

The blockchain global state can be represented as a mapping from nodes to local states. For global states, we can state and prove properties of the entire system like, for instance,  correctness of the consensus protocol. 

\paragraph{{\bf Transactions}}
Given two elliptic curves $G$ and $H$, we represent transactions as tuples of the form:
$$
\begin{array}{lcl}
 Transaction &\stackrel{{\rm def}}{=}& \{i : I^{\star},\ o : O^{\star}, tk : TxKernel^{\star} \}
\end{array}
$$ where $X^{\star}$ represents the lists of $X$ elements.
Each element in $i$ and $o$ is a pair of the form $(r, v)$
representing the Pedersen commitment in curves $G$, $H$.  The transaction kernel $tk$ contains a list of range proofs of the outputs, a list of transaction excess and the kernel signature $\sigma$\footnote{For simplicity, we leave aside fees in this paper.}.
The transaction excess can be defined as: 
$$ ke = \sum_{(r',v') \in o}{r'.G + v'.H} - \sum_{(r,v) \in i}{ r.G + v.H}\ $$
We said that the transaction is balanced iff $\sum_{}{r'} - \sum_{}{r} = 0$. So, in other words, the excess is $(\sum_{}{v'} - \sum_{}{v})H$.
The kernel signature proves that the transaction is honestly constructed, in particular that the excess only contains the blinding factor (no money is being created).

A {\it transaction is valid} if:
\begin{inparaenum}[1)] 
\item the range proofs of all the outputs are valid;
\item the kernel signature $\sigma$ is valid for the excess; and
\item the transaction is balanced.
\end{inparaenum}	

\paragraph{{\bf Blocks and chains}}
Transactions can be merged into a {\it block}. We can see a block as a big transaction with aggregated inputs, outputs and transaction kernels.

A {\it Block} is either the {\it genesis block $\mathit{Gen}$}, or  a record: 
$$
\begin{array}{lcl}

 Block &\stackrel{{\rm def}}{=}& \{i : I^{\star},\ o : O^{\star},\ k : \nat ,\ tks : TxKernel^{\star}\} \\
\end{array}
$$
representing the inputs, outputs, the kernel offset and the list of transaction kernels for the block. The kernel offset $k$ is a blinding factor that needs to be added back to the kernel excess to verify the commitments sum to zero.



Given a block $b = \{i,o,k,tks\}$, we say that a block is valid if the following equality holds:

$$ \sum_{(r',v') \in o}{(r'.G+v'.H)} - \sum_{(r,v) \in i}{(r.G+v.H)}
    = 
    k + \sum_{(ke,s) \in tks}{ke}$$
    
A {\it chain} is a non-empty list of {\it blocks}:
$$\mathit{Chain} \stackrel{{\rm def}}{=} \mathit{Block}^{\star}$$

For a chain $c$ and a valid block $b$, we can define a predicate 
$\mathit{validates(c, b)}$ representing the fact that is valid to add $b$ to $c$. This relation must check, for example, that all the inputs in $b$ are present as outputs in $c$, in other words, they are unspent transaction outputs (UTXOs). 
    
\paragraph{{\bf Validating a chain}}
The model formalizes a notion of valid state that captures several well-formedness conditions. In particular, every block in the blockchain must be valid.
A predicate $\mathit{validChain}$ can be defined for a chain 
$c = [b_{0}, b_{1}, \dots b_{n}]$ by checking that:
\begin{inparaenum}[1)] 
 \item $b_0$ is a valid genesis block, and
 \item for every $i\in \{1, \dots n\}$, 
 $\mathit{validates([b_{0}, \dots, b_{i-1}], b_{i})}.$
\end{inparaenum}


The axiomatic semantics of the system is modeled by defining a set of actions, and providing their semantics as state transformers.  
The behaviour of actions is specified by a precondition and by a postcondition. This approach is valid when considering local (nodes) or global (blockchain) states and actions. Different set of actions, pre and postcondition are defined to cover local or global state transformations.

Valid states are invariant under execution. The properties in this work are obtained from valid states of the system.



\section{Verification of MimbleWimble}
\label{sec:verification-MW}
We now proceed to discuss some relevant properties that can be verified on our model.
In addition to some of the properties mentioned in Section \ref{MW} we also plan to include other properties such as those formulated in \cite{Pirlea:2018:MBC:3176245.3167086}, and various security properties considered in \cite{DBLP:conf/eurocrypt/GarayKL15,DBLP:conf/crypto/KiayiasRDO17,FuchsbauerOS19} later.

\subsubsection{Protocol Properties.}
\label{sec:properties}
The \textit{zero-sum} for valid transactions can be proved using properties of ECC. This property, and its proof, straightforwardly propagates to blocks, because adding zero-sum Pedersen commitments is a zero-sum Pedersen commitment. 

An important feature of MimbleWimble is the \textit{cut-through} process. The purpose of this property is to erase redundant outputs that are used as inputs within the same block. Let $C$ be some coins that appear as an output in the block $b$. If the same coins appear as an input within the block, then $C$ can be removed from the list of inputs and outputs after applying the  cut-through process. In this way, eventually, the only data that remain are the block headers, transaction kernels and unspent transaction outputs (UTXOs).
After applying cut-through to a valid block $b$ is important to ensure that the resulting block $b'$ is still valid. We can say that the validity of a block should be invariant with respect to the cut-through process. Basically, this invariant holds because the matching inputs and outputs canceled each other in the overall sum. 
\paragraph{Privacy and Security Properties.}
\label{sec:sec_props}
In blockchain systems the notion of privacy is crucial: sensitive data should not be revealed over the network. In particular,  it is desirable to ensure properties such as  confidentiality, anonymity and unlinkability of transactions. The first one refers to the property of preventing other participants from knowing certain information about the transaction, such as the amounts and addresses of the owners. The second one refers to the property of hiding the real identity from the one is transacting while the third one refers to the inability of linking distinct transactions of the same user within the blockchain. 

In  the Bitcoin network, users interact with the system using public key hashes achieving a kind of pseudo-anonymity. Every transaction recorded on the ledger contains the addresses of the sender and receiver and the transaction amount. That information is publicly available  breaking then  the confidentiality property. Furthermore, it fails in providing unlinkability since it is possible to trace the transactions of the same associated addresses over the ledger. 

In the case of Mimblewimble no addresses or public keys are used, there are only encrypted inputs and outputs. Therefore the communication between the sender and receiver to share the proof of ownership of the coins must be done off-chain using a secure channel. Privacy concerns rely on confidential transactions, cut-through and CoinJoin. The goal of CoinJoin is to combine inputs and outputs from different transactions into a single unified transaction. Thus, for a third-party it is difficult to determine which party is making a particular transaction. It is important to ensure that the resulting transaction satisfies the property of validity defined in the model.

The security problem of double spending refers to spend a coin more than once. All the nodes keep track of the UTXO set, so before confirming a block to the chain, the node checks that the inputs come from it. If we refer to our model, it is performed in the predicate \textit{validates} mentioned in Section \ref{sec:model}.  

\paragraph{Zero-knowledge Proof.}
The goal of this kind of proofs is to prove that a statment is true without revealing any information beyond the verification of the statment. These proofs could require interaction between the prover and the verifier or not. 
Genereally, when there is no interaction the validity of the proof relies on computational assumptions. 
In MimbleWimble  we need to ensure that in every transaction the transaction amount is positive so that users cannot create coins. The key here is to prove that property without revealing the amount. As we defined in the model, the output amounts are hidden in the form of a Pedersen Commitment and the transaction contains a list of range proofs of the outputs to prove that the transaction amount is positive. MimbleWimble uses Bulletproofs \cite{BunzBullet} to achieve this goal\footnote{This proof rely on the discrete logarithm assumption and a trusted setup is not required. The proof size is logarithmic in the amount size and the proof generation and verification are linear in the bit length of the range.}. In our model, this verification is performed as first step of the validity of the transaction.

\subsubsection{\bf Model-driven verification.}
MimbleWimble is built on top of a consensus protocol. 
In that direction, we have developed a Z specification of a consensus protocol (see Appendix \ref{zModel}). Z specifications in turn can be easily translated into the $\{log\}$\xspace language \cite{Cristia2019}. $\{log\}$\xspace can be used as both a (prototyping) programming language and an automated theorem prover for an expressive fragment of set theory and set relation algebra. We include an excerpt of the $\{log\}$\xspace prototype of a consensus protocol in Appendix \ref{setlogModel}.  This $\{log\}$\xspace prototype can be used as an executable model where simulations can be run. This allows us to analyze the behavior of the protocol without having to implement it in a low level programming language.

We also plan to use $\{log\}$\xspace to prove some of the properties mentioned above.  However, for complex properties or for properties not expressible in the set theories supported by $\{log\}$\xspace we plan to develop a complete and uniform formulation of several security properties of the protocol using the \texttt{Coq} proof assistant \cite{coq-manual}. \texttt{Coq} has an important set of libraries; for example \cite{DBLP:conf/itp/BartziaS14} contains a formalization of elliptic curves theory, which allows the verification of elliptic curve cryptographic algorithms. 
The fact of first having a $\{log\}$\xspace prototype over which some verification activities can be carried out without much effort helps in simplifying the process of writing a detailed \texttt{Coq} specification. This is in acordance with proposals such as \texttt{QuickChick} whose goal is to decrease the number of failed proof attempts in \texttt{Coq} by generating counterexamples before a proof is attempted \cite{denes2014quickchick}.

Applying the program extraction mechanism provided by \texttt{Coq} we shall be able  to derive a certified Haskell prototype of the protocol, which can be used as a testing oracle and also to conduct further verification activities on correct-by-construction implementations of the protocol. In particular, both the $\{log\}$\xspace and \texttt{Coq} approaches can be used as forms of model-based testing. That is, we can use either specification to automatically generate test cases with which protocol implementations can be tested \cite{CristiaRossiSEFM13,denes2014quickchick}.


\section{Testing and monitoring in \texttt{Coq}}
\label{sec:prototype}
\newcommand{\exec}[4]{$#1 \overset{#2/#3}{\hookrightarrow} #4$}



A system like the MimbleWimble protocol interacts with many other software systems. Some of these external systems are large and complex (e.g. the operating system and the TCP/IP protocol stack). When proving the correctness of a MimbleWimble implementation the interfaces of these external systems have to be axiomatized and thus assumed correct (because it would be impractical to prove the correctness of, say, the Linux operating system as a prerequisite to prove the correctness of MimbleWimble). However, these axioms might not describe the true behavior of these interfaces. Given that the proof of correctness of the MimbleWimble protocol depends on these axioms, if they are not accurate then MimbleWimble might behave unexpectedly. A similar analysis can be made when the compiler or runtime of the programming language on which MimbleWimble is implemented, is considered (i.e. they might not produce or execute code as assumed and a formal proof is out of scope). 

Since a formal proof is not feasible, extensive testing and monitoring may be the only tools to help in revealing many of these mismatches. Furthermore, this context is the ideal situation to apply: a) some model-based testing method; and b) a certified MimbleWimble's monitor. Both activities are based on using \texttt{Coq}'s program extraction mechanism. By using this \texttt{Coq}'s feature, we can derive a \emph{certified} Haskell prototype of the model described in Section \ref{sec:model}. This means that this Haskell program behaves exactly as described in the formal model and that it verifies \emph{all} of the security and functional properties that the model satisfies.

We briefly comment and motivate these two activities in what follows.


\subsection{\label{testing}Certified security testing}
Model-based testing (MBT) is a lively research area whose main goal is to use
models of implementations as test case and oracle sources \cite{Utting00}. 
One of the possible high-level MBT processes is depicted in Figure \ref{f:mbt}. 
MBT methods based on such a process generate \emph{abstract test cases} by performing different
static analyzes of a (formal) model (of a given program). This abstract test
cases are later refined to the level of the program; the program
is run on these refined test cases; the outputs are collected and abstracted
away to the level of the model; and, finally, the model, the abstract test cases
and the abstracted outputs are used to decide whether the program has
errors or not. 

\begin{figure*}
\centering
\tikz [
    nonterminal/.style={
    rectangle, 
    minimum width=3.5cm, 
    minimum height=4mm,
    node distance=5mm,
    thick, 
    draw=black},
    >=Latex, arrows={[round]}] {
\node [nonterminal] (get) at (0,0) {get output};
\node [nonterminal] (abs) at (4.5,0) {abstract output};
\node [nonterminal] (vfys) at (9,0) {verify w.r.t. model};
\node [nonterminal] (set) at (9,1) {set initial values};
\node [nonterminal] (run) at (0,1) {run program};
\node [nonterminal] (gen) at (1.42,2) {generate abstract test cases from model};
\node [nonterminal] (ref) at (9,2) {refine  test cases};
\draw (gen) edge[->] (ref)
      (ref) edge[->] (set)
      (set) edge[->] (run)
      (get) edge[->] (abs)
      (abs) edge[->] (vfys)
      (run) edge[->] (get);
}
\caption{\label{f:mbt}Proposed MBT process}
\end{figure*}

In particular, for the generation of abstract test cases, a MBT method known as the Test Template Framework (TTF) \cite{Stocks2} can be applied. The TTF was originally thought as a MBT method for Z specifications \cite{Spivey:1989:ZNR:61690}  but it can be easily adapted to \texttt{Coq} models. 
In effect, a \texttt{Coq} model as the one we propose in Section \ref{sec:model} is a state machine featuring complex state and input variables and state transitions given by their pre- and post-conditions, much as Z specifications. Furthermore, pre- and post-conditions of our \texttt{Coq} axiomatic specification make use of non-trivial library operations on lists, similarly as Z specifications rest on library operations on sets. Besides, a tool such as $\{log\}$\xspace has proved to be effective in abstract test case generation and in eliminating unfeasible test specifications.


\subsubsection*{The Test Template Framework} 
In the TTF the specification of the system under test (SUT) takes the form of a state machine (not necessarily a finite one). The TTF defines a methodology for generating abstract test cases for each state transition of the state machine. Then, let $A(\vec i,\vec s,\vec s',\vec o)$ be such an state transition depending on a vectors $\vec i$, $\vec s$, $\vec s'$, and $\vec o$ of, respectively, input, before-state, after-state and output variables\footnote{For the sake of simplicity, from now on, we will avoid the vector notation.}. Such an state transition is specified by its pre- and post-conditions: $A(i,s,s',o) \equiv Pre_A(i,s) \implies Post_A(i,s,s',o)$, where $Pre_A$ and $Post_A$ are two predicates.

The first step of the test case generation method of the TTF is to define the \emph{valid input space} of each state transition, which is the set of all possible values for $i$ and $s$ satisfying the precondition. Formally, $A^{VIS} \equiv \{(i,s) \mid Pre_A(i,s)\}$. 

As the second step, the TTF states that the VIS must be partitioned by a technique called \emph{recursive domain partition} (RDP). RDP is the core of the TTF. RDP starts by applying a \emph{testing tactic} to the VIS thus generating a partition of the VIS in the form of a collection of \emph{test specifications}. Each testing tactic describes how a test specification can be partitioned in order to obtain new and more demanding test specifications. A test specification is simply a set of test cases described by a predicate depending of the input and before-state variables. These predicates are called \emph{characteristic predicates}. Then, each testing tactic is defined by the collection of characteristic predicates that it generates. 

Hence, if testing tactic $T_a$ applied to $A^{VIS}$ generates the (characteristic) predicates $P^a_1,\dots,P^a_{n_a}$, the TTF states that $A$ has to be tested with test cases taken from the following test specifications:
\begin{gather*}
A^{T_a}_1 \equiv \{A^{VIS} \mid P^a_1(i,s)\} \\
A^{T_a}_2 \equiv \{A^{VIS} \mid P^a_2(i,s)\} \\
\dots \\
A^{T_a}_{n_a} \equiv \{A^{VIS} \mid P^a_{n_a}(i,s)\}
\end{gather*}

RDP continues by picking one or more of the $A^{T_a}_i$ and applying to them one or more testing tactics. For example, testing tactic $T_b$ can be applied to $A^{T_a}_2$ thus generating the following test specifications:
\begin{gather*}
A^{T_b}_1 \equiv \{A^{T_a}_2 \mid P^b_1(i,s)\} \\
A^{T_b}_2 \equiv \{A^{T_a}_2 \mid P^b_2(i,s)\} \\
\dots \\
A^{T_b}_{n_b} \equiv \{A^{T_a}_2 \mid P^b_{n_b}(i,s)\}
\end{gather*}

This process continues until engineers think they have a good coverage of the specification. The test specifications generated in this way can be accommodated in a so-called \emph{testing tree}. The testing tree has the VIS as its root node, the test specifications generated after applying the first testing tactic in the first level; the test specifications generated after applying more testing tactics to the first level, in the second level; and so forth. Note that the more testing tactics are applied, the more precise are the leaves of the testing tree. In effect, observe that the characteristic predicates of each testing tactic are conjoined to each other thus turning the characteristic predicates of leaves into conjunctions of several constraints. For example, if $A^{T_a}_2$ is expanded inside $A^{T_b}_2$ we have:
\begin{gather*}
A^{T_b}_2 \equiv \{A^{VIS} \mid P^a_2(i,s) \land P^b_2(i,s)\}
\end{gather*}

The third step in the TTF is to prune the unsatisfiable leaves off the testing tree. If the TTF is mechanically applied it tends to generate many unsatisfiable leaves as contradictory constraints can be conjoined in the same test specification. Depending on the theory used for the specification of the SUT, pruning can be an intractable problem but in general there exist algorithms that perform well in practice \cite{CristiaRossiSEFM13}.

The fourth and final step in the TTF is to generate an abstract test case from each surviving leaf of the testing tree. In this context, abstract test cases take the form of closed propositional sentences
binding state and input variables to concrete values. More precisely, an
abstract test case is a conjunction of equalities between variables and constant
terms. For example, if $A^{T_b}_3$ is a satisfiable test specification, its corresponding test case is described as follows:
\begin{gather*}
A^{TC}_3 \equiv \{A^{T_b}_3 \mid i = c_i \land s = c_s\}
\end{gather*}
where $c_i$ and $c_s$ are two constant (vector) terms. Observe that such a test case must verify all the characteristic predicates all the way up in the testing tree to the root node. Then, essentially, such a test case sets the initial state
and input values from which the state transition to be tested must be executed. In the TTF, test case generation is the dual problem of leaf pruning as both amount to solve the same satisfiability problem (i.e. determining whether test specifications are satisfiable or not) \cite{DBLP:journals/stvr/CristiaAFPM14}.

One of the advantages of the TTF is that it encourages that all the artifacts involved in the testing process (e.g. state transitions and test specifications) can be expressed in the same notation.
 
According to Figure \ref{f:mbt}, abstract test cases must refined into the implementation platform so they can be executed on the SUT. 
The final step in Figure 
 \ref{f:mbt} is to check whether each abstract output conforms with the corresponding abstract test case. 


\subsubsection*{Applying the TTF to \texttt{Coq} models}
The TTF can be easily applied to MimbleWimble's \texttt{Coq} specification. In particular the Haskell prototype derived from the specification can be used as the oracle engine given that it correctly implements the specification. However, some tools, \hly{like ...}, need to be developed for automating the MBT process described above. The development of those tools is technically feasible, the timing depends on the amount of resources invested.


\subsection{Monitoring MimbleWimble's implementation}
The testing process proposed in the previous section is meant to be applied \emph{before} the MimbleWimble implementation goes into production. Clearly, the idea of testing is a) to uncover errors in the implementation and b) that critical errors are fixed,  both before the system is delivered. However, as every one knows, testing will not always uncover all the errors. Hence, even after a formal proof of correctness and extensive testing, errors in or flawed assumptions about external systems may still be used to compromise the security of MimbleWimble.

For this last class of issues we propose to use the certified Haskell prototype. Indeed, this prototype can be used as the basis for a (on-line, quasi-real-time) monitor of MimbleWimble's implementation. In this setting:
\begin{enumerate}
\item MimbleWimble's implementation passes to the monitoring system every input it receives.
\item The monitor uses the abstraction harnessing mentioned in Section \ref{testing} to abstract the inputs it receives.
\item The Haskell prototype is called with the abstracted inputs, thus mimicking the execution of the implementation.
\item If the Haskell prototype transitions to an unexpected state an alarm is rose and, either automatically or after a human evaluation, the implementation can be stopped, suspended or some other protective measure can be taken.
\end{enumerate}

Clearly, the monitoring system will not be as efficient as the real implementation, what may cause some delay between the time MimbleWimble's implementation receives the offending input and the time the monitor raises an alarm. However, most likely, this input will be one in a rather long chain of interactions that eventually would end in compromising MimbleWimble. Therefore, in most of the cases the alarm rose by the monitoring system will help to avoid otherwise successful attacks or errors that may lead the system to disrupt critical data or functions.

Monitoring systems have been proposed for the enforcement of critical security properties \cite{DBLP:conf/csfw/ZanariniJR13}.



\section{\label{setlogModel}Excerpt of a $\{log\}$\xspace Prototype of a Consensus Protocol}
In this section we show the $\{log\}$\xspace code corresponding to the Z model presented in Appendix \ref{zModel}. $\{log\}$\xspace code can be seen as both a formula and a program \cite{Cristia2019}. Thus, in this case we use the code as a prototype or executable model of the Z model. The intention is twofold: to show that passing from a Z specification to a $\{log\}$\xspace program is rather easy, and to show how a $\{log\}$\xspace program can be used as a prototype. The first point is achieved mainly because $\{log\}$\xspace provides the usual Boolean conectives and most of the set and relational operators available in Z. Hence, it is quite natural to encode a Z specification as a $\{log\}$\xspace program.

Given that $\{log\}$\xspace is based on Prolog its programs resemble Prolog programs. The $\{log\}$\xspace encoding of $RcvAddr$ is the following:
\begin{verbatim}
rcvAddr(LocState,P,Ps,LocState_) :-
LocState = {[as,As] / Rest} &
P = [_,this, addrMsg(Asm)] &
un(As,Asm,As_) &
diff(Asm,As,D) &
Ps1 = ris(A in D,[],true,[this,A,connectMsg]) &
Ps2 = ris(A in As,[],true,[this,A,addrMsg(As_)]) &
un(Ps1,Ps2,Ps) &
LocState_ = {[as,As_] / Rest}.
\end{verbatim}

As can be seen, \verb+rcvAddr+ is clause receiving the before state (\verb+LocState+), the input variable (\verb+P+), the output variable (\verb+Ps+) and the after state (\verb+LocState_+). As in Prolog, $\{log\}$\xspace programs are based on unification with the addition of set unification. In this sense, a statement such as \verb+LocState = {[as,As] / Rest}+ (set) unifies the parameter received with a set term singling out the state variable needed in this case (\verb+As+) and the rest of the variables (\verb+Rest+). The same is done with packet \verb+P+ where \verb+_+ means any value as first component and \verb+addrMsg(Asm)+ gets the set of addresses received in the packet without introducing an existential quantifier.

The set comprehensions used in the Z specification are implemented with $\{log\}$\xspace's so-called Restricted Intentional Sets (RIS) \cite{DBLP:conf/cade/CristiaR17}. A RIS is interpreted as a set comprehension where the control variable ranges over a finite set (\verb+D+ and \verb+As+). 

Given \verb+rcvAddr+ we can perform simulations on $\{log\}$\xspace such as:
\begin{verbatim}
S = {[as,{}] / R} & 
rcvAddr(S,[_,this,addrMsg({a1,a2})],P1,S1) & 
rcvAddr(S1,[_,this,addrMsg({a1,a3})],P2,S2).
\end{verbatim}
in which case $\{log\}$\xspace returns:
\begin{verbatim}
P1 = ris(A in {a1,a2/_N2},[],true,[this,A,connectMsg],true),  
S1 = {[as,{a1,a2}]/R},  
P2 = {[this,a3,connectMsg],[this,a1,addrMsg({a2,a1,a3})],
      [this,a2,addrMsg({a2,a1,a3})] /
      ris(A in _N1,[],true,[this,A,connectMsg],true)},  
S2 = {[as,{a2,a1,a3}]/R}
Constraint: subset(_N2,{a1,a2}), subset(_N1,{a1,a3}), 
            a1 nin _N1, a2 nin _N1
\end{verbatim}
That is, $\{log\}$\xspace binds values for all the free variables in a way that the formula is satisfied (if it is satisfiable at all). In this way we can trace the execution of the protocol w.r.t. states and outputs by starting from a given state (e.g. \verb+S+) and input values (e.g. \verb+[_,this,addrMsg({a1,a2})]+), and chaining states throughout the execution of the state transitions included in the simulation (e.g. \verb+S1+ and \verb+S2+).

\section{\label{zModel}Excerpt of a Z Model of a Consensus Protocol}
The following are some snippets of a Z model of a consensus protocol based on the model developed by P\^irlea and Sergey \cite{Pirlea:2018:MBC:3176245.3167086}. For reasons of space we just reproduce a little part of it.

The time stamps used in the protocol are modeled as natural numbers. Then we have the type of addresses ($Addr$), the type of hashes ($Hash$), the type of proofs objects ($Proof$) and the type of transactions ($Tx$). Differently from P\^irlea and Sergey's model\footnote{From now on we will refer to P\^irlea and Sergey model simply as PS.} we modeled addresses as a given type instead as natural numbers. In PS the only condition required for these types is that they come equipped with equality, which is the case in Z.
\begin{zed}
Time == \nat \also
[Addr,Hash,Proof,Tx]
\end{zed}
The block data structure is a record with three fields: $prev$, (usually) points to the parent block; $txs$, stores the sequence of transactions stored in the block; and $pf$ is a proof object required to validate the block.
\begin{schema}{Block}
prev:Hash \\
txs: \seq Tx \\
pf:Proof
\end{schema}
The local state space of a participating network node is given by three state variables: $as$, are the addresses of the peers this node is aware of; $bf$, is a block forest (not shown) which records the minted and received blocks; and $tp$, is a set of received transactions which eventually will be included in minted blocks.
\begin{schema}{LocState}
as:\power Addr \\
bf: Hash \pfun Block \\
tp: \power Tx
\end{schema}
The system configuration is represented by two state variables: $Delta$, which establishes a mapping between network addresses and the corresponding node (local) states (in PS this variable is referred to as the \emph{global state}); and $P$, a set of packets (which represent the messages exchanged by nodes). 
\begin{schema}{Conf}
Delta:Addr \pfun LocState \\
P:\power Packet
\end{schema}
Packets are just tuples of two addresses (origin and destination) and a message.
\begin{zed}
Packet == Addr \cross Addr \cross Msg
\end{zed}
The model has twelve state transitions divided into two groups: \emph{local} and \emph{global}. Local transitions are those executed by network nodes, while global transitions promote local transitions to the network level. In turn, the local transitions are grouped into \emph{receiving} and \emph{internal} transitions. Receiving transitions model the nodes receiving messages from other nodes and, possibly, sending out new messages; internal transitions model the execution of instructions run by each node when some local condition is met. Here, we show only the local, receiving transition named $RcvAddr$.
\begin{schema}{RcvAddr}
\Delta LocState \\
p?:Packet \\
ps!:\power Packet
\where
p?.2 = this \\
\exists asm:\power Addr @ \\
   \t1 p?.3 = AddrMsg~asm \\
   \t1 \land as' = as \cup asm \\
   \t1 \land bf' = bf \\
   \t1 \land tp' = tp \\
   \t1 \land ps! = \{a:asm \setminus as @ (p?.2,a,ConnectMsg)\}~\cup \\
        \t1 ~~~~~\{a:as @ (p?.2,a,AddrMsg~as')\}
\end{schema}
As can be seen, $RcvAddr$ receives a packet ($p?$) and sends out a set of packets ($ps!$). The node checks whether or not the packet's destination address coincides with its own address. In that case, the node adds the received addresses to its local state and sends out a set of packets that are either of the form $(p?.2,a,ConnectMsg)$ or $(p?.2,a,AddrMsg~as')$. The former are packets generated from the received addresses and sent to the new peers the node now knows, while the latter are messages telling its already known peers that it has learned of new peers.
