On the formal verification of delegation in SESAME

Author

Ayadi, Marc Mehdi ; Bolignano, Dominique

Author_Institution

Cap Germini/Div. Finance, Paris, France

fYear

1997

fDate

16-19 Jun 1997

Firstpage

23

Lastpage

34

Abstract

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

Keywords

access protocols; formal verification; security of data; SESAME; SESAME protocol; confidentiality of keys; delegation; formal approach; formal proof; formal verification; intruders; reliable agents; state-based; Access protocols; Authentication; Body sensor networks; Cryptographic protocols; Cryptography; Finance; Formal verification; Joining processes; Logic; Protection;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1997. COMPASS '97. Are We Making Progress Towards Computer Assurance? Proceedings of the 12th Annual Conference on

Conference_Location

Gaithersburg, MD

Print_ISBN

0-7803-3979-7

Type

conf

DOI

10.1109/CMPASS.1997.613201

Filename

613201