论文部分内容阅读
该文针对加密协议面临的各种攻击，提出了一个基于时序逻辑的加密协议描述语言(the Description Language of Encryption Protocols Basing Temporal Logic，简称为TL-EPDL)。TL-EPDL语言应用标准时序来描述密码协议，刻化模拟入侵者行为和系统需求正确性。特别地，研究人员用该语言框架描述和证明了一个系统入侵者不能用任何代数和逻辑的办法获得会话密钥的实例。该文还将本描述方法与同行相关工作进行了讨论；研究人员认为本方法具有形式化程度高、灵活等特点。