摘要： 本文指出了现有时限责任分析技术中存在的缺陷，提出了一种基于Kailar逻辑的安全协议时限责任分析框架。通过该分析框架对一个具有时限性要求的安全电子投递协议进行分析，发现了协议存在的时限问题，修改了协议并给出了修改后的协议满足时限性要求的证明。

关键词: 时限约束 安全协议分析技术 Kailar逻辑 形式化方法