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.
Article PDF
Similar content being viewed by others
References
Abadi, M., & Cortier, V. (2004). Deciding knowledge in security protocols under equational theories. In ICALP04, LNCS (Vol. 3142, pp. 46–58).
Abadi, M., & Fournet, C. (2001). Mobile values, new names, and secure communication. In POPL ’01 (pp. 104–115).
Abadi M., Rogaway P. (2002) Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2): 103–127
Abadi, M., & Tuttle, M. R. (1991). A semantics for a logic of authentication (extended abstract). In PODC ’91 (pp. 201–216). New York, NY, USA.
Accorsi, R., Basin, D., & Vigano, L. (2001). Towards an awareness-based semantics for security protocol analysis. In Logical aspects of cryptographic protocol verification, ENTCS (Vol. 55, pp. 5–24).
Alur, R., Henzinger, T. A., Mang, F. Y. C., Qadeer, S., Rajamani, S. K., & Tasiran, S. (1998). Mocha: Modularity in model checking. In CAV’98, LNCS (Vol. 1427, pp. 521–525).
Alur, R., Černý, P., & Chaudhuri, S. (2007). Model checking on trees with path equivalences. In TACAS’07, LNCS (Vol. 4424, pp. 664–678).
Alur, R., Černý, P., & Zdancewic, S. (2006). Preserving secrecy under refinement. In ICALP’06, LNCS (Vol. 4052, pp. 107–118).
Anderson, R., & Needham, R. (1995). Programming Satan’s computer. In J. Leeuwen (Ed.), Computer science today, LNCS (Vol. 1000, Chap. 26, pp. 426–440). Berlin/Heidelberg: Springer.
Baltag, A., Moss, L. S., & Solecki, S. (1999). The logic of public announcements, common knowledge, and private suspicions. Technical Report SEN-R9922, CWI, Amsterdam.
Baltag A., Smets S. (2008) Probabilistic dynamic belief revision. Synthese 165(2): 179–202
Baskar, A., Ramanujam, R., & Suresh, S. P. (2007). Knowledge-based modelling of voting protocols. In TARK ’07 (pp. 62–71).
Bhargava, M., & Palamidessi, C. (2005). Probabilistic anonymity. In CONCUR’05, LNCS (Vol. 3653, pp. 171–185).
Bieber, P. (1990). A logic of communication in hostile environment. In Computer security foundations workshop III (pp. 14–22).
Boureanu I., Cohen M., Lomuscio A. (2009) Automatic verification of temporal-epistemic properties of cryptographic protocols. Journal of Applied Non-Classical Logics 19(4): 463–487
Brookes D., Hoare C. A. R., Roscoe A. W. (1984) A theory of communicating sequential processes. Journal of the ACM 31(3): 560–599
Burrows, M., Abadi, M., & Needham, R. (1989). A logic of authentication. In Proceedings of the royal society of london, Series A, Mathematical and Physical Sciences (Vol. 426(1871), pp. 233–271).
Chadha, R., Delaune, S., & Kremer, S. (2009). Epistemic logic for the applied pi calculus. In FMOODS ’09/FORTE ’09, LNCS (Vol. 5522, pp. 182–197).
Chaum D. (1988) The dining cryptographers problem: Unconditional sender and receiver untraceability. Journal of Cryptology 1: 65–75
Chaum, D., Crépeau, C., & Damgard, I. (1988). Multiparty unconditionally secure protocols. In STOC ’88 (pp. 11–19).
Ciobâcă, S., Delaune, S., & Kremer, S. (2009). Computing knowledge in security protocols under convergent equational theories. In CADE-22, LNCS (Vol. 5663, pp. 355–370).
Clarke E.M., Grumberg O., Peled D.A. (1999) Model checking. The MIT Press, Cambridge
Clarke, E. M., Jha, S., & Marrero, W. R. (1998). Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In PROCOMET ’98 (pp. 87–106).
Cohen, M., & Dam, M. (2005a). A completeness result for BAN logic. In Methods for modalities (pp. 202–219).
Cohen, M., & Dam, M. (2005b). Logical omniscience in the semantics of BAN logic. In FCS’05 (pp. 121–132).
Cohen, M., & Dam, M. (2007). A complete axiomatization of knowledge and cryptography. In LICS (pp. 77–88).
Cohen, M., Dam, M., Lomuscio, A., & Russo, F. (2009a). Abstraction in model checking multi-agent systems. In AAMAS ’09 (pp. 945–952).
Cohen, M., Lomuscio, A., Dam, M., & Qu, H. (2009b). A symmetry reduction technique for model checking temporal epistemic logic. In IJCAI’09 (pp. 721–726).
Cremers, C. J. F. (2006). Scyther—Semantics and verification of security protocols. Ph.D. dissertation, Eindhoven University of Technology.
Dechesne, F., Mousavi, M. R., & Orzan, S. (2007). Operational and epistemic approaches to protocol analysis: Bridging the gap. In LPAR (pp. 226–241).
Dechesne, F., Orzan, S., & Wang, Y. (2008). Refinement of Kripke models for dynamics. In ICTAC’08, LNCS (Vol. 5160, pp. 111–125).
Dechesne, F., & Wang, Y. (2007). Dynamic epistemic verification of security protocols: Framework and case study. In A meeting of the minds (LORI 2008), Texts in Computer Science (Vol. 8, pp. 129–144).
Delaune, S., Kremer, S., & Ryan, M. (2006). Coercion-resistance and receipt-freeness in electronic voting. In CSFW’06 (pp. 28–42).
Delaune S., Kremer S., Ryan M. (2009) Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4): 435–487
Dixon, C., Carmen, Fisher, M., & van der Hoek, W. (2003). Using temporal logics of knowledge in the formal verification of security protocols. Technical Report ULCS-03-022, University of Liverpool, Department of Computer Science.
Dolev D., Yao A. (1983) On the security of public key protocols. IEEE Transactions on Information Theory 29(2): 198–208
Durgin, N. A., Lincoln, P. D., Mitchell, J. C., & Scedrov, A. (1999). Undecidability of bounded security protocols. In Proceedings of the workshop on formal methods and security protocols.
Emerson E. A. (1987) Uniform inevitability is tree automaton ineffable. Information Processing Letters 24(2): 77–79
Engelhardt, K., Gammie, P., & van der Meyden, R. (2007). Model checking knowledge and linear time: PSPACE cases. In LFCS (pp. 195–211)
Engelhardt, K., Van Der Meyden, R., & Su, K. (2002). Modal logics with a linear hierarchy of local propositional quantifiers. In Advances in modal logic (Vol. 9, pp. 9–30).
Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1995a). Knowledge-based programs. In Symposium on principles of distributed computing (pp. 153–163).
Fagin R., Halpern J.Y., Vardi M.Y., Moses Y. (1995b) Reasoning about knowledge. MIT Press, Cambridge, MA, USA
Fischer M.J., Wright R.N. (1996) Bounds on secret key exchange using a random deal of cards. Journal of Cryptology 9: 71–99
Focardi, R., Gorrieri, R., & Martinelli, F. (2004). Classification of security properties (Part II: Network Security), In LNCS (Vol. 2946, pp. 139–185). Springer.
Gammie, P., & van der Meyden, R. (2004). MCK: Model checking the logic of knowledge. In CAV’04, LNCS (Vol. 3114 pp. 256–259). Springer.
Garcia, F. D., Hasuo, I., van Rossum, P., & Pieters, W. (2005). Provable anonymity. In Formal Methods in Security Engineering ’05 (pp. 63–72).
Gerbrandy J., Groeneveld W. (1997) Reasoning about information change. Journal of Logic, Language and Information 6(2): 147–169
Gong, L., Needham, R., & Yahalom, R. (1990). Reasoning about belief in cryptographic protocols. In Research in security and privacy. pp. 234–248.
Halpern, J., & O’Neill, K. (2002). Secrecy in multiagent systems. In Proc. 15th IEEE Computer Security Foundations Workshop (pp. 32–46).
Halpern J., O’Neill K. (2005) Anonymity and information hiding in multiagent systems. Journal of Computer Security 13(3): 483–514
Halpern J. Y., Fagin R. (1989) Modelling knowledge and action in distributed systems. Distributed Computing 3(4): 159–177
Halpern J. Y., Moses Y. (1990) Knowledge and common knowledge in a distributed environment. Journal of the ACM 37(3): 549–587
Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1994). Algorithmic knowledge. In TARK ’94 (pp. 255–266).
Halpern, J. Y., & Pucella, R. (2003a). Modeling adversaries in a logic for security protocol analysis. In Formal aspects of security, LNCS (Vol. 2629, pp. 87–100). Springer.
Halpern J. Y., Pucella R. (2003) On the relationship between strand spaces and multi-agent systems. ACM Transactions on Information and System Security 6(1): 43–70
Halpern, J. Y., & Pucella, R. (2010). Dealing with logical omniscience: Expressiveness and pragmatics. Artificial Intelligence. doi:10.1016/j.artint.2010.04.009.
Halpern, J. Y., & Vardi, M. Y. (1986). The complexity of reasoning about knowledge and time. In STOC ’86 (pp. 304–315).
Halpern, J. Y., & Vardi, M. Y. (1991). Model checking vs. theorem proving: A manifesto. In Artificial intelligence and mathematical theory of computation: Papers in honor of John McCarthy (pp. 151–176). Academic Press Professional, Inc.
Herzog J. C., Guttman J. D. (1999) Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2–3): 191–230
Hintikka J. (1962) Knowledge and belief: An introduction to the logic of the two notions. Cornell University Press, Ithaca, NY
Hommersom A., Meyer J.-J., Vink E. (2005) Update semantics of security protocols. In: Hoek W. (ed.) Information, interaction and agency. Springer, Berlin, pp 289–327
Hoshi T., Yap A. (2009) Dynamic epistemic logic with branching temporal structures. Synthese 169(2): 259–281
Hunter, A., & Delgrande, J. P. (2007). Belief change and cryptographic protocol verification. In AAAI (pp. 427–433).
Jonker, H. L., & de Vink, E. P. (2006). Formalising receipt-freeness. In Information security, LNCS (Vol. 4176, pp. 476–488).
Jonker, H. L., & Pieters, W. (2006). Receipt-freeness as a special case of anonymity in epistemic logic. In Workshop On trustworthy elections 2006.
Kacprzak M., Nabiałek W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Woźna B., Zbrzezny A. (2008) VerICS 2007—A model checker for knowledge and real-time. Fundamenta Informaticae 85(1): 313–328
Kramer, S. (2007). Logical concepts in cryptography. Ph.D. thesis, EPFL.
Läuchli H., Savioz C. (1987) Monadic second order definable relations on the binary tree. The Journal of Symbolic Logic 52(1): 219–226
Lomuscio A., Penczek W. (2007) Symbolic model checking for temporal-epistemic logics. SIGACT News 38(3): 77–99
Lomuscio, A., Qu, H., & Raimondi, F. (2009). MCMAS: A model checker for the verification of multi-agent systems. In CAV’09, LNCS (Vol. 5643, pp. 682–688).
Lomuscio, A., & Raimondi, F. (2006a). The complexity of model checking concurrent programs against CTLK specifications. In AAMAS ’06 (pp. 548–550).
Lomuscio, A., & Raimondi, F. (2006b). MCMAS: A model checker for multi-agent systems. In TACAS ’06, LNCS (Vol. 3920, pp. 450–454).
Lowe, G. (1996). Breaking and fixing the needham-schroeder public-key protocol using FDR. In TACAS ’96, LNCS (Vol. 1055, pp. 147–166).
Needham R. M., Schroeder M. D. (1978) Using encryption for authentication in large networks of computers. Communications of the ACM 21(12): 993–999
Orzan, S. (2005). LYS. Available from http://www.mobanet.nl/simona/lys/.
Parikh, R., & Ramanujam, R. (1985). Distributed processes and the logic of knowledge. In Logic of programs, LNCS (Vol. 193, pp. 256–268).
Parikh R., Ramanujam R. (2003) A knowledge based semantics of messages. Journal of Logic, Language and Information 12(4): 453–467
Paulson, L. C. (1997). Proving properties of security protocols by induction. In 10th Computer Security Foundations Workshop (pp. 70–83).
Paulson L. C. (1998) The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6: 85–128
Petride, S., & Pucella, R. (2007). Perfect cryptography, S5 knowledge, and algorithmic knowledge. In TARK ’07 (pp. 239–247).
Plaza, J. A. (1989). Logics of public communications. In Proceedings of the 4th international symposium on methodologies for intelligent systems (pp. 201–216).
Pucella R. (2006) Deductive algorithmic knowledge. Journal of Logic and Computation 16(2): 287–309
Ramanujam R., Suresh S. P. (2005a) Decidability of context-explicit security protocols. Journal of Computer Security 13(1): 135–165
Ramanujam, R., & Suresh, S. P. (2005b). Deciding knowledge properties of security protocols. In TARK ’05 (pp. 219–235).
Reiter M. K., Rubin A. D. (1998) Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security 1: 66–92
Ryan P., Schneider S. (2001) Modelling and analysis of security protocols. Reading, MA, USA, Addison Wesley
Shilov, N. V., & Garanina, N. O. (2002). Model checking knowledge and fixpoints. In FICS, BRICS notes series (Vol. NS-02-2, pp. 25–39).
Shmatikov V. (2004) Probabilistic model checking of an anonymity system. Journal of Computer Security 12(3/4): 355–377
Su, K. (2004). Model checking temporal logics of knowledge in distributed systems. In AAAI (pp. 98–103).
Syverson P. F. (1992) Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security 1(3–4): 317–334
Syverson, P. F., & Stubblebine, S. G. (1999). Group principals and the formalization of anonymity. In World congress on formal methods, LNCS (Vol. 1708, pp. 814–833).
Teepe, W. (2006). BAN logic is not ‘sound’, constructing epistemic logics for security is difficult. In Proceedings of FAMAS’06 (pp. 79–91).
van Benthem J., Gerbrandy J., Hoshi T., Pacuit E. (2009) Merging frameworks for interaction. Journal of Philosophical Logic 38(5): 491–526
van Benthem, J., Gerbrandy, J., & Pacuit, E. (2007). Merging frameworks for interaction: DEL and ETL. In TARK ’07 (pp. 72–81).
van Benthem J., van Eijck J., Kooi B. (2006) Logics of communication and change. Information and Computation 204(11): 1620–1662
van der Hoek, W., & Wooldridge, M. (2002). Tractable multiagent planning for epistemic goals. In AAMAS ’02 (pp. 1167–1174).
van der Meyden, R., & Shilov, N. (1999). Model checking knowledge and time in systems with perfect recall. In FSTTCS ’99, LNCS (Vol. 1738, pp. 432–445).
van der Meyden, R., & Su, K. (2004). Symbolic model checking the knowledge of the dining cryptographers. In CSFW ’04 (pp. 280–291).
van der Meyden, R., & Wilke, T. (2007). Preservation of epistemic properties in security protocol implementations. In TARK ’07 (pp. 212–221).
van Ditmarsch H. (2003) The Russian cards problem. Studia Logica 75(1): 31–62
van Ditmarsch, H. (2008). Unconditionally secure protocols with card deals. Presentation, available at http://www.cs.otago.ac.nz/staffpriv/hans/lorentz/niaslorentz.pdf.
van Ditmarsch, H., van der Hoek, W., van der Meyden, R., & Ruan, J. (2006). Model checking Russian cards. In MoChArt 05, ENTCS (Vol. 149(2), pp. 105–123).
van Eijck, J. (2005). DEMO program and documentation. Available from http://www.cwi.nl/~jve/demo/.
van Eijck J., Orzan S. (2007) Epistemic verification of anonymity. Electronic Notes in Theoretical Computer Science 168: 159–174
Von Wright G. H. (1951) An essay in modal logic. North Holland, Amsterdam
Wang, Y., Kuppusamy, L., & van Eijck, J. (2009). Verifying epistemic protocols under common knowledge. In TARK ’09 (pp. 257–266).
Wang, Y., Sietsma, F., & van Eijck, J. (2010). Logic of information flow on communication channels (extended abstract). In AAMAS ’10 (to appear).
Acknowledgements
The authors would like to thank the anonymous referees for their insightful comments and Ramaswamy Ramanujam for the discussions on various issues that motivated this work.
Open Access
This article is distributed under the terms of the Creative Commons Attribution Noncommercial License which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
Author information
Authors and Affiliations
Corresponding author
Additional information
The work presented in this paper is part of the project Verification and Epistemics of Multi-Party Protocol Security funded by the Netherlands Organisation for Scientific Research (NWO project VEMPS 612.000.528, 2006–2010). Affiliation of F. Dechesne during the VEMPS-project: Formal Methods Group, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven. Affiliation of Y. Wang during the VEMPS-project: Centrum voor Wiskunde en Informatica (CWI), Amsterdam, The Netherlands.
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License (https://creativecommons.org/licenses/by-nc/2.0), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Dechesne, F., Wang, Y. To know or not to know: epistemic approaches to security protocol verification. Synthese 177 (Suppl 1), 51–76 (2010). https://doi.org/10.1007/s11229-010-9765-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11229-010-9765-8