Formal prototyping in early stages of protocol design

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 drawback 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 ...

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: Alwyn Goodloe, Carl A. Gunter, Mark-Oliver Stehr
• Keywords: IPsec Security Associations, Maude Executable Specifications, POPL 2005, Programming Languages, Simulation Uncovered Problems