Abstract
We suggest a Calculus for Mobile Ad Hoc Networks,CMAN. A node in a network is a process equipped with a location, it may communicate with other nodes using synchronous spatially oriented broadcast where only the current neighbors receive the message. Nodes may autonomously change their neighbor relationship and thereby change the network topology. We define a natural reduction semantics and a reduction congruence as well as a labeled transition semantics and prove a weak contextual bisimulation to be a sound and complete co-inductive characterization of the reduction congruence. Finally, we apply CMAN on a small example of a cryptographic routing protocol.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Blanchet, B.: Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM 52(1), 102–146 (2005)
Abadi, M., Fournet, C.: Mobile vales, new names, and secure communication. In: Nielson, H.R. (ed.) 28th ACM Symposium on Principles of Programming Languages, London, January 2001, pp. 104–115. ACM Press, New York (2001)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, Springer, Berlin Germany (1998)
Castagna, G., Vitek, J., Nardelli, F.Z.: The seal calculus. Information and Computation 201(1), 1–51 (2005)
Ene, C., Muntean, T.: A broadcast-based calculus for communicating systems. In: Müller, F. (ed.) HIPS 2001. LNCS, vol. 2026, Springer, Heidelberg (2001)
Godskesen, J.Chr.: Formal verification of the ARAN protocol using the applied π-calculus. In: WITS. Proceedings of Sixth International IFIP WG 1.7 Workshop on Issuses in the Theory of Security, Vienna, Austria, March 2006, pp. 99–113 (2006)
Godskesen, J.Chr., Hildebrandt, T.: Extending Howe’s method to early bisimulations for typed mobile embedded resources with local names. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 140–151. Springer, Heidelberg (2005)
Merro, M.: An observational theory for mobile ad hoc networks. Electron. Notes Theor. Comput. Sci. 173, 275–293 (2007)
Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. Electr. Notes Theor. Comput. Sci. 158, 331–353 (2006)
Milner, R.: Functions as processes. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 167–180. Springer, Heidelberg (1990)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I/II. Journal of Information and Computation 100, 1–77 (1992)
Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) Automata, Languages and Programming. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992)
Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theor. Comput. Sci. 367(1), 203–227 (2006)
De Nicola, R., Gorla, D., Pugliese, R.: Basic observables for a calculus for global computing. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1226–1238. Springer, Heidelberg (2005)
Ostrovsky, K., Prasad, K.V.S., Taha, W.: Towards a primitive higher order calculus of broadcasting systems. In: PPDP ’02. Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, pp. 2–13. ACM Press, New York (2002)
Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program 25(2-3), 285–327 (1995)
Riely, J., Hennessy, M.: A typed language for distributed mobile processes (extended abstract). In: Conference Record of POPL ’98. The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, pp. 378–390. ACM Press, New York (1998)
Sanzgiri, K., LaFlamme, D., Dahill, B., Levine, B.N., Shields, C., Belding-Royer, E.M.: Authenticated routing for ad hoc networks. IEEE Journal on Selected Areas in Communication 23(3), 598–610. special issue on Wireless Ad hoc Networks (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Godskesen, J.C. (2007). A Calculus for Mobile Ad Hoc Networks. In: Murphy, A.L., Vitek, J. (eds) Coordination Models and Languages. COORDINATION 2007. Lecture Notes in Computer Science, vol 4467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72794-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-72794-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72793-4
Online ISBN: 978-3-540-72794-1
eBook Packages: Computer ScienceComputer Science (R0)