Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Secure Two-Party Computation in Applied Pi-Calculus: Models and Verification Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

A Switch, in Time

verfasst von : Lenore D. Zuck, Sanjiva Prasad

Erschienen in: Trustworthy Global Computing

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Near-Optimal Scheduling for LTL with Future Discounting
Nächstes Kapitel Verification of Component-Based Systems via Predicate Abstraction and Simultaneous Set Reduction
Fußnoten
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
In [14], this relation was inductively defined using four axiom schema, two of which – reflexivity and transitivity — are implicit in temporal logic.
 
3
Actually, this property can be weakened to one requiring only that any such forwarding cycle will eventually get broken (see [23] for details).
 
Literatur
1.
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)
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)CrossRef
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)CrossRefMathSciNet
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)
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)CrossRef
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)CrossRef
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)
9.
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)
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)
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)CrossRefMathSciNetMATH
13.
Hughes, D.J.D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)
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)
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)CrossRef
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)
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)CrossRef
18.
Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)MATH
19.
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)
21.
Prasad, S.: Abstract switches: A distributed model of communication and computation. In: Perspectives in Concurrency Theory. CRC Press (2009)
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)CrossRef
23.
Metadaten
Titel
A Switch, in Time
verfasst von
Lenore D. Zuck
Sanjiva Prasad
Copyright-Jahr
2016
Buch
Trustworthy Global Computing

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

Electronic ISBN: 978-3-319-28766-9

Copyright-Jahr: 2016

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