安全协议是保证网络安全的基础,形式化方法是分析安全协议是否符合安全目标的主流方法。目前对于存在漏洞的协议,需人为对其修正或设计新协议,这种人工处理方式不仅效率低下,而且严重依赖经验、易引入新的漏洞。初步研究表明,根据反例自动修正模型的自适应模型检测方法将有望解决安全协议分析的上述问题,目前国际上尚未出现相关研究工作。 本课题是对安全协议自动建模及设计进行的探索性研究,主要内容包括安全协议的自适应建模、自适应学习等算法的设计及实例仿真验证。旨在借鉴实时更新模型的自适应技术将安全协议的设计过程与分析过程统一起来,构造一套自适应建模方案及算法。该方案将根据攻击路径自动改进模型,并以此指导协议的设计,从而将协议的设计和改进从繁琐的人为试探中解放出来。安全协议自适应建模及设计的实现对于提高其验证和设计效率、降低分析和设计成本、增强协议本身对环境和攻击手段的自适应防御能力有重要意义。
英文主题词security protocol;formal analysis;model checking;adaptive method;protocol design