Skip to main content
SpringerLink
Log in

A Switch, in Time

  • Conference paper
  • First Online:
Trustworthy Global Computing (TGC 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9533))

Included in the following conference series:

  • 287 Accesses

Abstract

Communication networks are quintessential concurrent and distributed systems, posing verification challenges concerning network protocols, reliability, resilience and fault-tolerance, and security. While techniques based on logic and process calculi have been employed in the verification of various protocols, there is a mismatch between the abstractions used in these approaches and the essential structure of networks. In particular, the formal models do not accurately capture the organization of networks in terms of (fast but dumb) table-based switches forwarding structured messages, with intelligence/control located only at the end-points.

To bridge this gap, we propose an extension of the axiomatic basis of communication proposed by Karsten et al. In this paper, a simple model of abstract switches and table-based prefix rewriting is characterized axiomatically using temporal logic. This formulation is able to address reconfigurations over time of the network. We illustrate our framework with simple examples drawn from SDNs, IPv6 mobility and anonymous routing protocols.

This work was partially supported by a grant from Microsoft Research to the first author, and NSF CCS-1228697 to the second author.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This assumption is to keep the model simple; more complex matching rules such as matching with the maximal prefix, or allowing for priorities among potential prefixes may be viewed as practical optimizations.

  2. 2.

    In [14], this relation was inductively defined using four axiom schema, two of which – reflexivity and transitivity — are implicit in temporal logic.

  3. 3.

    Actually, this property can be weakened to one requiring only that any such forwarding cycle will eventually get broken (see [23] for details).

References

  1. Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427–476 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  2. Amadio, R.M., Prasad, S.: Modelling IP mobility. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 301–316. Springer, Heidelberg (1998)

    Google Scholar 

  3. Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Armando, A., Basin, D.A., Cuéllar, J., Rusinowitch, M., Viganò, L.: Automated reasoning for security protocol analysis. J. Autom. Reason. 36(1–2), 1–3 (2006)

    Article  MathSciNet  Google Scholar 

  5. Clark, D.: The design philosophy of the DARPA internet protocols. In: Proceedings of SIGCOMM 1988: ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, vol. 8, pp. 106–114. ACM (1988)

    Google Scholar 

  6. Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 24–37. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  7. Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 342–356. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Dingledine, R., Mathewson, N., Syverson, P.F.: Tor: The second-generation onion router. In: Proceedings of 13th USENIX Security Symposium, SSYM 2004, pp. 303–320. USENIX Association (2004)

    Google Scholar 

  9. Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198–207 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  10. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.:Knowledge-based programs. In: Proceedings of PODC 1995: 14th Annual ACM Symposium on Principles of Distributed Computing, pp. 153–163. ACM (1995)

    Google Scholar 

  11. Guttman, J.D., Thayer, F.J., Zuck, L.D.: The faithfulness of abstract protocol analysis: message authentication. J. Comput. Secur. 12(6), 865–891 (2004)

    Google Scholar 

  12. Halpern, J.Y., Zuck, L.D.: A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. J. ACM 39(3), 449–478 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  13. Hughes, D.J.D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)

    Google Scholar 

  14. Karsten, M., Keshav, S., Prasad, S., Beg, M.: An axiomatic basis for communication. In: Proceedings of SIGCOMM 2007:ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, pp. 217–228. ACM (2007)

    Google Scholar 

  15. Kreutz, D., Ramos, F.M.V., Veríssimo, P.J.E., Esteve Rothenberg, C., Azodolmolky, S., Uhlig, S.: Software-defined networking: a comprehensive survey. Proc. IEEE 103(1), 14–76 (2015)

    Article  Google Scholar 

  16. Lamport, L.: What good is temporal logic? In: Information Processing 83 - Proceedings of WCC 1983: 9th IFIP World Computer Congress, pp. 657–668. North-Holland/IFIP (1983)

    Google Scholar 

  17. Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  18. Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)

    MATH  Google Scholar 

  19. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I. Inf. Comput. 100(1), 1–40 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  20. Perkins, C.E., Johnson, D.B.: Mobility support in IPv6. In: Proceedings of MobiCom 1996: 2nd Annual International Conference on Mobile Computing and Networking, pp. 27–37, New York, NY, USA. ACM (1996)

    Google Scholar 

  21. Prasad, S.: Abstract switches: A distributed model of communication and computation. In: Perspectives in Concurrency Theory. CRC Press (2009)

    Google Scholar 

  22. Sangiorgi, D., Walker, D.W.: On barbed equivalences in \(\pi \)-Calculus. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 292–304. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  23. Zuck, L.D., Prasad, S.: Limited mobility, eventual stability. In: Piterman, N., et al. (eds.) HVC 2015. LNCS, vol. 9434, pp. 139–154. Springer, Heidelberg (2015). doi:10.1007/978-3-319-26287-1_9

    Chapter  Google Scholar 

Download references

Acknowledgements

The authors thank the anonymous referees for their valuable suggestions.

Author information

Authors and Affiliations

  1. University of Illinois at Chicago, Chicago, USA

    Lenore D. Zuck

  2. Indian Institute of Technology Delhi, New Delhi, India

    Sanjiva Prasad

Authors
  1. Lenore D. Zuck
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sanjiva Prasad
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sanjiva Prasad .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute, Pozuelo de Alarcón, Madrid, Spain

    Pierre Ganty

  2. Università degli Studi di Firenze, Florence, Italy

    Michele Loreti

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Zuck, L.D., Prasad, S. (2016). A Switch, in Time. In: Ganty, P., Loreti, M. (eds) Trustworthy Global Computing. TGC 2015. Lecture Notes in Computer Science(), vol 9533. Springer, Cham. https://doi.org/10.1007/978-3-319-28766-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28766-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28765-2

  • Online ISBN: 978-3-319-28766-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation