Paper 2012/139

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

Ta Vinh Thong

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 aws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a formal verication method for secure ad-hoc network routing protocols that helps increasing the condence 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 algebra that we specically 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 verication of secure ad-hoc network routing protocols, our verication method can be made fully automated, and provides expressiveness for explicitly modelling cryptography privitives

Note: Corrected many typos, english grammar, and notions, notations, formulations. Removed unnecessary sentences and paragraphs.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. This report is the extended and revised version of our 6 pages conference paper (mentioned in the paper))
Keywords
Automated verificationad-hoc network routing protocolsformal methodprocess algebracryptographysecurity
Contact author(s)
thong @ crysys hu
History
2013-08-15: last of 4 revisions
2012-03-22: received
See all versions
Short URL
https://ia.cr/2012/139
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2012/139,
      author = {Ta Vinh Thong},
      title = {Formal verication of secure ad-hoc network routing protocols using deductive model-checking},
      howpublished = {Cryptology ePrint Archive, Paper 2012/139},
      year = {2012},
      note = {\url{https://eprint.iacr.org/2012/139}},
      url = {https://eprint.iacr.org/2012/139}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.