{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:19:14Z","timestamp":1762521554056},"reference-count":0,"publisher":"National Library of Serbia","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2013]]},"abstract":"<jats:p>Mobile Ad Hoc Networks (MANETs) are formed dynamically by mobile nodes\n   without the support of prior stationary infrastructures. In such networks,\n   routing protocols, particularly secure ones are always the essential parts.\n   Ariadne, an efficient and well-known on-demand secure protocol of MANETs,\n   mainly concerns about how to prevent a malicious node from compromising the\n   route. In this paper, we apply the method of process algebra Communicating\n   Sequential Processes (CSP) to model and reason about the Ariadne protocol,\n   focusing on the process of its route discovery. In our framework, we consider\n   the communication entities as CSP processes, including the initiator, the\n   intermediate nodes and the target. Moreover, we also propose an intruder\n   model allowing the intruder to learn and deduce much information from the\n   protocol and the environment. Note that the modeling approach is also\n   applicable to other protocols, which are based on the on-demand routing\n   protocols and have the route discovery process. Finally, we use PAT, a model\n   checker for CSP, to verify whether the model caters for the specification and\n   the non-trivial secure properties, e.g. nonexistence of fake path. Three case\n   studies are given and the verification results naturally demonstrate that the\n   fake routing attacks may be present in the Ariadne protocol.<\/jats:p>","DOI":"10.2298\/csis120601009w","type":"journal-article","created":{"date-parts":[[2013,1,17]],"date-time":"2013-01-17T08:44:20Z","timestamp":1358412260000},"page":"393-421","source":"Crossref","is-referenced-by-count":3,"title":["Modeling and verifying the Ariadne protocol using process algebra"],"prefix":"10.2298","volume":"10","author":[{"given":"Xi","family":"Wu","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute, East China Normal University, Shanghai, China"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute, East China Normal University, Shanghai, China"}]},{"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[{"name":"School of Computing, National University of Singapore, Singapore"}]},{"given":"Zheng","family":"Wang","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, China"}]},{"given":"Liu","family":"Si","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign"}]}],"member":"1078","container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T08:30:53Z","timestamp":1685349053000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02141300009W"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013]]}},"URL":"https:\/\/doi.org\/10.2298\/csis120601009w","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}