Construction and Verification of Mobile Ad Hoc Network Protocols

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.