At a high level, APG is, as Figure 1 shows, a pipeline composed of an automatic protocol generator and an automatic protocol screener. In general, the process of APG has four stages. First, the protocol designer specifies the desired security properties and system requirements as input. Second, the protocol generator searches through the protocol space and generates candidate protocols that satisfy the system requirements. Third, the protocol screener analyzes the candidate protocols. Finally, the flawed protocols are discarded and the correct ones that satisfy the desired security properties are output.
