Panel: What Protocol Designers Need From Formal Methods
Naval Research Laboratory, Code 5543
Washington, DC 20375
The past few years have seen a rapidly growing amount of research
in the application of formal methods to the design and verification
of cryptographic protocols. They have also seen an equally rapidly
growing amount of work in developing and fielding cryptographic protocols,
and a growing need for secure communication over the Internet.
The problem of assuring the correctness of these protocols
has been a matter of some concern, and this sparked interest
in making use of the products of formal methods research.
However, formal methods has traditionally been seen as an
arcane field requiring special expertise, and for this reason
difficult to transition into industry.
The purpose of a this panel is to examine the issues
around the question of making formal methods for cryptographic protocol
analysis into tools that can be used by developers. We have
invited a panel of experts on cryptographic protocol development
to talk about what they need and expect from formal methods
tools and techniques, and in what direction they would
like the field to be going. Some of the questions we
will be considering are:
- What problems should formal methods research be addressing that it isn't?
Where in the design process do problems most usually appear,
and at what level of abstraction? Is it at the level much of the research
has been concentrated at, in which messages are modeled
as sequences of words encrypted by algorithms that behave
as black boxes, is at a lower level involving attacks on algorithms,
or is it higher up, at the policy or requirements level?
Can this information be used to help
researchers focus their efforts?
- How could/should formal methods be integrated into the design process?
Where can they be of the most help?
- What are the biggest barriers to using formal methods in
cryptographic protocol design?
- Where are cryptographic protocols going? What are the new applications
that will require new types of protocols? In what direction should
this be driving research?
- Are there any new developments in the application of formal
methods to cryptographic protocol analysis that seem like they would
be particularly useful?
- Are formal methods researchers making the right assumptions
about the mechanisms used by cryptographic protocols and the environments
in which they operate? If not, how should they be changed? In particular,
do we need a revision of the threat models commonly used?
- Catherine Meadows, NRL (chair)
- John Brainard, RSA
- Robert Cordery, Pitney Bowes
- Carl Ellison, Cybercash
- Steven Kent, BBN