Bell Labs Researchers Spot Bluetooth Insecurities

Kyobu writes: "There's an article by John Markoff in [Saturday's] New York Times about insecurities in Bluetooth. The defects allow eavesdropping and caller identification." Markus Jacobson and Susanne Wetzel, both of Bell Laboratories, discovered weaknesses in the key exchange protocol currently implememented by Bluetooth. From the article: "The researchers are suggesting that the Bluetooth standard be altered so that the identity numbers are masked by a constantly changing pseudonym when transmitted." Considering the ubiquity many people expect Bluetooth devices to achieve, perhaps it's a good thing that this kind of attention starts early rather than late. (Complete with gratuitous Bruce Schneier quote.)

Comments

Problems in protocols, analysis

[Submarine]

A little known fact in the general computing public is that problems in secure communications lie more often in the communication protocol than in the encryption primitives.

There are some classical attacks:

• Man-in-the-middle Idea: I can prove to both Karpov and Kasparov that I'm a great chess player. I challenge them both in a play through mail. I use the moves of each one against the other. Both think I play like a grandmaster.
• Use of old keys Idea: recover some secret data of a previous session (for instance from old temporary files on a common machine - after all, many operating systems do not really erase erased data). Use it in a current session.

It is possible to prevent those attacks by clever design of the protocol. For instance, the use of old keys can be prevented by some "nonce" numbers (generated once) or some clock data.

It is very difficult to analyse protocols and prove them correct.

First, a formal model of the protocol, its environment and what it means for it to be correct. This is nontrivial, since some models may just ignore some kinds of attacks.

Then the protocol must be proved correct with respect to the formal specification. Alas:

• manual theorem proving is error-prone
• formal theorem proving is tedious
• automatic analysis tools are not so powerful

I have made some research on these topics. For more information, see for instance Jon Millen's page.