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]