Abstract
We propose an epistemic logic for the applied pi calculus, which is a variant of the pi calculus with extensions for modeling cryptographic protocols. In such a calculus, the security guarantees are usually stated as equivalences. While process calculi provide a natural means to describe the protocols themselves, epistemic logics are often better suited for expressing certain security properties such as secrecy and anonymity.
We intend to bridge the gap between these two approaches: using the set of traces generated by a process as models, we define a logic which has constructs for reasoning about both intruder’s epistemic knowledge and the set of messages in possession of the intruder. As an example we consider two formalizations of privacy in electronic voting and study the relationship between them.
This work has been partially supported by ANR SeSur AVOTÉ and NSF CCF 0448178.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 387(1-2), 2–32 (2006)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages, pp. 104–115 (2001)
Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: Proc. 29th IEEE Symposium on Security and Privacy (2008)
Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: Proc. 11th Conference on Theoretical Aspects of Rationality and Knowledge, pp. 62–71 (2007)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: Proc. 14th Computer Security Foundations Workshop, pp. 82–96 (2001)
Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: 9th International Static Analysis Symposium, pp. 342–359 (2002)
Borgström, J., Kramer, S., Nestmann, U.: Calculus of Cryptographic Communication. In: Proc. Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (2006)
Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)
Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi-calculus. Research Report LSV-09-06, Laboratoire Spécification et Vérification, ENS Cachan, France (March 2009)
Chadha, R., Kremer, S., Scedrov, A.: Formal analysis of multi-party contract signing. Journal of Automated Reasoning 36(1-2), 39–83 (2006)
Cohen, M., Dam, M.: A complete axiomatization of knowledge and cryptography. In: Proc. 22nd IEEE Symposium on Logic in Computer Science, pp. 77–88 (2007)
Corin, R., Saptawijaya, A., Etalle, S.: PS-LTL for constraint-based security protocol analysis. In: Proc. 21st International Conference on Logic Programming, pp. 439–440 (2005)
Dechesne, F., Mousavi, M.R., Orzan, S.: Operational and epistemic approaches to protocol analysis: Bridging the gap. In: Proc. 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 226–241 (2007)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security (2009) (to appear)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. Journal of Computer Security 13(3), 483–512 (2005)
Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. Journal of Computer Security 12(1), 3–36 (2004)
Hüttel, H., Pedersen, M.D.: A logical characterisation of static equivalence. Electr. Notes Theor. Comput. Sci. 173, 139–157 (2007)
Jonker, H., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proc. IAVoSS Workshop On Trustworthy Elections (2006)
van Eijck, J., Orzan, S.: Epistemic verification of anonymity. Electr. Notes Theor. Comput. Sci. 168, 159–174 (2007)
Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: Proc. 14th IEEE Symposium on Security and Privacy (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 IFIP International Federation for Information Processing
About this paper
Cite this paper
Chadha, R., Delaune, S., Kremer, S. (2009). Epistemic Logic for the Applied Pi Calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2009 2009. Lecture Notes in Computer Science, vol 5522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02138-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-02138-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02137-4
Online ISBN: 978-3-642-02138-1
eBook Packages: Computer ScienceComputer Science (R0)