On automating the verification of secure ad-hoc network routing protocols

Ta Vinh Thong, L. Buttyán

Research output: Contribution to journalArticle

2 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 fully automatic 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 method is based on a deductive proof technique and a backward reachability approach. The main novelty of this approach compared to the prior works is that beside providing expressive semantics and syntax for modelling and specifying secure routing protocols, it assumes an arbitrary topology, and a strong attacker model.

Original languageEnglish
Pages (from-to)2611-2635
Number of pages25
JournalTelecommunication Systems
Volume52
Issue number4
DOIs
Publication statusPublished - Apr 2013

Fingerprint

Network routing
Ad hoc networks
Routing protocols
Semantics
Topology
Network protocols
Defects

Keywords

  • Automated security verification
  • Cryptography
  • Formal analysis
  • Mobile ad-hoc networks
  • Process calculus
  • Secure routing protocols
  • Security
  • Wireless communication

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Cite this

On automating the verification of secure ad-hoc network routing protocols. / Thong, Ta Vinh; Buttyán, L.

In: Telecommunication Systems, Vol. 52, No. 4, 04.2013, p. 2611-2635.

Research output: Contribution to journalArticle

@article{ee319cb0f00c4a4fbd4e3e64caa783cf,
title = "On automating the verification of secure ad-hoc network routing protocols",
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 fully automatic 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 method is based on a deductive proof technique and a backward reachability approach. The main novelty of this approach compared to the prior works is that beside providing expressive semantics and syntax for modelling and specifying secure routing protocols, it assumes an arbitrary topology, and a strong attacker model.",
keywords = "Automated security verification, Cryptography, Formal analysis, Mobile ad-hoc networks, Process calculus, Secure routing protocols, Security, Wireless communication",
author = "Thong, {Ta Vinh} and L. Butty{\'a}n",
year = "2013",
month = "4",
doi = "10.1007/s11235-011-9592-3",
language = "English",
volume = "52",
pages = "2611--2635",
journal = "Telecommunication Systems",
issn = "1018-4864",
publisher = "Springer Netherlands",
number = "4",

}

TY - JOUR

T1 - On automating the verification of secure ad-hoc network routing protocols

AU - Thong, Ta Vinh

AU - Buttyán, L.

PY - 2013/4

Y1 - 2013/4

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 fully automatic 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 method is based on a deductive proof technique and a backward reachability approach. The main novelty of this approach compared to the prior works is that beside providing expressive semantics and syntax for modelling and specifying secure routing protocols, it assumes an arbitrary topology, and a strong attacker model.

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 fully automatic 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 method is based on a deductive proof technique and a backward reachability approach. The main novelty of this approach compared to the prior works is that beside providing expressive semantics and syntax for modelling and specifying secure routing protocols, it assumes an arbitrary topology, and a strong attacker model.

KW - Automated security verification

KW - Cryptography

KW - Formal analysis

KW - Mobile ad-hoc networks

KW - Process calculus

KW - Secure routing protocols

KW - Security

KW - Wireless communication

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

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

U2 - 10.1007/s11235-011-9592-3

DO - 10.1007/s11235-011-9592-3

M3 - Article

VL - 52

SP - 2611

EP - 2635

JO - Telecommunication Systems

JF - Telecommunication Systems

SN - 1018-4864

IS - 4

ER -