Mechanising BAN Kerberos by the Inductive Method

The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of expired session keys. Thanks to timestamping, the protocol provides the involved parties with strong guarantees in a realistically hostile environment. These guarantees are supported by the generic theorem prover Isabelle.

• Type: Conference
• Year: 1998
• Where: CAV
• Authors: Giampaolo Bella, Lawrence C. Paulson
• Keywords: CAV 1998, Expired Session Keys, Hardware, Session Keys, Theorem Prover Isabelle