added ref to related work of Chen et al

introduction.tex

@@ -42,6 +42,10 @@ unexpected orders to expose any hidden anomalies.
 %but that research does not consider logical flaws in actual software
 %implementations.
 
+Chen et al.\cite{ChenDW04} use the MOPS software model checking tool
+to detect security vulnerabilities in the OpenSSH C implementation
+due to violation of folk rules for the construction of secure programs
+such as ``Do not open a file in writing mode to stdout or stderr''.
 Udrea et al.\cite{Udrea_rule-based_2008} also investigated SSH
 implementations for logical flaws.  They used a static analysis tool to
 check two C implementations of SSH against an extensive set of rules.
@@ -54,6 +58,7 @@ defined at an abstract level so do not need such tailoring. Moreover,
 our black box approach approach means we can analyze any implementation
 of SSH, not just C implementations.  
 
+
 Formal models of SSH in the form of state machines have been used
 before, namely for a manual code review of OpenSSH
 \cite{Poll_rigorous_2011}, formal program verification of a Java

sigproc.bib

@@ -261,28 +261,24 @@ machine learning algorithms},
 
 @misc{rfc4254,
     author = {Ylonen, T. and Lonvick, C.},
-    month = jan,
     title = {The Secure Shell ({SSH}) Connection Protocol. {RFC} 4254, IETF, Network Working Group},
     year = {2006}
 }
 
 @misc{rfc4252,
     author = {Ylonen, T. and Lonvick, C.},
-    month = jan,
     title = {The Secure Shell ({SSH}) Authentication Protocol. {RFC} 4252, IETF, Network Working Group},
     year = {2006}
 }
 
 @misc{rfc4253,
     author = {Ylonen, T. and Lonvick, C.},
-    month = jan,
     title = {The Secure Shell ({SSH}) Transport Layer Protocol. {RFC} 4253, IETF, Network Working Group},
     year = {2006}
 }
 
 @misc{rfc4251,
     author = {Ylonen, T. and Lonvick, C.},
-    month = jan,
     title = {The Secure Shell ({SSH}) Protocol Architecture. {RFC} 4251, IETF, Network Working Group},
     year = {2006}
 }
@@ -564,3 +560,17 @@ machine learning algorithms},
 } 
 
 
+
+
+@inproceedings{ChenDW04,
+  author    = {H. Chen and
+               D. Dean and
+               D. Wagner},
+  title     = {Model Checking One Million Lines of {C} Code},
+  booktitle = {{NDSS}},
+  year      = {2004},
+  publisher = {The Internet Society},
+  url       = {http://www.isoc.org/isoc/conferences/ndss/04/proceedings/Papers/Chen.pdf},
+}
+
+