With the Internet of Things (IoT) quickly becoming a reality, the importance of secure communications between devices cannot be overstated. Since there are many small devices involved in such networks, the algorithms needed for authentication must be able to process a large number of messages both quickly and reliably. The contribution of this paper is in showing the generation of an efficient batch verifier from a high-level description of a signature scheme. The code generation approach adds the benefit of the generated code being automatically correct, provided the generator is correct. In this case, the generator creates a respective correctness proof as an additional benefit.

The paper starts out with a concise introduction presenting an overview of the problem, the contributions of the paper, and related approaches. Background and the basic definitions of the domain are presented in the following section. The general ideas of the AutoBatch toolchain developed by the authors are developed and illustrated in the following section, whereas the fourth section provides some benchmark results from controlled experiments as well as some relevant practice tests. The conclusion follows.

In summary, the approach looks very interesting and the paper is quite easy to read. To fully grasp what has been achieved with the toolchain provided, additional literature needs to be consulted; however, there are sufficient references in the paper.