Abstract
In recent years, Mobile Ad hoc Networks (MANETs) have been focused with the development and the spread of mobile devices. However, MANETs have a security problem. MANETs do not have choke points like Firewalls. It is difficult for MANETs to have choke points because each mobile device in MANETs moves and because fixed routing does not exist. Moreover there are many kinds of attacks in MANETs such as packet sniffing, tampering, spoofing, etc. Gang Xu et al. proposed a method for constructing secure MANETs. The method is considered to prevent attacks against MANETs because each mobile device in MANETs uses Trusted Platform Module (TPM). TPM can become foundation of security because Tamper-resistance of TPM is difficult to analyze. However, Gang Xu et al. does not present the concrete protocol. This paper constructs the concrete protocol from the proposal of Gang Xu et al and verifies the concrete protocol by SPIN to construct secure protocol. This paper presents the process of constructing secure protocols from ideas of protocols. As a result of constructing and verifying the protocols, this paper concludes that the secure protocol cannot be constructed from the proposal of Gang Xu et al without the connection with certificate authority (CA) of public keys.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Xu, G., Borcea, C., Iftode, L.: A policy Enforcing Mechanism for Trusted Ad Hoc Networks. IEEE Transactions on Dependable and Secure Computing 8(3), 321–336 (2011)
Xu, G., Borcea, C., Iftode, L.: Satem: A Service-Aware Attestation Method toward Trusted Service Transaction. In: Proceedings of IEEE Symposium on Reliable Distributed System (SRDS), pp. 321–336 (2006)
Perkins, C.E., Royer, E.M.: Ad Hoc On-Demand Distance Vector Routing. In: Proceedings of Second IEEE Workshop Mobile Computing Systems and Applications, pp. 90–100 (1999)
Zhou, L., Yin, X., Wang, Z.: Protocol Security Testing with SPIN and TTCN-3. In: 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 511–519 (2011)
Holzmann, G.J.: The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5), 1–17 (1997)
Capkun, S., Hubaux, J., Buttyan, L.: Mobility Helps Security in Ad Hoc Networks. Proceedings of ACM MobiHOC, 46–56 (2003)
Ni, S.-Y., Tseng, Y.-C., Chen, Y.-S., Sheu, J.-P.: The Broadcast Storm Problem in a Mobile Ad Hoc Network. Proceedings of ACM/IEEE MobiCom, 151–162 (1999)
Xu, G., Iftode, L.: Locality Driven Key Management for Mobile Ad-Hoc Networks. In: Proceedings of First IEEE International Conference on Mobile Ad-Hoc Networks and Sensor Systems (MASS 2004), pp. 436–446 (2004)
Kong, J., Zerfos, P., Luo, H., Lu, S., Zhang, L.: Providing Robust and Ubiquitous Security Support for Mobile Ad-Hoc Networks. In: Proceedings of Ninth IEEE International Conference on Network Protocols (ICNP 2001), p. 251 (2001)
Capkun, S., Buttyan, L., Hubaux, J.P.: Self-Organized Public-Key Management for Mobile Ad Hoc Networks. IEEE Transaction on Mobile Computing 2(1), 52–64 (2003)
Xu, G., Borcea, C., Iftode, L.: Trusted Application-Centric Ad-Hoc Networks. In: Proceedings of Fourth IEEE International Conference on Mobile Ad-Hoc Networks and Sensor Systems, MASS 2007 (2007)
Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. Theoretical Computer Science 299(1-3), 451–475 (2003)
Trusted Computing Group: TCG 1.1b Specifications (2010), https://www.trustedcomputinggroup.org.home
Trusted Computing Group-Mobile Phone Working Group: Use Case Scenarios v2.7 (2005)
Ben-Ari, M.: Principles of the Spin Model Checker (2008)
SPIN website, http://spinroot.com/spin/whatispin.html
Trusted Computing Group, http://www.trustedcomputinggroup.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Kimura, N., Yoshiura, N. (2013). Construction and Verification of Mobile Ad Hoc Network Protocols. In: Wang, G., Ray, I., Feng, D., Rajarajan, M. (eds) Cyberspace Safety and Security. CSS 2013. Lecture Notes in Computer Science, vol 8300. Springer, Cham. https://doi.org/10.1007/978-3-319-03584-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-03584-0_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03583-3
Online ISBN: 978-3-319-03584-0
eBook Packages: Computer ScienceComputer Science (R0)