Verifying Second-Level Security Protocols
Verifying Second-Level Security Protocols
复制标题
验证二级安全协议
DOI：
10.1007/10930755_23
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
G. Bella;Cristiano Longo;Lawrence Charles Paulson
第二级安全协议被定义为依赖于底层安全协议以实现其目标的安全协议。经典认证协议的验证已经成为常规，但第二层协议提出了新的挑战。这些包括对底层协议的形式化呼吁，威胁模型的修改以及新目标的形式化。使用Isabelle和归纳法[14]已经解决了这些挑战。结果在Abadi等人最近的认证电子邮件交付协议上得到了证明。[2]。
A second-level security protocol is defined as a security protocol that relies on an underlying security protocol in order to achieve its goals. The verification of classical authentication protocols has become routine, but second-level protocols raise new challenges. These include the formalisation of appeals to the underlying protocols, the modification of the threat model, and the formalisation of the novel goals. These challenges have been met using Isabelle and the Inductive Approach [14]. The outcomes are demonstrated on a recent protocol for certified e-mail delivery by Abadi et al. [2].