arXiv:2503.22755v2 安全公告类型：替换交叉 摘要：网络安全需要严格且可扩展的技术，以确保系统的正确性、鲁棒性和对不断变化的威胁的弹性。自动化推理，涵盖形式逻辑、定理证明、模型检查和符号分析，为跨各种领域（如访问控制、协议设计、漏洞检测和对手建模）验证安全属性提供了基础框架。本文综述了自动化推理在网络安全中的作用，分析了逻辑系统（包括时间逻辑、应许逻辑和知识逻辑）如何被用来形式化和验证安全保证。我们探讨了最先进的工具和框架，探讨了与AI集成进行神经符号推理的途径，并指出了关键的研究空白，特别是在可扩展性、组合性和多层安全建模方面。文章以一组坚实的研究方向结束，旨在通过正式、自动化和可解释的推理技术促进安全系统的开发。