On the formal verification of delegation in SESAME

The objective of this paper is to present the verification of delegation in the SESAME protocol, a compatible extension version of Kerberos. For this we use the formal approach presented in Bolignano (1997). This approach is based on the use of state-based general purpose formal methods. It makes a clear separation between modeling of reliable agents and that of intruders. The SESAME protocol allows a principal in the system to delegate his rights to another principal or a group of principals. The formalization is transposed in a quite systematic manner into the Coq prover´s formalism, and the complete formal proof is performed. The proof relies on the fact that confidentiality of keys shared by the multiple authorities involved in the protocol is guaranteed