Towards an Analysis of Dynamic Gossip in Netkat

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.

1. 1.

   To be precise, we use the verification_and_felix branch currently at commit be47c929ed84904f9bdb81bf9765a0432db63069. We would like to thank Steffen Smolka and Nate Foster for their help to get the decision method running.

We received helpful feedback from Jan van Eijck, Tobias Kappé, Jurriaan Rot, Jan Rutten and the anonymous RAMiCS reviewers. The first author was affiliated with the ILLC at the University of Amsterdam during most of this work. The research of the second author is funded by the Dutch NWO project 612.001.210.

Authors and Affiliations

1. University of Groningen, Groningen, The Netherlands

   Malvin Gattinger

2. CWI, Amsterdam, The Netherlands

   Jana Wagemaker

Corresponding author

Correspondence to Jana Wagemaker .

Editors and Affiliations

1. Université Laval, Québec, QC, Canada

   Jules Desharnais

2. University of Canterbury, Christchurch, New Zealand

   Walter Guttmann

3. Open Universiteit, Heerlen, The Netherlands

   Stef Joosten

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

and want to show for \(\sigma ;xy\) that

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 \)

Reprints and permissions

© 2018 Springer Nature Switzerland AG

Policies and ethics