|Title||To know or not to know: epistemic approaches to security protocol verification|
|Affiliation||Delft Univ Technol, Dept Technol Policy & Management, Philosophy Sect, Delft, Netherlands.|
Peking Univ, Dept Philosophy, Beijing 100871, Peoples R China.
Dynamic epistemic logic
Epistemic temporal logic
|Abstract||Security properties naturally combine temporal aspects of protocols with aspects of knowledge of the agents. Since BAN-logic, there have been several initiatives and attempts to incorporate epistemics into the analysis of security protocols. In this paper, we give an overview of work in the field and present it in a unified perspective, with comparisons on technical subtleties that have been employed in different approaches. Also, we study to which degree the use of epistemics is essential for the analysis of security protocols. We look for formal conditions under which knowledge modalities can bring extra expressive power to pure temporal languages. On the other hand, we discuss the cost of the epistemic operators in terms of model checking complexity.|
|Appears in Collections:||哲学系（宗教学系）|