%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 }