Using SMT solvers to automate design tasks for encryption and signature schemes
Using SMT solvers to automate design tasks for encryption and signature schemes
复制标题
使用 SMT 求解器自动执行加密和签名方案的设计任务
DOI：
10.1145/2508859.2516718
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
S. Hohenberger
中科院分区：
文献类型：
--
作者：
Joseph A. Akinyele;M. Green;S. Hohenberger
今天，密码设计任务主要是手工完成的。将更多的负担转移到计算机上可以使设计过程更快，更准确，更便宜。在这项工作中，我们调查的工具，以编程方式改变现有的加密结构，以反映特定的设计目标。我们的技术提高了安全性和效率与先进的工具，包括可满足性模理论（SMT）求解器的帮助。具体来说，我们提出了两个互补的工具，AutoGroup和AutoStrong。AutoGroup将以（简单）对称组表示法编写的基于配对的加密或签名方案转换为更有效的非对称设置中的特定实例化。一些现有的对称方案有数百种可能的非对称翻译，该工具允许用户根据各种度量（如密文大小，密钥大小或计算时间）优化结构。AutoStrong工具通过自动地将存在不可伪造的签名方案转换为强不可伪造的签名方案来关注数字签名方案的安全性。这里的主要技术挑战是自动化“分区”检查，这允许高效的转换。这些工具与AutoBatch工具（ACM CCS 2012）集成并补充，但也通过利用SMT求解器的功能来推进自动化任务的复杂性。我们的实验表明，研究的两个设计任务可以在几秒钟内自动执行。
Cryptographic design tasks are primarily performed by hand today. Shifting more of this burden to computers could make the design process faster, more accurate and less expensive. In this work, we investigate tools for programmatically altering existing cryptographic constructions to reflect particular design goals. Our techniques enhance both security and efficiency with the assistance of advanced tools including Satisfiability Modulo Theories (SMT) solvers. Specifically, we propose two complementary tools, AutoGroup and AutoStrong. AutoGroup converts a pairing-based encryption or signature scheme written in (simple) symmetric group notation into a specific instantiation in the more efficient, asymmetric setting. Some existing symmetric schemes have hundreds of possible asymmetric translations, and this tool allows the user to optimize the construction according to a variety of metrics, such as ciphertext size, key size or computation time. The AutoStrong tool focuses on the security of digital signature schemes by automatically converting an existentially unforgeable signature scheme into a strongly unforgeable one. The main technical challenge here is to automate the "partitioned" check, which allows a highly-efficient transformation. These tools integrate with and complement the AutoBatch tool (ACM CCS 2012), but also push forward on the complexity of the automation tasks by harnessing the power of SMT solvers. Our experiments demonstrate that the two design tasks studied can be performed automatically in a matter of seconds.
DOI：
10.1109/sp.2008.23
发表时间：
2008-05
期刊：
2008 IEEE Symposium on Security and Privacy (sp 2008)
影响因子：
--
作者：
M. Backes;Matteo Maffei;Dominique Unruh
通讯作者：
M. Backes;Matteo Maffei;Dominique Unruh