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 be cause 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.pro posed a method for constructing secure MANETs.The method is con sidered 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 proto cols 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.
Mobile Ad Hoc Network Model Checking Protocol Verification SPIN
Natsuki Kimura Noriaki Yoshiura
Department of Information and Computer Science,Saitama University,255,Shimo-ookubo Urawa-ku,Saitama City,Japan
国际会议
The 5th International Symposium on Cyberspace Safety and Security ( CSS2013)(第五届国际网络空间安全和安保研讨会)
张家界
英文
198-212
2013-11-13（万方平台首次上网日期，不代表论文的发表时间）