Conclusion

The main points of the paper are the following:

• We present the novel approach of automatic generation of security protocols. With a user-defined specification of security properties and the system requirements, including a system metric function, APG generates minimal protocols that satisfy the specified security properties and system requirements, minimal with respect to the metric function. This approach is a significant improvement over the current protocol design process, because it is more reliable, efficient, and produces protocols that suit the given system requirements ideally.
• We perform a case study on the automatic generation of two-party mutual authentication protocols for proof of concept and to gain experience with APG. During the case study, APG automatically generates protocols that are simpler than the documented standard ones. In two examples from the real world, APG is also able to generate different optimal protocols with respect to varying metric functions, and hence, demonstrate its benefit.