Conference,
Survey of communication protocol verification techniques, Trends and Applications 1976: Computer Networks
C. Sunshine.(1976)Gaithersburg, Maryland, Nov. 1976.
Meta data
- BibTeX key
- Sunshine76
- entry type
- conference
- booktitle
- Symposium sponsored by IEEE Computer Society; National Bureau of Standards
- year
- 1976
- file
- :I\:\\My Documents\\Thesis\\Research\\Sunshine76.pdf:PDF
- owner
- msteele
- review
- This paper provides a survey of formal verification of communication protocols. Petri nets, UCLA graphs, state diagrams, assertions, programming languages, state tranition matrices, flow charts and prose are all identified as previously explored formal methods. A key idea introduced is that communication protocol specifications should serve the purpose of verification, among others. The paper discusses the "explosion of states" that occur as the protocols become more complex and more detail is modeled in the transmission medium. The bottom line the author presents is that there is a lack of rigor in verifying real world protocols. Andel07b picks up on this same idea 21 years latter and applies it to the concept of rigor in security. Holzmann04 picked up this torch with the development of SPIN, so clearly there has been some work in formal verification, but its focus has primarily been on the verification of protocols against random errors rather than against injected and colluding errors or attacks. We proposed an extension to formal verification that takes into account the idea of the attacker and attempt to find a general solution to find vulnerabilities against attackers.
- note
- Gaithersburg, Maryland, Nov. 1976
Tags
Users
Comments and Reviewsshow / hide
Cite this publication
More citation styles
- please select -%0 Generic
%1 Sunshine76
%A Sunshine, C. A.
%B Symposium sponsored by IEEE Computer Society; National Bureau of
Standards
%D 1976
%K communication protocol_verification survey verification
%T Survey of communication protocol verification techniques, Trends
and Applications 1976: Computer Networks
@conference{Sunshine76,
added-at = {2011-07-15T15:18:02.000+0200},
author = {Sunshine, C. A.},
biburl = {https://www.bibsonomy.org/bibtex/21f0c19a27f21c98bd213a286e9bb0334/msteele},
booktitle = {Symposium sponsored by IEEE Computer Society; National Bureau of
Standards},
file = {:I\:\\My Documents\\Thesis\\Research\\Sunshine76.pdf:PDF},
interhash = {e349e6aa4e6b67b21a552d12a1f48fd0},
intrahash = {1f0c19a27f21c98bd213a286e9bb0334},
keywords = {communication protocol_verification survey verification},
note = {Gaithersburg, Maryland, Nov. 1976},
owner = {msteele},
review = {This paper provides a survey of formal verification of communication
protocols. Petri nets, UCLA graphs, state diagrams, assertions, programming
languages, state tranition matrices, flow charts and prose are all
identified as previously explored formal methods. A key idea introduced
is that communication protocol specifications should serve the purpose
of verification, among others. The paper discusses the "explosion
of states" that occur as the protocols become more complex and more
detail is modeled in the transmission medium. The bottom line the
author presents is that there is a lack of rigor in verifying real
world protocols. Andel07b picks up on this same idea 21 years latter
and applies it to the concept of rigor in security. Holzmann04 picked
up this torch with the development of SPIN, so clearly there has
been some work in formal verification, but its focus has primarily
been on the verification of protocols against random errors rather
than against injected and colluding errors or attacks. We proposed
an extension to formal verification that takes into account the idea
of the attacker and attempt to find a general solution to find vulnerabilities
against attackers.},
timestamp = {2011-07-15T20:02:52.000+0200},
title = {{Survey of communication protocol verification techniques, Trends
and Applications 1976: Computer Networks}},
year = 1976
}