期刊名称：Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications
印刷版ISSN：2093-5374
电子版ISSN：2093-5382
出版年度：2011
卷号：2
期号：3
页码：26-52
出版社：Innovative Information Science & Technology Research Group
摘要：In order to protect Mobile Internet Protocol Version 6 (MIPv6), considerable researches have been made, consequently followed by various security protocols, which are based on public key cryptog- raphy. Especially, depending on a proper address based public key method, these protocols use each node's address as a public key certificate to authenticate its public key because no global public key infrastructure is available in MIPv6 environments. In addition, they execute an appropriate address test to check if a node exists at its claimed address. With such security features, the protocols prevent critical attacks including redirect, man-in-the middle, and denial of service ones. On the other hand, it is clearly of paramount importance to formally evaluate the MIPv6 security protocols to design them without .aws. Unfortunately, there is lack of the formal verification method to precisely reason about their correctness while considering their unique security properties to our best knowledge. In this paper, we propose an extended SVO logic for the thorough verification of the MIPv6 security protocols. Then, we show its effectiveness by applying the proposed logic to four security protocols.
关键词：MIPv6 security; Formal verification; SVO logic
