There are two main challenges for the protocol screener. First, the protocol screener needs to be sound. If the protocol screener outputs a flawed protocol, the automatic protocol generation is not trustworthy. Second, the protocol screener has to be efficient because potentially the protocol generator could generate thousands of candidate protocols.
Hence, one point worth mentioning is that this research also serves a second purpose: a real test for Athena. As far as shown in previous literature, most of the automatic tools for protocol analysis have only been tested with a handful testing protocols and the testing protocols are mainly existing human-designed protocols. The candidate protocols generated by the protocol generator are purely machine-generated from a large protocol space, and hence, could potentially contain more misbehavior and difficult errors. Therefore, this is a good test for the soundness of both design and implementation of Athena. During the experiments, the protocol generator generates thousands of candidate protocols. Therefore, this is also a good test for the performance of Athena. As a sanity check, we also manually analyzed the protocols which Athena proved correct. We were not able to find errors in these protocols. On average, Athena verifies around 5 protocols per second, based on a 400 MHz Pentium II Linux workstation.