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.
Mechanising BAN kerberos by the inductive method
Bella G.
;
1998-01-01
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
