形式逻辑分析(analyzing cryptographic protocols in mathematical logic),理学-计算机科学技术-信息安全-密码学-密码协议-密码协议分析,利用数理逻辑分析密码协议安全性的方法。密码协议形式化分析方法的一类。利用逻辑方法对密码协议进行分析时,从协议描述的用户会话消息出发,在初始假设的基础上,利用逻辑公理,通过一系列推理,证明协议是否满足安全属性,如图所示。密码协议形式逻辑分析原理逻辑分析法又称逻辑推理法,起源于Burrows、Abadi和Needham提出的BAN逻辑,BAN逻辑将体现信念的认知模态逻辑用于安全协议的分析,其中协议主体的信念被描述为一组公式,新的信念可由一组推理规则可从原有的信念得到。BAN逻辑的语法区分为3种密码要素:主体、密钥和时鲜值,协议的每个消息表达为该逻辑的1个公式。