A Formal Semantics for Evaluating Crytographic Protocols

Abstract

Much research in the field of network security is concentrated on the technology and application of cryptography. While the cryptographic methods are heavily investigated to ensure confidence in the security of the code, many cryptographic schemes are Vulnerable due to the protocols used to implement communication in a cryptographic environment. Much work has been done to develop secure protocols, but protocols, like software, are very difficult to verify. Recent research is aimed at finding methods of verifying cryptographic protocols, though no method has achieved widespread acceptance and use. The research presented here is focused on developing a methodology for verifying cryptographic protocols based on the classical program verification technique of "weakest precondition". A specification language based on an ad hoc standard "pseudo code" will be proposed and a formal semantics given to allow evaluation of cryptographic protocols. Note: Abstract extracted from PDF file via OCR