Abstract
We propose a symbolic semantics for the finite applied pi calculus, which is a variant of the pi calculus with extensions for modelling cryptographic protocols. By treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms. We define a sound symbolic labelled bisimulation relation. This is an important step towards automation of observational equivalence for the finite applied pi calculus, e.g. for verification of anonymity or strong secrecy properties.
This work has been partly supported by the RNTL project POSÉ, the EPSRC projects EP/E029833, Verifying Properties in Electronic Voting Protocols and EP/E040829/1, Verifying anonymity and privacy properties of security protocols, the ARA SESUR project AVOTÉ and the ARTIST2 NoE. We also thank M. Johansson and B. Victor for interesting discussions.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: Proc. 4th Conference on Computer and Communications Security, pp. 36–47. ACM Press, New York (1997)
Amadio, R., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. Theoretical Computer Science 290, 695–740 (2002)
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. 12th Conference on Computer and Communications Security, pp. 16–25. ACM Press, New York (2005)
Baudet, M.: Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. Thèse de doctorat, LSV, ENS Cachan, France (January 2007)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: Proc. 14th Computer Security Foundations Workshop, pp. 82–96. IEEE Comp. Soc. Press, Los Alamitos (2001)
Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: Proc. 20th Symposium on Logic in Computer Science, pp. 331–340. IEEE Comp. Soc. Press, Los Alamitos (2005)
Boreale, M., Nicola, R.D.: A symbolic semantics for the pi-calculus. Information and Computation 126(1), 34–52 (1996)
Borgström, J., Briais, S., Nestmann, U.: Symbolic bisimulation in the spi calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, Springer, Heidelberg (2004)
Delaune, S., Jacquemard, F.: A decision procedure for the verification of security protocols with explicit destructors. In: Proc. 11th ACM Conference on Computer and Communications Security (CCS 2004), pp. 278–287. ACM Press, New York (2004)
Delaune, S., Kremer, S., Ryan, M.D.: Coercion-resistance and receipt-freeness in electronic voting. In: Proc. 19th Computer Security Foundations Workshop, pp. 28–39. IEEE Comp. Soc. Press, Los Alamitos (2006)
Delaune, S., Kremer, S., Ryan, M.D.: Symbolic bisimulation for the applied pi calculus. Research Report LSV-07-14, LSV, ENS Cachan, France, pp. 47 (April 2007)
Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138(2), 353–389 (1995)
Kremer, S., Ryan, M.D.: Analysis of an electronic voting protocol in the applied pi-calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)
Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. 8th Conference on Computer and Communications Security, pp. 166–175 (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delaune, S., Kremer, S., Ryan, M. (2007). Symbolic Bisimulation for the Applied Pi Calculus. In: Arvind, V., Prasad, S. (eds) FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2007. Lecture Notes in Computer Science, vol 4855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77050-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-77050-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77049-7
Online ISBN: 978-3-540-77050-3
eBook Packages: Computer ScienceComputer Science (R0)