Towards an Analysis of Dynamic Gossip in Netkat

Abstract

In this paper we analyse the dynamic gossip problem using the algebraic network programming language Netkat.

Netkat is a language based on Kleene algebra with tests and describes packets travelling through networks. It has a sound and complete axiomatisation and an efficient coalgebraic decision procedure. Dynamic gossip studies how information spreads through a peer-to-peer network in which links are added dynamically.

In this paper we embed dynamic gossip into Netkat. We show that a reinterpretation of Netkat in which we keep track of the state of switches allows us to model Learn New Secrets, a well-studied protocol for dynamic gossip. We axiomatise this reinterpretation of Netkat and show that it is sound and complete with respect to the packet-processing model, via a translation back to standard Netkat.

Our main result is that many common decision problems about gossip graphs can be reduced to checks of Netkat equivalences. We also implemented the reduction.

Appendix

1.1 Proof of Lemma 3

By induction on the call sequence $\sigma$. The base case follows instantly as $pol_\epsilon = 1$ outputs the same packet and thus the same gossip graph.

For the induction step we use that calling agents exchange everything they know and that this is encoded in the modifications done by $pol_{ab}$. As an example, consider the $\subseteq$ direction for N. By the induction hypothesis for $\sigma$ we have

$$\begin{aligned} N^{\sigma } \subseteq \{(a,b)\mid \forall \textsf {pk}\in \llbracket pol_{\sigma }\rrbracket (\textsf {pk}_G): \textsf {pk}.Nab = 1 \} \end{aligned}$$

and want to show for $\sigma ;xy$ that

$$\begin{aligned} N^{\sigma ;xy} \subseteq \{(a,b)\mid \forall \textsf {pk}\in \llbracket pol_{\sigma ;xy}\rrbracket (\textsf {pk}_G): \textsf {pk}.Nab = 1 \} \end{aligned}$$

Suppose $(a,b)\in N^{\sigma ;xy}$. Either $(a,b)\in N^{\sigma }$, in which case we are done by the induction hypothesis because $\textsf {pk}.Nab=1$ is preserved by $pol_{xy}$, or $(a,b)\notin N^{\sigma }$. For the latter case, w.l.o.g. we can assume that $a=x$. Thus we know that $(y,b) \in N^{\sigma }$. From our induction hypothesis we can conclude that $\forall \textsf {pk}\in \llbracket pol_{\sigma }\rrbracket (\textsf {pk}_G): \textsf {pk}.Nyb = 1$. Then in $pol_{xy}$ the field Nxb gets set to 1. Hence we know that $\forall \textsf {pk}\in \llbracket pol_{\sigma ;xy}\rrbracket (\textsf {pk}_G): \textsf {pk}.Nxb = 1$.    $\square$

1.2 Proof of Theorem 4

Using soundness and completeness of Netkat the given syntactic equivalence holds iff we semantically have .

Suppose LNS is weakly successful on G. Let us consider input packet $\textsf {pk}_G$ from Definition 10. We have $\llbracket pol_G \rrbracket (\textsf {pk}_G) = \{ pk_G \}$ by definition. There is at least one call sequence $\sigma \in LNS(G)$ that is successful. By Theorem 3 we know that $\sigma$ corresponds to an execution of $pol_\mathrm {LNS}$ on input $\textsf {pk}_G$ and there is a packet $\textsf {pk}$ such that and its fields $\mathsf {call}_m$ encode $\sigma$. Because $\sigma$ is successful we also have $\llbracket pol_\mathrm {success} \rrbracket (\textsf {pk}) = \{ \textsf {pk}\}$. Hence we can conclude $\textsf {pk}\in \llbracket pol_G\cdot pol_\mathrm {LNS}\cdot pol_\mathrm {success}\rrbracket (\textsf {pk}_G)$ and thus that $\llbracket pol_G\cdot pol_\mathrm {LNS}\cdot pol_\mathrm {success}\rrbracket \ne \varnothing$.

The other direction is similar, so we omit the proof here.    $\square$

1.3 Proof of Theorem 5

By soundness and completeness of Netkat the equivalence holds iff we have .

Suppose LNS is strongly successful on G. We immediately have $\supseteq$ because any packet passing the success check also passes the test that LNS has finished.

To show $\subseteq$, take any $\textsf {pk}$ and $\textsf {pk}'$ such that . We then know that $\textsf {pk}= \textsf {pk}_G$ because $\textsf {pk}$ passed the test $pol_G$. Hence . As $\llbracket pol_G\rrbracket (\textsf {pk}_G)=\{ \textsf {pk}_G \}$, we get that . From Theorem 3 we know that every output $\textsf {pk}'$ of corresponds to a call sequence $\sigma \in LNS(G)$. From the assumption that LNS is strongly successful on G we get that all of these $\sigma$ are successful call sequences. We thus know that $\llbracket pol_\mathrm {success} \rrbracket (\textsf {pk}') = \{ \textsf {pk}' \}$ and thereby .

The other direction is similar.    $\square$

1.4 Proof of Theorem 6

By soundness and completeness of Netkat, the statement is equivalent to:

$\Rightarrow$ Take the packet $\textsf {pk}_G$. We know that $\llbracket pol_G\rrbracket (\textsf {pk}_G)=\{\textsf {pk}_G\}$. As G is a sun graph, we know that for each agent i either $\llbracket pol_{Ni}\rrbracket (\textsf {pk}_G)=\{\textsf {pk}_G\}$ or $\llbracket pol_{\mathrm {self}_i}\rrbracket (\textsf {pk}_G)=\{\textsf {pk}_G\}$. Hence we have

for some packet $\textsf {pk}$. Thus we can conclude:

$\Leftarrow$ is similar.    $\square$

1.5 Proof of Corollary 1

Fix some G. By Theorem 5 LNS is strongly successful on G if and only if

and from Theorem 6 that G is a sun graph if and only if

Now suppose we have . From Theorem 5 we then know that LNS is strongly successful on G. By Theorem 2 it follows that G is a sun graph. From Theorem 6 we know this is equivalent to

The other direction is similar.    $\square$