Abstract
We define a higher-order process calculus with algebraic operations such as encryption and decryption, and develop a bisimulation proof method for behavioral equivalence in this calculus. Such development has been notoriously difficult because of the subtle interactions among generative names, processes as data, and the algebraic operations. We handle them by carefully defining the calculus and adopting Sumii et al.’s environmental bisimulation, and thereby give (to our knowledge) the first “useful” proof method in this setting. We demonstrate the utility of our method through examples involving both higher-order processes and asymmetric cryptography.
Detailed proofs are available online [12]
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 104–115 (2001)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999); Preliminary version appeared in Proceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36–47 (1997)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: 20th Annual IEEE Symposium on Logic in Computer Science, pp. 331–340 (2005)
Borgström, J., Nestmann, U.: On bisimulations for the spi calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 287–303. Springer, Heidelberg (2002)
Maffeis, S., Abadi, M., Fournet, C., Gordon, A.D.: Code-carrying authorization. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 563–579. Springer, Heidelberg (2008)
Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigm. PhD thesis, University of Edinburgh (1992)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Appendices to “environmental bisimulations for higher-order languages”, http://www.cs.unibo.it/~sangio/DOC_public/appLICS07.pdf
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Twenty-Second Annual IEEE Symposium on Logic in Computer Science, pp. 293–302 (2007)
Sangiorgi, D., Milner, R.: The problem of “weak bisimulation up to”. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32–46. Springer, Heidelberg (1992)
Sangiorgi, D., Walker, D.: The Pi Calculus – A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Sato, N., Sumii, E.: Proofs for “the higher-order, call-by-value applied pi-calculus”, http://www.kb.ecei.tohoku.ac.jp/~nsato/hoapp.pdf
Schneier, B.: Applied Cryptography. John Wiley & Sons, Inc., Chichester (1996)
Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theoretical Computer Science 375(1-3), 169–192 (2004); Extended abstract appeared in Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161–172 (2004)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. Journal of the ACM 54(5-26), 1–43 (2007); Extended abstract appeared in Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 63–74 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sato, N., Sumii, E. (2009). The Higher-Order, Call-by-Value Applied Pi-Calculus. In: Hu, Z. (eds) Programming Languages and Systems. APLAS 2009. Lecture Notes in Computer Science, vol 5904. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10672-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-10672-9_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10671-2
Online ISBN: 978-3-642-10672-9
eBook Packages: Computer ScienceComputer Science (R0)