The approach of automatic protocol generation sounds attractive, but it is initially unclear whether it is feasible to generate meaningful and correct protocols automatically. One goal of this research is to try to answer this question. During the case study, we were able to generate correct authentication protocols automatically and some of them were documented before and are currently in use. The automatic protocol generation process for authentication protocols is efficient, usually only takes matter of seconds of running time. This illustrates that the approach of automatic protocol generation is feasible.
The case study is a proof of concept and shows that automatic protocol generation can accomplish simple tasks, but it says little about whether this approach will scale up to more complicated protocols. Since the protocol space grows exponentially with the number of parties and the number of messages, we expect that the number of candidate protocols, generated by the protocol generator in more complicated cases, can be orders of magnitudes larger than the numbers that appeared in the experiments. It is an interesting research direction to explore more powerful reduction techniques to make this approach scale.
The case study mainly covers the authentication security property. There are many other interesting security properties including properties related to electronic commerce, such as atomicity. We need to extend our system to handle these properties. For example, new reduction techniques are needed for the protocol generator. Athena terminated and successfully analyzed all the candidate protocols generated in the case study for authentication protocols. But for protocols requiring other properties, we might need to add new unreachability theorems to enhance Athena.
Currently, in the protocol analysis, we assume perfect encryption. The perfect-encryption assumption states that a ciphertext can only be decrypted if the decryption key is present, and similarly, a ciphertext can only be produced if the encryption key is present. Researchers have been exploring protocols which are resistant against stronger attacks, such as dictionary attacks. It is also interesting to try to strengthen the attacker model in the current approach to produce stronger protocols.