Modal tableaux for verifying security protocols

Mehmet A. Orgun, Guido Governatori, Chuchang Liu

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

4 Downloads (Pure)


To develop theories to specify and reason about various aspects of multi-agent systems, many researchers have proposed the use of modal logics such as belief logics, logics of knowledge, and logics of norms. As multi-agent systems operate in dynamic environments, there is also a need to model the evolution of multi-agent systems through time. In order to introduce a temporal dimension to a belief logic, we combine it with a linear-time temporal logic using a powerful technique called fibring for combining logics. We describe a labelled modal tableaux system for a fibred belief logic (FL) which can be used to automatically verify correctness of inter-agent stream authentication protocols. With the resulting fibred belief logic and its associated modal tableaux, one is able to build theories of trust for the description of, and reasoning about, multi-agent systems operating in dynamic environments.
Original languageEnglish
Title of host publicationProceedings of Formal Approaches to Multi-Agent Systems (FAMAS'06)
EditorsBarbara Dunin-Keplicz, Rineke Verbrugge
Place of PublicationUniversity di Trento, Italy
Number of pages16
Publication statusPublished - 2006
EventWorkshop Formal Approaches to Multi-Agent Systems (FAMAS'06) - Riva del Garda, Italy
Duration: 28 Aug 20061 Sep 2006


WorkshopWorkshop Formal Approaches to Multi-Agent Systems (FAMAS'06)
CityRiva del Garda, Italy

Fingerprint Dive into the research topics of 'Modal tableaux for verifying security protocols'. Together they form a unique fingerprint.

Cite this