Enhancing SVO logic for mobile IPv6 security protocols

Ilsun You, Yoshiaki Hori, Kouichi Sakurai

Research output: Contribution to journalArticle

19 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)26-52
Number of pages27
JournalJournal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications
Volume2
Issue number3
Publication statusPublished - Jan 1 2011

Fingerprint

Internet protocols
Network protocols
Public key cryptography
Mobile security
Defects

All Science Journal Classification (ASJC) codes

  • Computer Science (miscellaneous)
  • Computer Science Applications
  • Computer Networks and Communications

Cite this

Enhancing SVO logic for mobile IPv6 security protocols. / You, Ilsun; Hori, Yoshiaki; Sakurai, Kouichi.

In: Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, Vol. 2, No. 3, 01.01.2011, p. 26-52.

Research output: Contribution to journalArticle

@article{8853cfef23f548eab3fe50f141ca648a,
title = "Enhancing SVO logic for mobile IPv6 security protocols",
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.",
author = "Ilsun You and Yoshiaki Hori and Kouichi Sakurai",
year = "2011",
month = "1",
day = "1",
language = "English",
volume = "2",
pages = "26--52",
journal = "Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications",
issn = "2093-5374",
publisher = "Innovative Information Science & Technology Research Group (ISYOU)",
number = "3",

}

TY - JOUR

T1 - Enhancing SVO logic for mobile IPv6 security protocols

AU - You, Ilsun

AU - Hori, Yoshiaki

AU - Sakurai, Kouichi

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84863652807&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84863652807&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:84863652807

VL - 2

SP - 26

EP - 52

JO - Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications

JF - Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications

SN - 2093-5374

IS - 3

ER -