next up previous
Next: References Up: On Searching for Known Previous: Results of Using the

Conclusion

  This work constitutes a significant step towards proving secure uses of mechanisms that assume absence of known or chosen pairs. We have given a characterization of known and chosen pairs, and a means of specifying their presence or absence. We have also shown how it can be applied to the use of an existing tool, the NRL Protocol Analyzer, and how the tool could use the model to find ways of generating chosen pairs in the ESP protocol. We then went on to show how it could be extended to be used to find attacks based on cutting and pasting.

Much work still remains to be done. In work connected to this paper, we have developed a number of inference rules describing the conclusions an attacker may draw about known and chosen pairs. As yet these have no formal foundation. However, we have begun to map these rules to the process that can be taken by the NRL Protocol Analyzer. We see this as a way, not only of providing a more concrete basis for our inference rules, but also possibly a means of abstracting away from the more computationally intensive approach of the Analyzer.

We also need to consider strategies for developing specifications for the Analyzer. The assumptions we made (that all packets were four blocks long, that headers took up one or two blocks entirely) were designed with the idea in mind of capturing the relevant security features of the specification, while still keeping the analysis tractable. However, our approach to doing this was informal and ad hoc, and as we have shown, led to some errors that resulted in the generation of spurious attacks. We need to develop more systematic ways of identifying assumptions, as well as rigorous arguments that our abstractions capture the assumptions. This will give us ways of generating specifications in a more systematic fashion, and will allow us more confidence in the usefulness of any proofs that we obtain that a specification is secure against certain types of attacks. However, as we learned from writing the specification that appears in this paper, it is possible to clarify assumptions and discover errors by examining the attacks produced by the Analyzer and comparing them against what we know to be possible. We expect continued use of the Analyzer to test our hypotheses to help us further in the development of our heuristics.

Finally, there are probably some improvements that need to be made to the Analyzer itself before it can be used successfully to analyze more complex protocols involving low-level properties. Surprisingly, we did not find the Analyzer's inability to model the commutivity and associativity of exclusive-or as much of a handicap as we had feared. This was because many threats posed by cipher block chaining, that is, its cut-and-paste and self-healing properties, were easily expressible in terms that could be modeled by the Analyzer. However, we found that the specification of block-by-block encryption was complex. Consequently, the analysis resulted in a certain amount of state space explosion. This could clearly be a drawback if we wanted to specify anything more than the simple sending and receiving of messages. However, we note that, as part of the work on the Protocol Analyzer this year, the second author of this paper has developed a more sophisticated specification language for the Protocol Analyzer that makes for much cleaner specifications. Indeed, this language had been used to specify the ISAKMP/Oakley protocol and the extremely complex SET protocol. Since the language incorporates constructs such as subroutines and if-then-else, it should be easier to modify recursive procedures in it.

The problem of state explosion is tougher. However, we note that much of the state explosion results from the recursive specification generating a number of very similar-looking states. The Analyzer already includes some features for recognizing when one state is reachable only if another state is has a way of cutting down on the size of the search space. It may be possible to extend this to permit the Analyzer to perform induction over recursively generated states.


next up previous
Next: References Up: On Searching for Known Previous: Results of Using the