Modal tableaux for verifying stream authentication protocols

Mehmet A. Orgun, Guido Governatori*, Chuchang Liu

*Corresponding author for this work

Research output: Contribution to journalArticle

7 Citations (Scopus)


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 the resulting 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
Pages (from-to)53-75
Number of pages23
JournalAutonomous Agents and Multi-Agent Systems
Issue number1
Publication statusPublished - Aug 2009

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

Cite this