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

Levente Buttyán, Ta Vinh Thong

Research output: Contribution to journalArticle

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
Pages (from-to)31-43
Number of pages13
JournalPeriodica Polytechnica Electrical Engineering
Volume55
Issue number1-2
DOIs
Publication statusPublished - Jan 1 2011

Keywords

  • Ad-hoc activals
  • Automatic reasoning
  • Formal verification
  • Process calculus
  • Routing protocol
  • Security

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Formal verification of secure ad-hoc network routing protocols using deductive model-checking'. Together they form a unique fingerprint.

  • Cite this