|Previous||Table of Contents||Next|
The Navy Research Laboratorys (NRL) Protocol Analyzer is probably the most successful application of these techniques [1512,823,1046,1513]; it has been used to discover both new and known flaws in a variety of protocols [1044,1045,1047]. The Protocol Analyzer defines the following actions:
From these actions, requirements can be specified. For example:
To use the NRL Protocol Analyzer, a protocol must be specified using the previous constructs. Then, there are four phases of analysis: defining transition rules for honest participants, describing operations available to allhonest and dishonestparticipants, describing the basic building blocks of the protocol, and describing the reduction rules. The point of all this is to show that a given protocol meets its requirements. Tools like the NRL Protocol Analyzer could eventually lead to a protocol that can be proven secure.
While much of the work in formal methods involves applying the methods to existing protocols, there is some push towards using formal methods to design the protocols in the first place. Some preliminary steps in this direction are . The NRL Protocol Analyzer also attempts to do this [1512,222,1513].
The application of formal methods to cryptographic protocols is still a fairly new idea and its really hard to figure out where it is headed. At this point, the weakest link seems to be the formalization process.
Public-key cryptography uses two keys. A message encrypted with one key can be decrypted with the other. Usually one key is private and the other is public. However, lets assume that Alice has one key and Bob has the other. Now Alice can encrypt a message so that only Bob can decrypt it, and Bob can encrypt a message so that only Alice can read it.
This concept was generalized by Colin Boyd . Imagine a variant of public-key cryptography with three keys: KA, KB, and KC, distributed as shown in Table 3.2.
Alice can encrypt a message with KA so that Ellen, with KB and KC, can decrypt it. So can Bob and Carol in collusion. Bob can encrypt a message so that Frank can read it, and Carol can encrypt a message so that Dave can read it. Dave can encrypt a message with KA so that Ellen can read it, with KB so that Frank can read it, or with both KA and KB so that Carol can read it. Similarly, Ellen can encrypt a message so that either Alice, Dave, or Frank can read it. All the possible combinations are summarized in Table 3.3; there are no other ones.
Three-Key Key Distribution
|Dave||KA and KB|
|Ellen||KB and KC|
|Frank||KC and KA|
This can be extended to n keys. If a given subset of the keys is used to encrypt the message, then the other keys are required to decrypt the message.
Broadcasting a Message
Imagine that you have 100 operatives out in the field. You want to be able to send messages to subsets of them, but dont know which subsets in advance. You can either encrypt the message separately for each person or give out keys for every possible combination of people. The first option requires a lot of messages; the second requires a lot of keys.
Multiple-key cryptography is much easier. Well use three operatives: Alice, Bob, and Carol. You give Alice KA and KB, Bob KB and KC, and Carol KC and KA. Now you can talk to any subset you want. If you want to send a message so that only Alice can read it, encrypt it with KC. When Alice receives the message, she decrypts it with KA and then KB. If you want to send a message so that only Bob can read it, encrypt it with KA; so that only Carol can read it, with KB. If you want to send a message so that both Alice and Bob can read it, encrypt it with KA and KC, and so on.
This might not seem exciting, but with 100 operatives it is quite efficient. Individual messages mean a shared key with each operative (100 keys total) and each message. Keys for every possible subset means 2100 - 2 different keys (messages to all operatives and messages to no operatives are excluded). This scheme needs only one encrypted message and 100 different keys. The drawback of this scheme is that you also have to broadcast which subset of operatives can read the message, otherwise each operative would have to try every combination of possible keys looking for the correct one. Even just the names of the intended recipients may be significant. At least for the straightforward implementation of this, everyone gets a really large amount of key data.
|Previous||Table of Contents||Next|