Identifying andTesting for Insecure Paths in Cryptographic Protocol Implementations

Cryptographic protocols, which are also referred to as security protocols are used to process, store and transfer increasing volumes of information on our financial networks, health networks, and even our library systems, not to mention our conventional communication systems and our networked systems of personal and corporate computers. Users should be able to justifiably rely on their implementations to process, store, and communicate sensitive information securely. Testing is indispensable even when a security protocol is formally verified because most formal verification techniques only guarantee the correctness of the design, under certain assumptions. More importantly, no guarantees about the implementation are provided. A mathematical proof that an implementation of a security protocol conforms to its specifications is usually not feasible because it would require complicated formal semantics of the language in which it is written and the environment in which the protocol runs (the operating system and hardware)