Our Findings of the Protocols

Continuing the experiment from the previous subsection, Athena analyzed the remaining candidate protocols and output 2 correct symmetric-key protocols, which have the minimum cost 10. Among the 110 asymmetric-key protocols, only 1 is correct and has the minimal cost 14. The three protocols are listed below:

• Symmetric-key mutual authentication protocols.

  $Protocol:A\to B:N$_A,A B→A:{N_A,N_B,A}₅₄₆K_AB A→B:N_B

  $Protocol:A\to B:N$_A,A B→A:{N_A,N_B,B}₆₀₄K_AB A→B:N_B

  The standard symmetric key mutual authentication protocol using random numbers is documented in ISO/IEC 9798 [Int93] as ISO Symmetric-Key Three-Pass Mutual Authentication Protocol:

  $Protocol:A\to B:N$_A,A B→A:{N_A,N_B,B}₆₆₈K_AB A→B:{N_A,N_B}₆₈₉K_AB

  Our automatically-generated protocols are clearly simpler than the one listed as ISO standard with respect of serving the same purpose as mutual authentication protocol.
• Asymmetric-key mutual authentication protocols.

  $Protocol:A\to B:\{N$_A,A}₇₃₃K_B B→A:{N_A,N_B,B}₇₅₅K_A A→B:N_B

  This protocol happens to be the same as the fixed version of Needham-Schroeder protocol [Low96], except for that the last message is not encrypted. This is because we do not have the secrecy requirement in the security property specification.

Although intuitive, another interesting result from the statistics is that the number of correct protocols comparing to the protocols that have the same cost is very low. For example, in this case study, the ratio of generated protocols to correct protocols is around $10-4$. This ratio decreases when we increase the cost threshold.