JUCS - Journal of Universal Computer Science 19(10): 1396-1432, doi: 10.3217/jucs-019-10-1396
An Algebraic Theory of Epistemic Processes
expand article infoHamid Reza Mahrooghi, Rasool Jalili
‡ Sharif University of Technology, Tehran, Iran
Open Access
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.
process algebra, epistemic logic, axiomatization, security protocols, cryptography