SDL: A DSL for Cryptographic Schemes

in he a few years there has been an increasing interest in automating the development and implementation of cryptographic schemes, which traditionally are manual, difficult and error-prone tasks. Projects including AutoBatch and AutoGroup+ mechanically generate cryptographic schemes, and use a Domain-Specific Language (d l) called the Scheme Description Language ( dl) to represent them; but, despite being a critical component in these systems, dl is significantly limited. We introduce a redesigned dl which addresses these shortcomings: we extend the language with new features, provide a formal specification, define a type system and several other static analyses, allow it to express various kinds of cryptographic schemes, and present techniques for manipulation via term rewriting. Finally, we explore two applications: a simple transformer to assert the consistent use of group operators (additive vs. multiplicative notation); and a generalization of AutoBatch, which includes more sophisticated term rewriting. Operations that previously required hundreds of lines of code in the original AutoBatch implementation are expressed with our techniques in less then ten lines. Overall, the redesigned dl is a more solid and practical foundation upon which to build cryptographicsystem development automations.