Abstract: A framework for evaluating security levels of Learning With Error (LWE)-based lattice schemes was presented, grounded in automated reasoning, combining formal modeling with algorithmic methods. Security evaluation under two mainstream attack paradigms, primal and dual attacks, were formulated as global optimization problems. For the primal attack, symbolic computation was used to derive theorem-level results that directly yield the optimal solution. For the dual attack, a refined optimization model was specified and solved more precisely via global optimization. Accordingly, the evaluation workflow was made more automated and systematic. A companion software tool was developed. It provides detailed transparency by exposing the reasoning path, key formulas, and intermediate statistics for inspection and verification. Experimental results show that, on the test set, the security estimates under primal attack are consistent with those produced by Lattice Estimator, while under dual attack, the results are more accurate and intentionally conservative, owing to finer modeling and more precise solution procedures. The approach is auditable and interpretable and supports parameter selection and security justification.

Key words: lattice-based scheme, Learning With Error (LWE), security level evaluation, primal attack, dual attack

摘要： 以自动推理为核心思想，沿形式化建模与算法化求解相结合的路线，面向基于容错学习(LWE)问题的格密码方案构建一套安全级别评估框架。将原始攻击与对偶攻击两类主流攻击下的安全级别评估问题系统性地表述为全局优化问题。其中，针对原始攻击，借助符号计算给出定理化结论，可直接导出最优解；针对对偶攻击，规范化为明确的优化模型，并结合全局优化算法进行更精确的求解。由此，安全级别评估的求解过程可以实现更高程度的自动化与算法化。在此基础上，开发具备细节展示功能的软件，可呈现求解依据、关键公式及中间统计量，以便用户理解、核查与验证。实验结果表明：在原始攻击下，测试参数上的评估结果与Lattice Estimator基本一致；在对偶攻击上，由于建模更细致，求解方法更精确，结果也更为精确且偏保守。本文方法兼具可复核、可解释与工程可用性，可为参数选型与安全论证提供支持。

关键词: 格密码方案；容错学习；安全级别评估；原始攻击；对偶攻击 ,  ,