Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 19 / Issue 10

available in:   PDF (301 kB) PS (554 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-019-10-1396


An Algebraic Theory of Epistemic Processes

Hamid Reza Mahrooghi (Sharif University of Technology, Iran)

Rasool Jalili (Sharif University of Technology, Iran)

Abstract: In the past few years, several process-algebraic frameworks have been proposed that incorporate the notion of epistemic knowledge. These frameworks allow for reasoning about knowledge-related properties, such as anonymity, secrecy and authentication, in the operational specifications given in process-algebraic languages. Hitherto, no sound and (ground-)complete axiomatization has been given for the abovementioned process-algebraic frameworks. In this paper, we define notions of bisimulation that are suitable for such process algebras with histories and give a sound and ground-complete axiomatization for the theory of CryptoPAi, which is a process algebra based on Milner's Calculus of Communicating Systems (CCS) extended with cryptographic terms and identities. Moreover, we show that one of our defined notions of bisimulation is precisely characterized by the extension of the Hennessy-Milner logic with epistemic constructs.

Keywords: axiomatization, cryptography, epistemic logic, process algebra, security protocols

Categories: F.4, F.4.1, F.4.3