Formalising theories of trust for authentication protocols

Ji Ma*, Mehmet A. Orgun

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)


This paper discusses a formal approach for establishing theories of trust for authentication systems which can be used to reason about how agent beliefs evolve through time. The goal of an authentication system is to verify and authorise users in order to protect restricted data and information, so trust is a critical issue for authentication systems. After authentication, two principals (people, computers, services) should be entitled to believe that they are communicating with each other and not with intruders. So, it is important to express such beliefs precisely and to capture the reasoning that leads to them. In this paper, we focus on analysis of agent beliefs in dynamic environments using a temporalised belief logic, obtained by adding a temporal logic onto a belief logic. Working through a well-known authentication protocol, namely Kerberos, we discuss how to express principal beliefs involved in authentication protocols and the evolution of those beliefs based on a series of observations of agents as a consequence of communication. Our approach could be used for designing, verifying and implementing authentication protocols.

Original languageEnglish
Pages (from-to)19-32
Number of pages14
JournalInformation Systems Frontiers
Issue number1
Publication statusPublished - Mar 2008


Dive into the research topics of 'Formalising theories of trust for authentication protocols'. Together they form a unique fingerprint.

Cite this