In [KR04] we use Bruno Blanchet's protocol verifier [B01] to analyse whether a protocol offers the possibility to launch known pair or chosen text attacks. 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 [L95] as well as the Needham-Schroeder symmetric-key protocol [NS78]. 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 Needham-Schroeder symmetric key protocol.
The verification using Blanchet's protocol verifier requires the specification of the protocols and the definition of the attacker capabilities as Prolog rules.
Some slides are available here.
Download and instructionsBefore you are able to analyse the protocols, you need to install the protocol verifier. Installation instructions and source code can be found here (at the bottom of the page).
You can find here the files corresponding to the Needham-Schroeder-Lowe public-key protocol, the Needham-Schroeder-Lowe public-key protocol with an explicit integrity mechanism and the Needham-Schroeder symmetric-key protocol.
You need to uncomment the properties you wish to verify. The
verification is launched by
analyser [filename]
| [B01] | Bruno Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Steve Schneider, editor, 14th IEEE Computer Security Foundations Workshop, pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society Press. |
| [KR04] | Steve Kremer and Mark D Ryan. Analysing vulnerability of protocols to produce known-pair and chosen-text attacks. In 2nd International Workshop on Security Issues in Coordination Models, Languages, and Systems, Electronic Notes in Theoretical Computer Science, London, UK, August 2004. Elsevier. Co-located with Concur 2004. |
| [L95] | Gavin Lowe. An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters, 56(3):131-133, November 1995. |
| [NS78] | Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993-999, 1978. |