Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V

• 作者: Jun Pang Yongjian Li
• 来源期刊: 信息安全(英文)
• 学科: 工学
• 关键词: STRAND Space KERBEROS V THEOREM Proving Verification Isabelle/HOL
• 年，卷（期）: 2010,（2）
• 页码范围: 56-67
• 页数: 12页
• 分类号: TP39

摘要

In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL.