Supervisory Control and Data Acquisition (SCADA) systems control the critical utility and process control infrastructures in many countries. However, little attention was given to security considerations in the initial design and deployment of these systems, which has caused an urgent need to upgrade existing systems to withstand hostile cyber-based attacks. This paper briefly describes two security models that were suggested to enhance security of SCADA communication protocols. After discussing formal logical verification methods, this research suggests appropriate verification methods and provides a comprehensive list of tools that can be used to test the soundness of security models. Two tools, namely On-the-Fly Model-Checker (OFMC) and Security Protocol Engineering and Analysis Resources, version II (SPEAR II) are selected to illustrate formal security analysis on the two security enhancement models. 

Basin D., Mödersheim S., and Viganò, L. (2003), 'An On-the-Fly Model-Checker for Security Protocol Analysis'. Proceedings of 8th European Symposium on Research in Computer Security-Lecture notes in computer science Volume 2808/2003. October 13-15. Norway: 253-270.

Basin, D., Mödersheim, S., and Viganò, L (2005), "OFMC: A symbolic model checker for security protocols," International Journal of Information Security, 4 (3): 181-208.

Boreale, M. (2001), 'Symbolic Trace Analysis of Cryptographic Protocols'. Proceedings of the 28th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science Vol. 2076. July 08-12. Heraklion, Crete, Greece, Springer, London: 667-681.

Boreale, M. and Buscemi M. (2002), 'Experimenting with STA, a Tool for Automatic Analysis of Security Protocols'. Proceedings of the 2002 ACM symposium on applied computing. March 11-14. Madrid, Spain: 281-285.

Byres, E. (2004), 'The Myths and Facts behind Cyber Security Risks for Industrial Control Systems', News Release, BCIT News, 4 October 2004.

CAPSL (2009), 'Common Authentication Protocol Specification Language', http://www.csl.sri.com/users/millen/capsl/capslhome.html, 27 January 2009.

Casper (2009), 'Formal Analysis of Security Protocols', http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security, 27 January 2009.

CASRUL (2009), 'CASRUL Home Page', http://loria.fr/equipes/cassis/softwares/casrul, 27 January 2009.

DNP User Group (2005), 'A DNP3 Protocol Primer', http://www.dnp.org/About/DNP3%20Primer%20Rev%20A.pdf, 27 January 2009.

DOE (2009), '21 Steps to Improve Cyber Security of SCADA Network by the US Department of Energy' http://www.oe.energy.gov/DocumentsandMedia/21_Steps_-_SCADA.pdf, 27 January 2009.

Estelle (1989), 'Estelle-A Formal Description Technique Based on an Extended State Transition Model', ISO Standard OSI 9074, International Standards Organization, Geneva.

EVA (2009), 'The RNTL EVA Project', http://www.lsv.ens-cachan.fr/~goubault/EVA.html, 27 January 2009.

Frost and Sullivan (2009), 'European SCADA systems Market in Dynamic Shape', http://engineeringtalk.com/news/fro/fro144.html, 27 January 2009.

Gordon, A., and Jeffrey. A. (2009), Cryptographic Protocol Type Checker (CRYPTC), http://cryptyc.cs.depaul.edu, 27 January 2009.

Graham, J. H. and Patel, S. C. (2005), "Security Issues in SCADA Systems," DIAS Technology Review: The International Journal of Business and IT, 1 (2): 28-33.

Jackson, K.M. and Hruska, J. (1992), Computer Security Reference Book, CRC Press, Boca Raton, Florida.

LOTOS (1989), 'LOTOS-A Formal Description Technique Based on the Temporal Ordering of Observational Behavior', ISO Standard OSI 880, International Standards Organization, Geneva.

Patel, S.C. (2006), 'Secure Internet-Based Communication Protocol for SCADA Systems'. Computer Science, University of Louisville, Louisville, Kentucky, Unpublished PhD Thesis.

Patel, S.C., Bhatt, G.D. and Graham, J.H. (2007), "Improving the Cyber Security of SCADA Communication Networks", Communications of the ACM (accepted).

Patel, S. C., and Graham, J. H (2004), 'Security Considerations in DNP3 SCADA Systems'. Proceedings of the 17th International Conference on Computer Applications in Industry and Engineering. November 17-19. Orlando, FL: 73-78.

Patel, S., and Yu, Y. (2007), "Analysis of SCADA Security Models", The International Management Review, 3(2): 68-76.

Perrow, C. (1999), Normal Accidents: Living with High-Risk Technologies. Princeton University Press, Princeton, New Jersey.

ProVerif (2009), 'ProVerif: Cryptographic protocol verifier in the formal model', http://www.proverif.ens.fr, 27 January 2009.

Sandia (2009), 'The Center for SCADA Security at Sandia National Laboratories', sandia.gov/scada, 27 January 2009.

SPEAR (2009), 'Security Protocol Engineering and Analysis Resources, version II', http://www.cs.uct.ac.za/Research/DNA/SPEAR2, 27 January 2009.

Spi (2009), 'Spi Calculus', http://www.cse.psu.edu/~catuscia/teaching/cg597/01Fall/lecture_notes/ TheSpiCalculus.ppt, 27 January 2009.

Wright, A.K., Kinast, J.A., and McCarty, J. (2004), 'Low-Latency Cryptographic Protection for SCADA communications'. Proceedings of the Second International Conference on Applied Cryptography and Network Security. June 8-11. Yellow Mountain, China: 263-277.

Yasinsac, A. and Childs, J. (2001), 'Analyzing Internet Security Protocols'. Proceedings of the Sixth IEEE International Symposium on High Assurance Systems Engineering. Oct. 22-24. Boca Raton, Florida: 149-159.