A Comparison between two Methods of Security Proof.
Duong Hieu Phan and David Pointcheval.
Abstract: In this paper, we compare two methods for security proofs - a formal method, and the method by reduction from the complexity theory. A modification of the Otway-Rees protocol is proposed to show out a difference between the two methods: the exchanged key is provably secure in the sense of the BAN logic but it is not when we analyze it by reduction. The difference is due to a limitation of BAN logic, which has not been noticed before, that it does not consider the relation between different ciphertexts. Note that in the original Otway-Rees protocol, under the hypothesis of semantic security of the symmetric encryption scheme, we prove the semantic security of the exchanged key which is a similar result to the one obtained with BAN logic.
Ref: Proceeding of RIVF. Pages 105-110, Hanoï -- February 2003, Editions Suger, Paris, pages 105-110.