To know or not to know: epistemic approaches to security protocol verification.
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 an...
| Publicado en: | Synthese Vol. 177; pp. 51 - 77 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Springer Nature
Dec2010 Supplement
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=56526544&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 56526544 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00397857 4LI jtl: Synthese issn: 00397857 maglogo: N pubinfo: dt: Dec2010 Supplement vid: 177 pid: 237 pub: Springer Nature artinfo: ui: 56526544 10.1007/s11229-010-9765-8 ppf: 51 ppct: 26 formats: fmt: @attributes: type: P size: 379KB tig: atl: To know or not to know: epistemic approaches to security protocol verification. aug: au: Dechesne, Francien Yanjing Wang affil: Philosophy section, Department of Technology, Policy and Management, Delft University of Technology, Delft, The Netherlands Department of Philosophy, Peking University, Beijing, China su: Computer security Computer network protocols Intelligent agents Computer logic Programming languages sug: subj: Computer security Computer network protocols Intelligent agents Computer logic Programming languages keyword: Dynamic epistemic logic Epistemic temporal logic Interpreted systems Security protocols Verification ab: 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. pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y custom: Synthese is a copyright of Springer, 2010. All Rights Reserved. item: Synthese holder: Springer Nature dt: @attributes: year: 2010 holdings: @attributes: islocal: N |
|---|