A formal analysis of ome properties of kerberos 5 using MSR
A formal analysis of ome properties of kerberos 5 using MSR
复制标题
使用 MSR 对 kerberos 5 的 ome 属性进行正式分析
DOI：
10.1109/csfw.2002.1021815
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
A. Scedrov
中科院分区：
文献类型：
--
作者：
F. Butler;I. Cervesato;A. D. Jaggard;A. Scedrov
我们正式方面的125认证协议的多集重写形式主义（MSR）的两个层次的细节。更详细的形式化反映了1995年规范的复杂结构，考虑到以前没有考虑过的几个协议特性。在抽象形式化中，我们证明了一个认证性质约为5。我们发现了三个异常，其中之一发生在两个层次的细节，而其他两个依赖于更丰富的结构的详细形式化。我们还讨论了如何增加校验和（其中一些是在协议规范，其中一些不是）可能会消除这些异常。
We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the intricate structure of the Kerberos 5 specification, taking into account several protocol features which have not been previously considered. In the abstract formalization, we prove an authentication property about Kerberos 5. We discovered three anomalies, one of which occurs on both levels of detail, while the other two rely on the richer structure of the detailed formalization. We also discuss how the addition of checksums (some of which are in the protocol specification and some of which are not) may eliminate some of these anomalies.