Protocol Analysis Beyond the Dolev-Yao Model

摘要

In their paper in 1983, Dolev and Yao presented a method for protocol analysis that is based on term-rewriting. Later, the term Dolev-Yao model was coined to differentiate between this type of protocol analysis and an approach developed in cryptography, which is based on complexity theory and uses reduction proofs as a main technique. Today, analysis in the Dolev-Yao model' usually means that two assumptions are made: 1. Cryptography is 'perfect'. The adversary does not try to exploit any weakness in the underlying cryptographic algorithms but only algebraic properties of cryptographic operators and interactions between protocol messages. 2. The adversary can observe and manipulate all messages exchanged in a protocol run and can itself start protocol runs. While there are currently notable efforts to remove the first assumption from protocol analysis, see e.g. the work by Canetti, and by Pfitzmann and Backes (and others), the validity of the second assumption, which goes back to Needham and Schroeder, is hardly ever analyzed. As a standard assumption, the communications network is treated as a cloud and all messages are handed to the adversary for delivery. One might indeed think that security results would thus be stronger because a strong adversary is assumed. This talk will discuss three example protocols to show the importance of performing protocol analysis using more structured models of the communications network. The three examples are the binding update protocol for mobile IPv6 (RFC3775. and [1]), where keys are sent in the clear, the CANVAS protocol, a data integrity protocol for sensor networks that achieves its goal by relying on independent witnesses instead of data origin authentication, and finally the Host Identity Protocol, a mobility protocol for the Internet where we focus on protocol design issues caused by so-called middleboxes such as Network Address Translators (NATs) and firewalls.