Assumptions

We initially analyzed how many first messages the initiator $A$ can send, with a given depth of the message tree. Subsequently, we refer to the two protocol principals as the initiator $A$ and the responder $B$. Initially the initiator knows the following atomic message components: $A,\; B,\; K$_A, K_A^-1, K_B, N_A. With a message depth of 4 the initiator can generate about one thousand messages; and with a depth of 6, it can generate about 8 million messages. If a two-party mutual authentication protocol uses three rounds, considering 1000 possible messages in each round would leave us with $109$ protocols. A protocol screener which analyzes 20 protocols per second, would take over 1 year.

After the initial estimate, we decide to make certain assumptions to keep the protocol space small. We do not intend to prove that these assumptions do not eliminate the potential optimal protocol. But we believe these assumptions are intuitively reasonable. We list all the assumptions we make in the case study as the following:

• Message components are typed. This allows any participant to distinguish a nonce from a principal name, for example.
• In any concatenated message, there are no redundant message components, i.e., $N$_A, N_A.
• No initial keys are sent in a message, since it does not make sense to send a private key, and we assume every principal knows all the public keys. Session keys generated during the protocol run do not fall into this category of authentication protocols.
• We assume that the initiator's name needs to be in the first message in a understandable format to the responder, so that the responder knows who to reply to. (This assumption might not be necessary when the initiator and the responder have a link between them that is only used to communicate between the two parties, although this case is not very general so we do not consider it here.)
• We do not consider permutations of the message components of a concatenated message.

The last point reduces the protocol space tremendously. Unfortunately, this optimization might result in missing a correct protocol. This case can occur if the generated protocol is vulnerable to a specific replay attack, where a message of round $i$ can be replayed for another message of round $j$ ($i\; \ne \; j$). In our current implementation of APG, the protocol is rejected and no permutation of the message components is considered. In the future, however, we could detect this case and try to repair the protocol through a message reordering.