Abstract
We introduce a theory of weak bisimilarity for the π-calculus with linear type structure [35] in which we abstract away not only τ - actions but also non-τ actions which do not affect well-typed environments. This gives an equivalence far larger than the standard bisimilarity while retaining semantic soundness. The congruency of the bisimilarity relies on a liveness property at linear channels ensured by typing. The theory is consistently extendible to settings which involve nontermination, nondeterminism and state. As an application we develop a behavioural theory of secrecy for the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach in [20][23].
Partially supported by EPSRC grant GR/R33465/01.
Partially supported by EPSRC grant GR/N/37633.
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., Secrecy by typing in security protocols. Journal of the ACM, 46(5):749–786, 1999.
Abadi, M., Secrecy in programming-language semantics, MFPS XV, ENTCS, 20 (April 1999).
Abadi, M., Banerjee, A., Heintze, N. and Riecke, J., A core calculus of dependency, POPL’99, ACM, 1999.
Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF. Info. & Comp. 163(2000), 409–470.
Boreale, M. and Sangiorgi, D. Bisimulation in name-passing calculi without matching. LICS’98, IEEE, 1998.
Berger, M., Honda, K. and Yoshida, N., Sequentiality and the π-Calculus, TLCA’01, LNCS 2044, 29–45, Springer, 2001. The full version available at http://www.dcs.qmw.ac.uk/~kohei.
Boudol, G. and Castellani, I., Noninterference for Concurrent Programs, ICALP’01, LNCS, Springer, 2001.
Denning, D. and Denning, P., Certification of programs for secure information flow. Communication of ACM, ACM, 20:504–513, 1997.
Focardi, R. and Gorrieri, R., The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering, 23(9), 1997.
Focardi, R., Gorrieri, R. and Martinelli, F., Non-interference for the analysis of cryptographic protocols. ICALP’00, LNCS 1853, Springer, 2000.
Gay, S. and Hole, M., Types and Subtypes for Client-Server Interactions, ESOP’99, LNCS 1576, 74–90, Springer, 1999.
Girard, J.-Y., Linear Logic, TCS, 50, 1–102, 1987.
Hennessy, M. and Rathke, J., Typed behavioural equivalences for processes in the presence of subtyping, To appear in Proc. CATS 2002.
Hennessy, M. and Riely, J., Information flow vs resource access in the asynchronous pi-calculus, ICALP’00, LNCS 1853, 415–427, Springer, 2000.
Honda, K., Types for Dyadic Interaction. CONCUR’93, LNCS 715, 509–523, 1993.
Honda, K., Composing Processes, POPL’96, 344–357, ACM, 1996.
Honda, K., Notes on Linear Typing for Free Outputs, May, 2001.
Honda, K., Kubo, M. and Vasconcelos, V., Language Primitives and Type Discipline for Structured Communication-Based Programming. ESOP’98, LNCS 1381, 122–138. Springer-Verlag, 1998.
Honda, K. and Tokoro, M. An object calculus for asynchronous communication. ECOOP’91, LNCS 512, 133–147, 1991.
Honda, K., Vasconcelos, V. and Yoshida, N., Secure Information Flow as Typed Process Behaviour, ESOP’00, LNCS 1782, 180–199, 2000.
Honda, K. and Yoshida, N. On Reduction-Based Process Semantics. TCS, 151, 437–486, 1995.
Honda, K. and Yoshida, N., Game-theoretic analysis of call-by-value computation. TCS, 221 (1999), 393–456, 1999.
Honda, K. and Yoshida, N., A uniform type structure for secure information flow, To appear in POPL’02, ACM, 2002.
Hyland, M. and Ong, L., “On Full Abstraction for PCF”: I, II and III. Info. & Comp. 163(2000), 285–408, 2000.
Kobayashi, N., Pierce, B., and Turner, D., Linearity and the π-calculus, POPL’96, 358–371, 1996.
Milner, R., Functions as Processes. MSCS, 2(2), 119–146, CUP, 1992.
Milner, R. and Sangiorgi, D., Barbed Bisimulation, ICALP’92, LNCS 623, 685–695, Springer, 1992.
Philippou, A. and Walker, D., On confluence in the π-Calculus, ICALP’97, LNCS 1256, 314–324, Springer, 1997.
Sangiorgi, D. π-calculus, internal mobility, and agent-passing calculi. TCS, 167(2):235–271, 1996.
Sangiorgi, D., The name discipline of uniform receptiveness, TCS, 221, 457–493, 1999.
Sabelfield, A. and Sands, D. A per model of secure information flow in sequential programs. ESOP’99, LNCS 1576, Springer, 1999.
Smith, G. and Volpano, D., Secure information flow in a multi-threaded imperative language, 355–364, POPL’98, ACM, 1998.
Vasconcelos, V., Typed concurrent objects. ECOOP’94, LNCS 821, 100–117. Springer, 1994.
Yoshida, N. Graph Types for Mobile Processes. FST/TCS’16, LNCS 1180, 371–386, Springer, 1996.
Yoshida, N., Berger, M. and Honda, K., Strong Normalisation in the π-Calculus, LICS’01, IEEE, 2001. The full version as MCS technical report, 2001-09, University of Leicester, 2001. Available at http://www.mcs.le.ac.uk/~nyoshida/paper.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yoshida, N., Honda, K., Berger, M. (2002). Linearity and Bisimulation. In: Nielsen, M., Engberg, U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2002. Lecture Notes in Computer Science, vol 2303. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45931-6_29
Download citation
DOI: https://doi.org/10.1007/3-540-45931-6_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43366-8
Online ISBN: 978-3-540-45931-6
eBook Packages: Springer Book Archive