Formal verification of secure ad-hoc network routing protocols using deductive model-checking

L. Buttyán, Ta Vinh Thong

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for ad-hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a formal verification method for secure ad-hoc network routing protocols that helps increasing the confidence in a protocol by providing an analysis framework that is more systematic, and hence, less error-prone than the informal analysis. Our approach is based on a new process calculus that we specifically developed for secure ad-hoc network routing protocols and a deductive proof technique. The novelty of this approach is that contrary to prior attempts to formal verification of secure ad-hoc network routing protocols, our verification method can be made fully automated.

Original languageEnglish
Title of host publication2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010
DOIs
Publication statusPublished - 2010
Event2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010 - Budapest, Hungary
Duration: Oct 13 2010Oct 15 2010

Other

Other2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010
CountryHungary
CityBudapest
Period10/13/1010/15/10

Fingerprint

Network routing
Model checking
Ad hoc networks
Routing protocols
Formal verification
Network protocols
Defects

ASJC Scopus subject areas

  • Computer Networks and Communications

Cite this

Buttyán, L., & Vinh Thong, T. (2010). Formal verification of secure ad-hoc network routing protocols using deductive model-checking. In 2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010 [5678752] https://doi.org/10.1109/WMNC.2010.5678752

Formal verification of secure ad-hoc network routing protocols using deductive model-checking. / Buttyán, L.; Vinh Thong, Ta.

2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010. 2010. 5678752.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Buttyán, L & Vinh Thong, T 2010, Formal verification of secure ad-hoc network routing protocols using deductive model-checking. in 2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010., 5678752, 2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010, Budapest, Hungary, 10/13/10. https://doi.org/10.1109/WMNC.2010.5678752
Buttyán L, Vinh Thong T. Formal verification of secure ad-hoc network routing protocols using deductive model-checking. In 2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010. 2010. 5678752 https://doi.org/10.1109/WMNC.2010.5678752
Buttyán, L. ; Vinh Thong, Ta. / Formal verification of secure ad-hoc network routing protocols using deductive model-checking. 2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010. 2010.
@inproceedings{10f2246d6fbc41beb0f54bab2cbe3b00,
title = "Formal verification of secure ad-hoc network routing protocols using deductive model-checking",
abstract = "Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for ad-hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a formal verification method for secure ad-hoc network routing protocols that helps increasing the confidence in a protocol by providing an analysis framework that is more systematic, and hence, less error-prone than the informal analysis. Our approach is based on a new process calculus that we specifically developed for secure ad-hoc network routing protocols and a deductive proof technique. The novelty of this approach is that contrary to prior attempts to formal verification of secure ad-hoc network routing protocols, our verification method can be made fully automated.",
author = "L. Butty{\'a}n and {Vinh Thong}, Ta",
year = "2010",
doi = "10.1109/WMNC.2010.5678752",
language = "English",
isbn = "9781424484317",
booktitle = "2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010",

}

TY - GEN

T1 - Formal verification of secure ad-hoc network routing protocols using deductive model-checking

AU - Buttyán, L.

AU - Vinh Thong, Ta

PY - 2010

Y1 - 2010

N2 - Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for ad-hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a formal verification method for secure ad-hoc network routing protocols that helps increasing the confidence in a protocol by providing an analysis framework that is more systematic, and hence, less error-prone than the informal analysis. Our approach is based on a new process calculus that we specifically developed for secure ad-hoc network routing protocols and a deductive proof technique. The novelty of this approach is that contrary to prior attempts to formal verification of secure ad-hoc network routing protocols, our verification method can be made fully automated.

AB - Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for ad-hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a formal verification method for secure ad-hoc network routing protocols that helps increasing the confidence in a protocol by providing an analysis framework that is more systematic, and hence, less error-prone than the informal analysis. Our approach is based on a new process calculus that we specifically developed for secure ad-hoc network routing protocols and a deductive proof technique. The novelty of this approach is that contrary to prior attempts to formal verification of secure ad-hoc network routing protocols, our verification method can be made fully automated.

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

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

U2 - 10.1109/WMNC.2010.5678752

DO - 10.1109/WMNC.2010.5678752

M3 - Conference contribution

SN - 9781424484317

BT - 2010 3rd Joint IFIP Wireless and Mobile Networking Conference, WMNC 2010

ER -