Enhancing SVO Logic for Mobile IPv6 Security Protocols
Ilsun You1, Yoshiaki Hori2, and Kouichi
Sakurai2
1Korean Bible
University
16 Danghyun 2-gil, Nowon-gu
Seoul, Republic of Kroea
isyou@bible.ac.kr
2Kyushu University
Fukuoka-shi 819-0395, Japan
{hori,sakurai}@csce.kyushu-u.ac.jp
Abstract
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 cryptography.
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 flaws. 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.
Keywords: MIPv6
security, Formal verification, SVO logic
Journal of Wireless Mobile Networks,
Ubiquitous Computing, and Dependable Applications (JoWUA),
Vol. 2, No. 3, pp. 26-52, September
2011 [pdf]