Analysing the Vulnerability of Protocols to Produce Known-pair and Chosen-text Attacks

In this paper we report on an analysis for finding known-pair and chosen-text attacks in protocols. As these attacks are at the level of blocks, we extend the attacker by special capabilities related to block chaining techniques. The analysis is automated using Blanchet's protocol verifier and illustrated on two well-known protocols, the Needham-Schroeder-Lowe public-key protocol as well as the Needham-Schroeder symmetric-key protocol. On the first protocol, we show how the special intruder capabilities related to chaining may compromise the secrecy of nonces and that chosen- ciphertext attacks are possible. We propose two modified versions of the protocol which strengthen its security. We then illustrate known-pair and chosen-plaintext attacks on the second protocol.