Abstract
We propose a process calculus for mobile ad hoc networks which relies on an abstract behaviour-based multilevel trust model. The operational semantics of the calculus is given in terms of a labelled transition system, where actions are executed at a certain security level. We define a labelled bisimilarity over networks parameterised on security levels. Our bisimilarity is a congruence and an efficient proof method for an appropriate variant of barbed congruence, a standard contextually-defined program equivalence. Communications in the calculus are safe with respect to the security levels of the involved parties. In particular, we ensure safety despite compromise: compromised nodes cannot affect the rest of the network. A non-interference result is also proved in terms of information flow. Finally, we use our calculus to provide formal descriptions of trust-based versions of both a routing protocol and a leader election protocol for ad hoc networks.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ács G, Buttyán L, Vajda I (2006) Provably secure on-demand source routing in mobile ad hoc networks. IEEE Trans Mob Comput 5(11): 1533–1546
Aivaloglou E, Gritzalis S, Skianis C (2008) Trust establishment in sensor networks: behaviour-based, certificate-based and a combinational approach. Int J Syst Syst Eng 1(1–2): 128–148
Abdul-Rahman A, Hailes S (2000) Supporting trust in virtual communities. In: Proc annual Hawaii international conference on system sciences, pp 6007–6016
Boudol G, Castellani I (2002) Noninterference for concurrent programs and thread systems. Theor Comput Sci 281(1–2): 109–130
Bodei C, Degano P, Nielson F, Nielson HR (2001) Static analysis for the pi-calculus with applications to security. Inf Comput 168(1): 68–92
Blaze M, Feigenbaum J, BLacy JE (1996) Decentralized trust management. In: Proc symposium on security and privacy, pp 164–173
Bell DE, LaPadula LJ (1976) Secure computer system: unified exposition and multics interpretation. Technical Report MTR-2997, MITRE Corporation
Bhargavan K, Obradovic D, Gunter CA (2002) Formal verification of standards for distance vector routing protocols. J ACM 49(4): 538–576
Balakrishnan V, Varadharajan V, Tupakula U (2009) Trust management in mobile ad hoc networks: guide to wireless ad hoc networks. In: Proc conf computer communications and networks, pp 473–500
Clausen T, Qayuum A, Jacquet P, Laouitti A (2001) Optimized link state routing protocol. In: Proc IEEE international multiopic conference, pp 250–256
Carbone M, Nielsen M, Sassone V (2004) A calculus for trust management. In: Proc. conf. on foundations of software technology and theoretical computer science, pp 161–173
Crafa S, Rossi S (2007) Controlling information release in the pi-calculus. Inf Comput 205(8): 1235–1273
Dijiang H, Deep M (2008) A secure group key management scheme for hierarchical mobile ad hoc networks. Ad Hoc Netw 6(4): 560–577
Di Pietro R, Mancini LV, Law YW, Etalle S, Havinga PJM (2003) LKHW: a directed diffusion-based secure multicast scheme for wireless sensor networks. In: Proc international conference on parallel processing workshops, pp 397–413
Focardi R, Gorrieri R (1995) A classification of security properties for process algebras. J Comput Secur 3(1): 5–33
Focardi R, Gorrieri R (1997) The compositional security checker: a tool for the verification of information flow security properties. IEEE Trans Softw Eng 27(3): 550–571
Focardi R, Gorrieri R (2001) Classification of security properties (part i: information flow). In: Proc conf on foundations of security analysis and design, pp 331–396
Fournet C, Gordon AD, Maffeis S (2007) A type discipline for authorization in distributed systems. Proc IEEE computer security foundations symposium, pp 31–48
Gambetta D (1990) Trust: making and breaking cooperative relations. Basil Blackwell, Oxford
Ghassemi F, Fokkink W, Movaghar A (2008) Restricted broadcast process theory. In: Proc conf on software engineering and formal methods, pp 345–354
Ghassemi F, Fokkink W, Movaghar A (2009) Equational reasoning on ad hoc networks. In: Proc conf on fundamentals of software engineering, pp 113–128
Goguen JA, Meseguer J (1982) Security policies and security models. Proc conf on security and privacy, pp 11–20
Godskesen JC, Nanz S (2009) Mobility models and behavioural equivalence for wireless networks. Proc conf on coordination models and languages, pp 106–122
Godskesen JC (2007) A calculus for mobile ad hoc networks. Proc conf on coordination models and languages, pp 132–150
Grandison TWA (2003) Trust management for internet applications. PhD thesis, Department of Computing, University of London
Hu Y, Perrig A, Johnson DB (2005) Ariadne: a secure on-demand routing protocol for ad hoc networks. Wirel Netw 11(1–2): 21–38
Heintze N, Riecke JG (1998) The SLam calculus: programming with secrecy and integrity. In: Conf record ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 365–377
Intanagonwiwat C, Govindan R, Estrin D, Heidemann J, Silva F (2003) Directed diffusion for wireless sensor networking. IEEE/ACM Trans Netw 11(1): 2–16
Jøsang A, Gray E, Kinateder M (2006) Simplification and analysis of transitive trust networks. Web Intell Agent Syst 4(2): 139–161
Jøsang A, Ismail R, Boyd C (2006) A survey of trust and reputation systems for online service provision. Decis Support Syst 43(2): 618–644
Johnson DB, Maltz DA (1996) Dynamic source routing in ad hoc wireless networks. In: Proc conf on mobile computing, pp 153–181
Lanese I, Sangiorgi D (2010) An operational semantics for a calculus for wireless systems. Theor Comput Sci 411(19): 1928–1948
Merro M (2009) An observational theory for mobile ad hoc networks. Inf Comput 207(2): 194–208
Milner R (1989) Communication and concurrency. Prentice Hall, Cambridge
Milner R, Parrow J, Walker D (1992) A calculus of mobile processes (parts I and II). Inf Comput 100: 1–77
Milner R, Sangiorgi D (1992) Barbed bisimulation. In: Proc international colloquium on automata, languages and programming, pp 685–695
Nanz S, Hankin C (2006) A framework for security analysis of mobile wireless networks. Theor Comput Sci 367(1–2): 203–227
Perkins CE, Bhagwat P (1994) Highly dynamic destination-sequenced distance-vector routing (DSDV) for mobile computers. Proc ACM conference on communications architectures, protocols and applications, pp 234–244
Perkins CE, Belding-Royer EM (1999) Ad-hoc on-demand distance vector routing. Proc workshop on mobile computing systems and applications, pp 90–100
Park V, Corson S (2001) Temporally ordered routing algorithm (tora) version 1, functional specification. Internet Draft, IETF MANET
Pirzada AA, Datta A, McDonald C (2004) Trust based routing for ad hoc wireless networks. In: Proc IEEE international conference of networks, pp 326–330
Papadimitratos P, Haas ZJ (2003) Secure link state routing for mobile ad hoc networks. In: Proc symposium on applications and the internet workshops, pp 379–383
Pirzada AA, McDonald C, Datta A (2006) Performance comparison of trust-based reactive routing protocols. IEEE Trans Mob Comput 5(6): 695–710
Reitman RP, Andrews GR (1980) An axiomatic approach to information flow in programs. ACM Trans Program Lang Syst 2(1): 56–76
Roman R, Fernandez-Zago MC, Lopez J, Hsiao-Hwa C (2009) Trust and reputation systems for wireless sensor networks. In: Proc security and privacy in mobile and wireless networking, pp 105–127
Ryan PYA, Schneider SA (1999) Process algebra and non-interference. In: Proc IEEE computer security foundations symposium, pp 214–227
Shehab M, Bertino E, Ghafoor A (2005) Efficient hierarchical key generation and key diffusion for sensor networks. In: Proc IEEE communications society conference on sensor and ad hoc communications and networks, pp 76–84
Song L, Godskesen JC (2010) Probabilistic mobility models for mobile and wireless networks. In: Proc IFIP advances in information and communication technology, pp 86–100
Sanzgiri K, LaFlamme D, Dahill B, Levine BN, Shields C, Belding-Royer EM (2005) Authenticated routing for ad hoc networks. IEEE J Selected Areas Commun 23(3): 598–610
Singh A, Ramakrishnan CR, Smolka SA (2010) A process calculus for mobile ad hoc networks. Sci Comput Program 75: 440–469
Sandhu RS, Samarati P (1994) Access control: principles and practice. IEEE Commun Mag 32: 40–48
Vasudevan S, Kurose J, Towsley D (2004) Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Proc IEEE international conference on network protocols, pp 350–360
Volpano DM, Smith G (1998) Secure information flow in a multi-threaded imperative language. In: Conf record ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 355–364
Zapata MG, Asokan N (2002) Securing ad hoc routing protocols. In: Proc ACM workshop on wireless security, pp 1–10
Zhang C, Zhu X, Song Y, Fang Y (2010) A formal study of trust-based routing in wireless ad hoc networks. In: Proc IEEE international conference on computer communications, pp 2838–2846
Author information
Authors and Affiliations
Corresponding author
Additional information
Joachim Parrow
Rights and permissions
About this article
Cite this article
Merro, M., Sibilio, E. A calculus of trustworthy ad hoc networks. Form Asp Comp 25, 801–832 (2013). https://doi.org/10.1007/s00165-011-0210-7
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-011-0210-7