Abstract
Routing protocols aim at establishing a route between distant nodes in ad hoc networks. Secured versions of routing protocols have been proposed to provide more guarantees on the resulting routes, and some of them have been designed to protect the privacy of the users.
In this paper, we propose a framework for analysing privacy-type properties for routing protocols. We use a variant of the applied-pi calculus as our basic modelling formalism. More precisely, using the notion of equivalence between traces, we formalise three security properties related to privacy, namely indistinguishability, unlinkability, and anonymity. We study the relationship between these definitions and we illustrate them using two versions of the ANODR routing protocol.
This work has been partially supported by the project JCJC VIP ANR-11-JS02-006.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages, POPL 2001, pp. 104–115. ACM Press (2001)
Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. In: Proc. 4th Conference on Computer and Communications Security, CCS 1997, pp. 36–47. ACM Press (1997)
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proc. 23rd Computer Security Foundations Symposium, CSF 2010, pp. 107–121. IEEE Computer Society Press (2010)
Armando, A., Carbone, R., Compagna, L., Cuéllar, J., Tobarra, M.L.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps. In: Proc. of the 6th ACM Workshop on Formal Methods in Security Engineering, FMSE 2008, pp. 1–10. ACM (2008)
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: 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)
Arnaud, M., Cortier, V., Delaune, S.: Modeling and verifying ad hoc routing protocols. In: Proc. 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pp. 59–74. IEEE Computer Society Press (July 2010)
Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. IEEE Comp. Soc. Press (2008)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. 14th Computer Security Foundations Workshop, CSFW 2001. IEEE Comp. Soc. Press (2001)
Bruso, M., Chatzikokolakis, K., den Hartog, J.: Formal verification of privacy for RFID systems. In: Proc. 23rd Computer Security Foundations Symposium, CSF 2010, IEEE Computer Society Press (2010)
Chrétien, R., Delaune, S.: Formal analysis of privacy for routing protocols in mobile ad hoc networks. Research Report LSV-12-21, Laboratoire Spécification et Vérification, ENS Cachan, France, 24 pages (December 2012)
Cortier, V., Degrieck, J., Delaune, S.: Analysing Routing Protocols: Four Nodes Topologies Are Sufficient. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 30–50. Springer, Heidelberg (2012)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security (4), 435–487 (2008)
Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Proc. ACM Workshop on Formal Methods in Security Engineering, FMSE 2005, pp. 63–72. ACM (2005)
Hu, Y.-C., Perrig, A., Johnson, D.: Ariadne: A Secure On-Demand Routing Protocol for Ad Hoc Networks. Wireless Networks 11, 21–38 (2005)
Kong, J., Hong, X.: ANODR: anonymous on demand routing with untraceable routes for mobile ad-hoc networks. In: Proc. 4th ACM Interational Symposium on Mobile Ad Hoc Networking and Computing, MobiHoc 2003. ACM (2003)
Mauw, S., Verschuren, J.H.S., de Vink, E.P.: A Formalization of Anonymity and Onion Routing. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 109–124. Springer, Heidelberg (2004)
Nanz, S., Hankin, C.: A Framework for Security Analysis of Mobile Wireless Networks. Theoretical Computer Science 367(1), 203–227 (2006)
Papadimitratos, P., Haas, Z.: Secure routing for mobile ad hoc networks. In: Proc. SCS Communication Networks and Distributed Systems Modelling Simulation Conference, CNDS (2002)
Serjantov, A., Danezis, G.: Towards an Information Theoretic Metric for Anonymity. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol. 2482, pp. 41–53. Springer, Heidelberg (2003)
Song, R., Korba, L., Lee, G.: AnonDSR: Efficient anonymous dynamic source routing for mobile ad-hoc networks. In: Proc. ACM Workshop on Security of Ad Hoc and Sensor Networks, SASN 2005. ACM (2005)
Zapata, M.G., Asokan, N.: Securing ad hoc routing protocols. In: Proc. 1st ACM Workshop on Wireless SEcurity, WiSE 2002, pp. 1–10. ACM (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chrétien, R., Delaune, S. (2013). Formal Analysis of Privacy for Routing Protocols in Mobile Ad Hoc Networks. In: Basin, D., Mitchell, J.C. (eds) Principles of Security and Trust. POST 2013. Lecture Notes in Computer Science, vol 7796. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36830-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-36830-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36829-5
Online ISBN: 978-3-642-36830-1
eBook Packages: Computer ScienceComputer Science (R0)