Analysis of a Forced-Latency Defense Against Man-in-the-Middle Attacks

摘要

Several cryptographic protocols have been proposed to address the Man-in-the-Middle (MitM) attack without the prior exchange of keys. In this paper, one such protocol proposed by Zooko Wilcox-O'Hearn, the forced-latency defense against the chess grandmaster attack, is analyzed. Using the Cryptographic Protocol Shapes Analyzer (CPSA), the security properties of the protocol are validated through a novel use of CPSA's state features to represent time. A small message-space attack is also uncovered that highlights an assumption that many protocols make, and a solution is proposed that would prevent such an attack against Wilcox-O'Hearn's protocol.