Abstract
In the design process of distributed systems we may have to replace abstract specifications of components by more concrete specifications, thus providing more detailed design information. In the context of process algebra, this well-known approach is often referred to as action refinement. We study the relationships between action refinement and security properties within the Security Process Algebra (SPA). First we formalize the concept of action refinement as a structural inductive transformation. Then we prove several compositional results which can be exploited in the stepwise development of processes. Finally, we consider information flow security properties for SPA processes and define a decidable class of secure processes which is closed under refinement.
Supported by the MIUR projects 2005015785 “Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile” and 2005015491 “Vincoli per la programmazione con insiemi, l’analisi di sistemi con automi, il ragionamento su intervalli e la bioinformatica”.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aceto, L., Hennessy, M.: Adding Action Refinement to a Finite Process Algebra. Information and Computation 115(2), 179–247 (1994)
Bossi, A., Focardi, R., Macedonio, D., Piazza, C., Rossi, S.: Unwinding in Information Flow Security. Electronic Notes in Theoretical Computer Science 99, 127–154 (2004)
Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Refinement Operators and Information Flow Security. In: Proc. of the 1st IEEE Int. Conference on Software Engineering and Formal Methods (SEFM 2003), pp. 44–53. IEEE Computer Society Press, Los Alamitos (2003)
Bossi, A., Piazza, C., Rossi, S.: Modelling Downgrading in Information Flow Security. In: Proc. of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004), pp. 187–201. IEEE Computer Society Press, Los Alamitos (2004)
Bossi, A., Piazza, C., Rossi, S.: Action Refinement in Process Algebra and Security Issues. Technical Report CS-2007-8, Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Italy (2007)
Boudol, G.: Atomic Actions. Bulletin of the EATCS 38, 136–144 (1989)
Bravetti, M., Gorrieri, R.: Deciding and axiomatizing weak ST bisimulation for a process algebra with recursion and action refinement. ACM Transaction on Computational Logic 3(4), 465–520 (2002)
de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.): REX 1989. LNCS, vol. 430. Springer, Heidelberg (1990)
de Bakker, J.W., de Vink, E.P.: Bisimulation Semantics for Concurrency with Atomicity and Action Refinement. Fundamenta Informaticae 20(1), 3–34 (1994)
Degano, P., Gorrieri, R.: A Causal Operational Semantics of Action Refinement. Information and Computation 122(1), 97–119 (1995)
Gorrieri, R., Focardi, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2001. LNCS, vol. 2171, Springer, Heidelberg (2001)
Focardi, R., Rossi, S.: Information Flow Security in Dynamic Contexts. Journal of Computer Security 14(1), 65–110 (2006)
Foley, S.N.: A Universal Theory of Information Flow. In: Proc. of the IEEE Symposium on Security and Privacy (SSP 1987), pp. 116–122. IEEE Computer Society Press, Los Alamitos (1987)
Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. of the IEEE Symposium on Security and Privacy (SSP 1982), pp. 11–20. IEEE Computer Society Press, Los Alamitos (1982)
Goltz, U., Gorrieri, R., Rensink, A.: Comparing Syntactic and Semantic Action Refinement. Information and Computation 125(2), 118–143 (1996)
Gorrieri, R., Rensink, A.: Action Refinement. Technical Report UBLCS-99-09, University of Bologna (Italy) (1999)
Jacob, J.: On the Derivation of Secure Components. In: Proc. of the IEEE Symposium on Security and Privacy (SSP 1989), pp. 242–247. IEEE Computer Society Press, Los Alamitos (1989)
Mantel, H.: Possibilistic Definitions of Security - An Assembly Kit -. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 185–199. IEEE Computer Society Press, Los Alamitos (2000)
McLean, J.: Security Models and Information Flow. In: Proc. of the IEEE Symposium on Security and Privacy (SSP1990), pp. 180–187. IEEE Computer Society Press, Los Alamitos (1990)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Montanari, U., Sassone, V.: CCS Dynamic Bisimulation is Progressing. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol. 520, pp. 346–356. Springer, Heidelberg (1991)
Nielsen, M., Engberg, U., Larsen, K.S.: Fully Abstract Models for a Process Language with Refinement. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 523–548. Springer, Heidelberg (1989)
Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communication 21(1), 5–19 (2003)
Seehusen, F., Stølen, K.: Maintaining Information Flow Security Under Refinement and Transformation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 143–157. Springer, Heidelberg (2007)
van Glabbeek, R.J., Goltz, U.: Equivalence Notions for Concurrent Systems and Refinement of Actions. In: Kreczmar, A., Mirkowska, G. (eds.) MFCS 1989. LNCS, vol. 379, pp. 237–248. Springer, Heidelberg (1989)
van Glabbeek, R.J., Goltz, U.: Refinement of Actions and Equivalence Notions for Concurrent Systems. Acta Informatica 37(4/5), 229–327 (2001)
van Glabbeek, R.J., Vaandrager, F.W.: The Difference between Splitting in n and n+1. Information and Computation 136(2), 109–142 (1997)
Wirth, N.: Program Development by Stepwise Refinement. Communications of the ACM 14(4), 221–227 (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bossi, A., Piazza, C., Rossi, S. (2008). Action Refinement in Process Algebra and Security Issues. In: King, A. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2007. Lecture Notes in Computer Science, vol 4915. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78769-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-78769-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78768-6
Online ISBN: 978-3-540-78769-3
eBook Packages: Computer ScienceComputer Science (R0)