Abstract
We study a higher-order concurrent language with cryptographic primitives, for which we develop a sound and complete, first-order testing theory for the preservation of safety properties. Our theory is based on co-inductive set simulations over transitions in a first-order Labelled Transition System. This keeps track of the knowledge of the observer, and treats transmitted higher-order values in a symbolic manner, thus obviating the quantification over functional contexts. Our characterisation provides an attractive proof technique, and we illustrate its usefulness in proofs of equivalence, including cases where bisimulation theory does not apply.
This research was supported by SFI project SFI 06 IN.1 1898.
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., Fournet, C.: Mobile values, new names, and secure communication. SIGPLAN Not. 36(3), 104–115 (2001)
Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nordic Journal of Computing 5, 267–303 (1998)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Inf. Comput. 148(1), 1–70 (1999)
Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput. 31(3), 947–986 (2001)
Borgström, J., Briais, S., Nestmann, U.: Symbolic bisimulation in the spi calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 161–176. Springer, Heidelberg (2004)
Borgström, J., Nestmann, U.: On bisimulations for the spi calculus. Math. Structures in Comp. Sc. 15(3), 487–552 (2005)
De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. Theoretical Computer Science 34(1-2), 83–133 (1984)
Delaune, S., Kremer, S., Ryan, M.D.: Symbolic bisimulation for the applied pi calculus. J. of Comp. Security 18(2), 317–377 (2010)
Durante, L., Sisto, R., Valenzano, A.: Automatic testing equivalence verification of spi calculus specifications. ACM Trans. Softw. Eng. Methodol. 12(2), 222–284 (2003)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization in distributed systems. In: CSF 2007, pp. 31–48. IEEE Computer Society, Los Alamitos (2007)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Hennessy, M.: The security pi-calculus and non-interference. J. Log. Algebr. Program 63(1), 3–34 (2005)
Honda, K., Yoshida, N.: A uniform type structure for secure information flow. ACM Trans. Program. Lang. Syst. 29(6) (2007)
Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order pi-calculus revisited. LMCS 1(1:4) (2005)
Koutavas, V., Hennessy, M.: First-order reasoning for higher-order concurrency (February 2010) (manuscript)
Laird, J.: Game semantics for higher-order concurrency. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 417–428. Springer, Heidelberg (2006)
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)
Milner, R.: Comunicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, Univ. of Edinburgh (1992)
Sangiorgi, D.: From pi-calculus to higher-order pi-calculus–and back. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 151–166. Springer, Heidelberg (1993)
Sangiorgi, D.: Bisimulation for higher-order process calculi. Information and Computation 131(2), 141–178 (1996)
Sangiorgi, D.: On the bisimulation proof method. Mathematical Structures in Comp. Sci. 8(5), 447–479 (1998)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: LICS (2007)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Sato, N., Sumii, E.: The higher-order, call-by-value applied pi-calculus. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 311–326. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Koutavas, V., Hennessy, M. (2011). A Testing Theory for a Higher-Order Cryptographic Language. In: Barthe, G. (eds) Programming Languages and Systems. ESOP 2011. Lecture Notes in Computer Science, vol 6602. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19718-5_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-19718-5_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19717-8
Online ISBN: 978-3-642-19718-5
eBook Packages: Computer ScienceComputer Science (R0)