Verification of secure network protocols in uncertain environments

Sarah Damiani, Christopher Griffin, Shashi Phoha, Stephan Racunas, Christopher Rogan

Research output: Contribution to journalArticle

Abstract

In this paper, we present a method for protocol checking and verification using discrete event control. By protocol checking and verification, we mean verifying that a protocol is logically correct, that it does not cause deadlocks, and that it has been defined to respond to uncontrollable events that may occur in a system implementing it. Our approach differs from those previously suggested in two key ways. We extend the elementary theory of discrete event control to allow us to model more complicated protocols, including protocols relying on arbitrary counting models. We then present a maximum probability method for analyzing a protocol's ability to react to a priori unspecified events. Unlike current protocol modeling, we use a pushdown automata for modeling protocols. This allows us to model protocols with greater fidelity. Our methods are illustrated using a simple two-level hierarchical protocol that defines the behavior of ad hoc wireless network nodes as they attempt to establish a secure connection. As wireless networks become more prevalent throughout the world, the off-line verification of protocols before they are implemented will help ensure that wireless network protocols are robust to security intrusions before they are deployed into the field. This will save time and money in the long run.

Original languageEnglish (US)
Pages (from-to)221-227
Number of pages7
JournalInternational Journal of Wireless Information Networks
Volume13
Issue number3
DOIs
StatePublished - Jul 1 2006

Fingerprint

Network protocols
Wireless networks
Wireless ad hoc networks
Computer simulation

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Computer Networks and Communications
  • Electrical and Electronic Engineering

Cite this

@article{7be3bca21cd94defae7e04d4385ea449,
title = "Verification of secure network protocols in uncertain environments",
abstract = "In this paper, we present a method for protocol checking and verification using discrete event control. By protocol checking and verification, we mean verifying that a protocol is logically correct, that it does not cause deadlocks, and that it has been defined to respond to uncontrollable events that may occur in a system implementing it. Our approach differs from those previously suggested in two key ways. We extend the elementary theory of discrete event control to allow us to model more complicated protocols, including protocols relying on arbitrary counting models. We then present a maximum probability method for analyzing a protocol's ability to react to a priori unspecified events. Unlike current protocol modeling, we use a pushdown automata for modeling protocols. This allows us to model protocols with greater fidelity. Our methods are illustrated using a simple two-level hierarchical protocol that defines the behavior of ad hoc wireless network nodes as they attempt to establish a secure connection. As wireless networks become more prevalent throughout the world, the off-line verification of protocols before they are implemented will help ensure that wireless network protocols are robust to security intrusions before they are deployed into the field. This will save time and money in the long run.",
author = "Sarah Damiani and Christopher Griffin and Shashi Phoha and Stephan Racunas and Christopher Rogan",
year = "2006",
month = "7",
day = "1",
doi = "10.1007/s10776-006-0034-1",
language = "English (US)",
volume = "13",
pages = "221--227",
journal = "International Journal of Wireless Information Networks",
issn = "1068-9605",
publisher = "Springer New York",
number = "3",

}

Verification of secure network protocols in uncertain environments. / Damiani, Sarah; Griffin, Christopher; Phoha, Shashi; Racunas, Stephan; Rogan, Christopher.

In: International Journal of Wireless Information Networks, Vol. 13, No. 3, 01.07.2006, p. 221-227.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Verification of secure network protocols in uncertain environments

AU - Damiani, Sarah

AU - Griffin, Christopher

AU - Phoha, Shashi

AU - Racunas, Stephan

AU - Rogan, Christopher

PY - 2006/7/1

Y1 - 2006/7/1

N2 - In this paper, we present a method for protocol checking and verification using discrete event control. By protocol checking and verification, we mean verifying that a protocol is logically correct, that it does not cause deadlocks, and that it has been defined to respond to uncontrollable events that may occur in a system implementing it. Our approach differs from those previously suggested in two key ways. We extend the elementary theory of discrete event control to allow us to model more complicated protocols, including protocols relying on arbitrary counting models. We then present a maximum probability method for analyzing a protocol's ability to react to a priori unspecified events. Unlike current protocol modeling, we use a pushdown automata for modeling protocols. This allows us to model protocols with greater fidelity. Our methods are illustrated using a simple two-level hierarchical protocol that defines the behavior of ad hoc wireless network nodes as they attempt to establish a secure connection. As wireless networks become more prevalent throughout the world, the off-line verification of protocols before they are implemented will help ensure that wireless network protocols are robust to security intrusions before they are deployed into the field. This will save time and money in the long run.

AB - In this paper, we present a method for protocol checking and verification using discrete event control. By protocol checking and verification, we mean verifying that a protocol is logically correct, that it does not cause deadlocks, and that it has been defined to respond to uncontrollable events that may occur in a system implementing it. Our approach differs from those previously suggested in two key ways. We extend the elementary theory of discrete event control to allow us to model more complicated protocols, including protocols relying on arbitrary counting models. We then present a maximum probability method for analyzing a protocol's ability to react to a priori unspecified events. Unlike current protocol modeling, we use a pushdown automata for modeling protocols. This allows us to model protocols with greater fidelity. Our methods are illustrated using a simple two-level hierarchical protocol that defines the behavior of ad hoc wireless network nodes as they attempt to establish a secure connection. As wireless networks become more prevalent throughout the world, the off-line verification of protocols before they are implemented will help ensure that wireless network protocols are robust to security intrusions before they are deployed into the field. This will save time and money in the long run.

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

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

U2 - 10.1007/s10776-006-0034-1

DO - 10.1007/s10776-006-0034-1

M3 - Article

VL - 13

SP - 221

EP - 227

JO - International Journal of Wireless Information Networks

JF - International Journal of Wireless Information Networks

SN - 1068-9605

IS - 3

ER -