Formal prototyping in early stages of protocol design

Alwyn Goodloe, Carl Gunter, Mark Oliver Stehr

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

Abstract

Network protocol design is usually an informal process where debugging is based on successive iterations of a prototype implementation. The feedback provided by a prototype can be indispensable since the requirements are often incomplete at the start. A draw-back of this technique is that errors in protocols can be notoriously difficult to detect by testing alone. Applying formal methods such as theorem proving can greatly increase one's confidence that the protocol is correct. However, formal methods can be tedious to use, rarely support successive design iterations and prototyping, are difficult to scale to entire designs, and typically require a clear understanding of requirements in advance. We investigate how formal simulation based on Maude executable specifications overcomes many of these hurdles. We apply this technique in the early stages of the design of a new security protocol, known as Layer 3 Accounting (L3A), aimed at protecting known vulnerabilities in the wireless accounting infrastructure. The protocol sets up a collection of IPsec security associations that provide the necessary protection. We demonstrate how formal simulation uncovered problems in several successive iterations of the L3A protocol design.

Original languageEnglish (US)
Title of host publicationProceedings of the 2005 Workshop on Issues in the Theory of Security, WITS '05
Pages67-80
Number of pages14
DOIs
StatePublished - Dec 1 2005
Event2005 Workshop on Issues in the Theory of Security, WITS '05 - Long Beach, CA, United States
Duration: Jan 10 2005Jan 11 2005

Publication series

NameProceedings of the 2005 Workshop on Issues in the Theory of Security, WITS '05

Other

Other2005 Workshop on Issues in the Theory of Security, WITS '05
Country/TerritoryUnited States
CityLong Beach, CA
Period1/10/051/11/05

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint

Dive into the research topics of 'Formal prototyping in early stages of protocol design'. Together they form a unique fingerprint.

Cite this