{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:28:30Z","timestamp":1772836110119,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2013,9,1]],"date-time":"2013-09-01T00:00:00Z","timestamp":1377993600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a<jats:italic>process calculus<\/jats:italic>for<jats:italic>mobile ad hoc networks<\/jats:italic>which relies on an abstract behaviour-based multilevel<jats:italic>trust model<\/jats:italic>. 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<jats:italic>labelled bisimilarity<\/jats:italic>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<jats:italic>safety despite compromise<\/jats:italic>: compromised nodes cannot affect the rest of the network. A<jats:italic>non-interference<\/jats:italic>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.<\/jats:p>","DOI":"10.1007\/s00165-011-0210-7","type":"journal-article","created":{"date-parts":[[2011,11,16]],"date-time":"2011-11-16T13:04:31Z","timestamp":1321448671000},"page":"801-832","source":"Crossref","is-referenced-by-count":9,"title":["A calculus of trustworthy ad hoc networks"],"prefix":"10.1145","volume":"25","author":[{"given":"Massimo","family":"Merro","sequence":"first","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 degli Studi di Verona, Verona, Italy"}]},{"given":"Eleonora","family":"Sibilio","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 degli Studi di Verona, Verona, Italy"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/TMC.2006.170"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1504\/IJSSE.2008.018135"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abdul-Rahman A Hailes S (2000) Supporting trust in virtual communities. In: Proc annual Hawaii international conference on system sciences pp 6007\u20136016","DOI":"10.1109\/HICSS.2000.926814"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00010-5"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3020"},{"key":"e_1_2_1_2_6_2","unstructured":"Blaze M Feigenbaum J BLacy JE (1996) Decentralized trust management. In: Proc symposium on security and privacy pp 164\u2013173"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bell DE LaPadula LJ (1976) Secure computer system: unified exposition and multics interpretation. Technical Report MTR-2997 MITRE Corporation","DOI":"10.21236\/ADA023588"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"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\u2013500","DOI":"10.1007\/978-1-84800-328-6_19"},{"key":"e_1_2_1_2_10_2","unstructured":"Clausen T Qayuum A Jacquet P Laouitti A (2001) Optimized link state routing protocol. In: Proc IEEE international multiopic conference pp 250\u2013256"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"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\u2013173","DOI":"10.1007\/978-3-540-30538-5_14"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.01.001"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2007.04.006"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"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\u2013413","DOI":"10.1109\/ICPPW.2003.1240395"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/2699879.2699882"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.629493"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"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\u2013396","DOI":"10.1007\/3-540-45608-2_6"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Fournet C Gordon AD Maffeis S (2007) A type discipline for authorization in distributed systems. Proc IEEE computer security foundations symposium pp 31\u201348","DOI":"10.1109\/CSF.2007.7"},{"key":"e_1_2_1_2_19_2","volume-title":"Trust: making and breaking cooperative relations","author":"Gambetta D","year":"1990"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Ghassemi F Fokkink W Movaghar A (2008) Restricted broadcast process theory. In: Proc conf on software engineering and formal methods pp 345\u2013354","DOI":"10.1109\/SEFM.2008.25"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Ghassemi F Fokkink W Movaghar A (2009) Equational reasoning on ad hoc networks. In: Proc conf on fundamentals of software engineering pp 113\u2013128","DOI":"10.1007\/978-3-642-11623-0_6"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Goguen JA Meseguer J (1982) Security policies and security models. Proc conf on security and privacy pp 11\u201320","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Godskesen JC Nanz S (2009) Mobility models and behavioural equivalence for wireless networks. Proc conf on coordination models and languages pp 106\u2013122","DOI":"10.1007\/978-3-642-02053-7_6"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Godskesen JC (2007) A calculus for mobile ad hoc networks. Proc conf on coordination models and languages pp 132\u2013150","DOI":"10.1007\/978-3-540-72794-1_8"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Grandison TWA (2003) Trust management for internet applications. PhD thesis Department of Computing University of London","DOI":"10.1007\/3-540-44875-6_7"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11276-004-4744-y"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"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\u2013377","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2002.808417"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/1239776.1239778"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.dss.2005.05.019"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Johnson DB Maltz DA (1996) Dynamic source routing in ad hoc wireless networks. In: Proc conf on mobile computing pp 153\u2013181","DOI":"10.1007\/978-0-585-29603-6_5"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.01.023"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.11.010"},{"key":"e_1_2_1_2_34_2","volume-title":"Communication and concurrency","author":"Milner R","year":"1989"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Milner R Sangiorgi D (1992) Barbed bisimulation. In: Proc international colloquium on automata languages and programming pp 685\u2013695","DOI":"10.1007\/3-540-55719-9_114"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.036"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"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\u2013244","DOI":"10.1145\/190809.190336"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Perkins CE Belding-Royer EM (1999) Ad-hoc on-demand distance vector routing. Proc workshop on mobile computing systems and applications pp 90\u2013100","DOI":"10.1109\/MCSA.1999.749281"},{"key":"e_1_2_1_2_40_2","unstructured":"Park V Corson S (2001) Temporally ordered routing algorithm (tora) version 1 functional specification. Internet Draft IETF MANET"},{"key":"e_1_2_1_2_41_2","unstructured":"Pirzada AA Datta A McDonald C (2004) Trust based routing for ad hoc wireless networks. In: Proc IEEE international conference of networks pp 326\u2013330"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"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\u2013383","DOI":"10.1109\/SAINTW.2003.1210190"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TMC.2006.83"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357088"},{"key":"e_1_2_1_2_45_2","unstructured":"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\u2013127"},{"key":"e_1_2_1_2_46_2","unstructured":"Ryan PYA Schneider SA (1999) Process algebra and non-interference. In: Proc IEEE computer security foundations symposium pp 214\u2013227"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"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\u201384","DOI":"10.1109\/SAHCN.2005.1557064"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Song L Godskesen JC (2010) Probabilistic mobility models for mobile and wireless networks. In: Proc IFIP advances in information and communication technology pp 86\u2013100","DOI":"10.1007\/978-3-642-15240-5_7"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2004.842547"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.07.008"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/35.312842"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"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\u2013360","DOI":"10.1109\/ICNP.2004.1348124"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"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\u2013364","DOI":"10.1145\/268946.268975"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Zapata MG Asokan N (2002) Securing ad hoc routing protocols. In: Proc ACM workshop on wireless security pp 1\u201310","DOI":"10.1145\/570681.570682"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"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\u20132846","DOI":"10.1109\/INFCOM.2010.5462116"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0210-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0210-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0210-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T03:35:36Z","timestamp":1741923336000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0210-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9]]},"references-count":55,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["10.1007\/s00165-011-0210-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0210-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9]]}}}