Formal analysis of two standardized protocols using standard spaces

Abstract

To achieve secure communication it is critical to provide protocols which are secure against attacks. Formal methods are helpful in finding whether or not a protocol is secure. The first formal method for this task, namely BAN logic was proposed by Burrows, Abadi and Needham. However, it is well known to have deficiencies. The most recent deficiency was found by Teepe who showed that the hash inference rule of BAN logic is unsound. This rule was first used in the analysis of CCITT by Burrows, Abadi and Needham. Later it was also used in the analysis of SET by Agray, Hoek and Vink.

This thesis proposes a simple modification to the BAN hash rule to remove its unsoundness. We demonstrate that the modified rule captures the inference that the original rule intended to capture for the above protocols. The deficiency of BAN in proving security guarantees cannot be overcome by just modifying the rules. It would therefore be preferable to have proof of security using alternate methods which are more rigorous than BAN logic. To this end, we provide proofs of correctness of the above protocols using the strand space technique proposed by Fabrega, Herzog and Guttman.