2005
Conference article
Open Access
Team automata for security - a survey
Ter Beek Mh, Lenzini G, Petrocchi M
Access control Computer Science(all) D.4.6 Security and Protection. Verification Theoretical Computer Science Team automata General Computer Science F.1. Models of Computation. Automata K.6.5 Security and Protection Security
In [Kleijn, J., Team Automata for CSCW - A Survey -, Petri Net Technology for Communication-Based Systems-Advances in Petri Nets, LNCS 2472, Springer, 2003, 295-320], Kleijn presented a survey of the use of team automata for the specification and analysis of phenomena from the field of computer supported cooperative work, in particular notions related to groupware systems. In this paper we present a survey of the use of team automata for the specification and analysis of some issues from the field of security. In particular, we show how team automata can adequately be used to model and verify various access control policies, multicast/broadcast communication protocols, and general (cryptographic) communication protocols.
Source: Electronic Notes in Theoretical Computer Science ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. London, 30 August 2004
Publisher: Elsevier
[1] Alur, R., and D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126 (1994), 183-235.
[2] ter Beek, M.H., “Team Automata-A Formal Approach to the Modeling of Collaboration Between System Components”, Ph.D. thesis, Leiden Institute of Advanced Computer Science, Leiden University, 2003.
[3] ter Beek, M.H., and R.P. Bloem, Model Checking Team Automata for Access Control, unpublished manuscript, 2003.
[4] ter Beek, M.H., C.A. Ellis, J. Kleijn, and G. Rozenberg, Team Automata for Spatial Access Control, Proc. ECSCW'01, Kluwer, 2001, 59-77.
[5] ter Beek, M.H., C.A. Ellis, J. Kleijn, and G. Rozenberg, Synchronizations in team automata for groupware systems, Computer Supported Cooperative Work-The Journal of Collaborative Computing 12, 1 (2003), 21-69.
[6] ter Beek, M.H., G. Lenzini, and M. Petrocchi, Team Automata for Security Analysis of Multicast/Broadcast Communication, Tech. Rep. 2003-TR-13, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche, 2003. Presented at WISP'03, 2003 (no formal proceedings).
[7] ter Beek, M.H., G. Lenzini, and M. Petrocchi, Team Automata for Security Analysis, Tech. Rep. TR-CTIT-04-13, Centre for Telematics and Information Technology, University of Twente, 2004. Presented at the DIMACS Workshop on Security Analysis of Protocols, 2004 (no formal proceedings).
[8] Bell, D.E., and L.J. La Padula, Secure Computer Systems-Unified Exposition and Multics Interpretation, Tech. Rep. ESD-TR-75-306, MITRE MTR-2997, 1976.
[9] Bullock, A., and S. Benford, Access Control in Virtual Environments, Proc. VRST'97, ACM Press, 1997, 29-35.
[10] Bullock, A., and S. Benford, An access control framework for multi-user collaborative environments, Proc. GROUP'99, ACM Press, 1999, 140-149.
[11] Chen, H., and D. Wagner, MOPS: an Infrastructure for Examining Security Properties of Software, Proc. CCS'02, ACM Press, 2002, 235-244.
[12] Chen, H., D. Wagner, and D. Dean, Setuid Demystified, Proc. Security'02, USENIX, 2002, 171-190.
[13] Dewan, P., and H. Shen, Flexible Meta Access-Control for Collaborative Applications, Proc. CSCW'98, ACM Press, 1998, 247-256.
[14] Diffie, W., and M. Hellman, New Directions in Cryptography, IEEE Transactions on Information Theory 22, 6 (1976), 644-656.
[15] Dolev, D., and A. Yao, On the security of public-key protocols, IEEE Transactions on Information Theory 2, 29 (1983), 198-208.
[16] Egidi, L., and M. Petrocchi, Modelling a Secure Agent with Team Automata, Tech. Rep. TRINF-2004-07-08-UNIPMN, Dipartimento di Informatica, Universit`a degli Studi del Piemonte Orientale Amedeo Avogadro, July 2004.
[17] Ellis, C.A., and K.-H. Kim, A Framework and Taxonomy for Workflow Architectures, Designing Cooperative Systems: The Use of Theories and Models-Proc. COOP'00, IOS Press, 2000, 99- 112.
[18] Ellis, C.A., Team Automata for Groupware Systems, Proc. GROUP'97, ACM Press, 1997, 415-424.
[19] Engels, G., and L.P.J. Groenewegen, Towards Team-Automata-Driven Object-Oriented Collaborative Work, Formal and Natural Computing, LNCS 2300, Springer, 2002, 257-276.
[20] Focardi, R., and R. Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security 3, 1 (1994), 5-33.
[21] Focardi, R., and R. Gorrieri, The Compositional Security Checker-a Tool for the Verification of Information Flow Security Properties, IEEE Transactions on Software Engineering 23, 9 (1997), 550-571.
[22] Focardi, R., and R. Gorrieri, Classification of Security Properties-Part II: Information Flow, Proc. FOSAD 2001-Tutorial Lectures, LNCS 2171, Springer, 2001, 331-396.
[23] Focardi, R., R. Gorrieri, and F. Martinelli, Non Interference for the Analysis of Cryptographic Protocols, Proc. ICALP'00, LNCS 1853, Springer, 2000, 354-372.
[24] Focardi, R., R. Gorrieri, and F. Martinelli, Secrecy in Security Protocols as Non Interference, ENTCS 32, 2000.
[25] Focardi, R., R. Gorrieri, and F. Martinelli, Classification of Security Properties-Part II: Network Security, Proc. FOSAD 2001/2002 Tutorial Lectures, LNCS 2946, Springer, 2004, 139-185.
[26] Focardi, R., and F. Martinelli, A Uniform Approach for the Definition of Security Properties, Proc. FM'99, LNCS 1708, Springer, 1999, 794-813.
[27] Garland, S.J., and N.A. Lynch, The IOA Language and Toolset-Support for Designing, Analyzing, and Building Distributed Systems, Tech. Rep. MIT/LCS/TR-762, MIT, 1998.
[28] Goguen, J.A., and J. Meseguer, Security Policy and Security Models, Proc. S&P'82, IEEE Press, 1982, 11-20.
[29] Gu¨rgens, S., P. Ochsenschl¨ager, and C. Rudolph, Role Based Specification and Security Analysis of Cryptographic Protocols Using Asynchronous Product Automata, Proc. DEXA'02, IEEE Press, 2002, 473-482.
[30] 't Hoen, P.J., “Towards Distributed Development of Large Object-Oriented Models-Views of Packages as Classes”, Ph.D. thesis, Leiden Institute of Advanced Computer Science, Leiden University, 2001.
[31] 't Hoen, P.J., and M.H. ter Beek, A Conflict-Free Strategy for Team-Based Model Development, Proc. PDTSD'00, 2000, 720-725.
[32] Holzmann, G.J., “The SPIN Model Checker-Primer and Reference Manual”, Addison Wesley, 2003.
[33] Kleijn, J., Team Automata for CSCW - A Survey -, Petri Net Technology for CommunicationBased Systems-Advances in Petri Nets, LNCS 2472, Springer, 2003, 295-320.
[34] Kurshan, R.P., “Computer-Aided Verification of Coordinating Processes-The AutomataTheoretic Approach”, Princeton Univ. Press, 1994.
[35] Lanotte, R., A. Maggiolo-Schettini, and A. Troina, Weak Bisimulation for Probabilistic Timed Automata and Applications to Security, Proc. SEFM'03, IEEE Press, 2003, 34-43.
[36] Lavana, H., “A Universally Configurable Architecture for Taskflow-Oriented Design of a Distributed Collaborative Computing Environment”, Ph.D. thesis, Department of Electrical and Computer Engineering, North Carolina State University, 2000.
[37] Lowe, G., Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proc. TACAS'96, LNCS 1055, Springer, 1996, 147-166.
[38] Lynch, N.A., I/O Automaton Models and Proofs for Shared-Key Communi- cation Systems, Proc. CSFW'99, IEEE Press, 1999, 14-31.
[39] Lynch, N.A., Input/Output Automata: Basic, Timed, Hybrid, Probabilistic, Dynamic,..., Proc. CONCUR'03, LNCS 2761, Springer, 1996, 191-192.
[40] Lynch, N.A., and M.R. Tuttle, An Introduction to Input/Output Automata, CWI Quarterly 2, 3 (1989), 219-246. Tech. Memo MIT/LCS/TM-373, 1988.
[41] Martinelli, F., M. Petrocchi, and A. Vaccarelli, Compositional Verification of Secure Streamed Data: a Case Study with EMSS, Proc. ICTCS'03, LNCS 2841, Springer, 2003, 383-396.
[42] Nipkow, T., L.C. Paulson, and M. Wenzel, “Isabelle/HOL-A Proof Assistant for Higher-Order Logic”, LNCS 2283, Springer, 2002. For an up-to-date description, see http://isabelle.in.tum.de/.
[43] Moskowitz, I.S., and O.L. Costich, A Classical Automata Approach to Noninterference Type Problems, Proc. CSFW'92, IEEE Press, 1992, 2-8.
[44] von Oheimb, D., Interacting State Machines-A Stateful Approach to Proving Security, Proc. FASec'02, LNCS 2629, Springer, 2003, 15-32.
[45] von Oheimb, D., and V. Lotz, Formal Security Analysis with Interacting State Machines, Proc. ESORICS'02, LNCS 2502, Springer, 2002, 212-228.
[46] Perrig, A., R. Canetti, J.D. Tygar, and D.X. Song, Efficient Authentication and Signing of Multicast Streams over Lossy Channels, Proc. S&P'00, IEEE Press, 2000, 56-73.
[47] Schneider, F.B., Enforceable Security Policies, ACM Transactions on Information and System Security 3, 1 (2000), 30-50.
[48] Segala, R., A Compositional Trace-Based Semantics for Proc. CONCUR'95, LNCS 962, Springer, 1995, 234-248.
[49] Tuttle, M.R., “Hierarchical Correctness Proofs for Distributed Algorithms”, Master's thesis, Dept. of Electrical Engineering and Computer Science, MIT, 1987. Tech. Rep. MIT/LCS/TR387, 1987.
[50] The TA webpage: http://fmt.isti.cnr.it/ mtbeek/TA.html. The TA bibliography: http://liinwww.ira.uka.de/bibliography/Theory/TA.html.
[2] ter Beek, M.H., “Team Automata-A Formal Approach to the Modeling of Collaboration Between System Components”, Ph.D. thesis, Leiden Institute of Advanced Computer Science, Leiden University, 2003.
[3] ter Beek, M.H., and R.P. Bloem, Model Checking Team Automata for Access Control, unpublished manuscript, 2003.
[4] ter Beek, M.H., C.A. Ellis, J. Kleijn, and G. Rozenberg, Team Automata for Spatial Access Control, Proc. ECSCW'01, Kluwer, 2001, 59-77.
[5] ter Beek, M.H., C.A. Ellis, J. Kleijn, and G. Rozenberg, Synchronizations in team automata for groupware systems, Computer Supported Cooperative Work-The Journal of Collaborative Computing 12, 1 (2003), 21-69.
[6] ter Beek, M.H., G. Lenzini, and M. Petrocchi, Team Automata for Security Analysis of Multicast/Broadcast Communication, Tech. Rep. 2003-TR-13, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche, 2003. Presented at WISP'03, 2003 (no formal proceedings).
[7] ter Beek, M.H., G. Lenzini, and M. Petrocchi, Team Automata for Security Analysis, Tech. Rep. TR-CTIT-04-13, Centre for Telematics and Information Technology, University of Twente, 2004. Presented at the DIMACS Workshop on Security Analysis of Protocols, 2004 (no formal proceedings).
[8] Bell, D.E., and L.J. La Padula, Secure Computer Systems-Unified Exposition and Multics Interpretation, Tech. Rep. ESD-TR-75-306, MITRE MTR-2997, 1976.
[9] Bullock, A., and S. Benford, Access Control in Virtual Environments, Proc. VRST'97, ACM Press, 1997, 29-35.
[10] Bullock, A., and S. Benford, An access control framework for multi-user collaborative environments, Proc. GROUP'99, ACM Press, 1999, 140-149.
[11] Chen, H., and D. Wagner, MOPS: an Infrastructure for Examining Security Properties of Software, Proc. CCS'02, ACM Press, 2002, 235-244.
[12] Chen, H., D. Wagner, and D. Dean, Setuid Demystified, Proc. Security'02, USENIX, 2002, 171-190.
[13] Dewan, P., and H. Shen, Flexible Meta Access-Control for Collaborative Applications, Proc. CSCW'98, ACM Press, 1998, 247-256.
[14] Diffie, W., and M. Hellman, New Directions in Cryptography, IEEE Transactions on Information Theory 22, 6 (1976), 644-656.
[15] Dolev, D., and A. Yao, On the security of public-key protocols, IEEE Transactions on Information Theory 2, 29 (1983), 198-208.
[16] Egidi, L., and M. Petrocchi, Modelling a Secure Agent with Team Automata, Tech. Rep. TRINF-2004-07-08-UNIPMN, Dipartimento di Informatica, Universit`a degli Studi del Piemonte Orientale Amedeo Avogadro, July 2004.
[17] Ellis, C.A., and K.-H. Kim, A Framework and Taxonomy for Workflow Architectures, Designing Cooperative Systems: The Use of Theories and Models-Proc. COOP'00, IOS Press, 2000, 99- 112.
[18] Ellis, C.A., Team Automata for Groupware Systems, Proc. GROUP'97, ACM Press, 1997, 415-424.
[19] Engels, G., and L.P.J. Groenewegen, Towards Team-Automata-Driven Object-Oriented Collaborative Work, Formal and Natural Computing, LNCS 2300, Springer, 2002, 257-276.
[20] Focardi, R., and R. Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security 3, 1 (1994), 5-33.
[21] Focardi, R., and R. Gorrieri, The Compositional Security Checker-a Tool for the Verification of Information Flow Security Properties, IEEE Transactions on Software Engineering 23, 9 (1997), 550-571.
[22] Focardi, R., and R. Gorrieri, Classification of Security Properties-Part II: Information Flow, Proc. FOSAD 2001-Tutorial Lectures, LNCS 2171, Springer, 2001, 331-396.
[23] Focardi, R., R. Gorrieri, and F. Martinelli, Non Interference for the Analysis of Cryptographic Protocols, Proc. ICALP'00, LNCS 1853, Springer, 2000, 354-372.
[24] Focardi, R., R. Gorrieri, and F. Martinelli, Secrecy in Security Protocols as Non Interference, ENTCS 32, 2000.
[25] Focardi, R., R. Gorrieri, and F. Martinelli, Classification of Security Properties-Part II: Network Security, Proc. FOSAD 2001/2002 Tutorial Lectures, LNCS 2946, Springer, 2004, 139-185.
[26] Focardi, R., and F. Martinelli, A Uniform Approach for the Definition of Security Properties, Proc. FM'99, LNCS 1708, Springer, 1999, 794-813.
[27] Garland, S.J., and N.A. Lynch, The IOA Language and Toolset-Support for Designing, Analyzing, and Building Distributed Systems, Tech. Rep. MIT/LCS/TR-762, MIT, 1998.
[28] Goguen, J.A., and J. Meseguer, Security Policy and Security Models, Proc. S&P'82, IEEE Press, 1982, 11-20.
[29] Gu¨rgens, S., P. Ochsenschl¨ager, and C. Rudolph, Role Based Specification and Security Analysis of Cryptographic Protocols Using Asynchronous Product Automata, Proc. DEXA'02, IEEE Press, 2002, 473-482.
[30] 't Hoen, P.J., “Towards Distributed Development of Large Object-Oriented Models-Views of Packages as Classes”, Ph.D. thesis, Leiden Institute of Advanced Computer Science, Leiden University, 2001.
[31] 't Hoen, P.J., and M.H. ter Beek, A Conflict-Free Strategy for Team-Based Model Development, Proc. PDTSD'00, 2000, 720-725.
[32] Holzmann, G.J., “The SPIN Model Checker-Primer and Reference Manual”, Addison Wesley, 2003.
[33] Kleijn, J., Team Automata for CSCW - A Survey -, Petri Net Technology for CommunicationBased Systems-Advances in Petri Nets, LNCS 2472, Springer, 2003, 295-320.
[34] Kurshan, R.P., “Computer-Aided Verification of Coordinating Processes-The AutomataTheoretic Approach”, Princeton Univ. Press, 1994.
[35] Lanotte, R., A. Maggiolo-Schettini, and A. Troina, Weak Bisimulation for Probabilistic Timed Automata and Applications to Security, Proc. SEFM'03, IEEE Press, 2003, 34-43.
[36] Lavana, H., “A Universally Configurable Architecture for Taskflow-Oriented Design of a Distributed Collaborative Computing Environment”, Ph.D. thesis, Department of Electrical and Computer Engineering, North Carolina State University, 2000.
[37] Lowe, G., Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proc. TACAS'96, LNCS 1055, Springer, 1996, 147-166.
[38] Lynch, N.A., I/O Automaton Models and Proofs for Shared-Key Communi- cation Systems, Proc. CSFW'99, IEEE Press, 1999, 14-31.
[39] Lynch, N.A., Input/Output Automata: Basic, Timed, Hybrid, Probabilistic, Dynamic,..., Proc. CONCUR'03, LNCS 2761, Springer, 1996, 191-192.
[40] Lynch, N.A., and M.R. Tuttle, An Introduction to Input/Output Automata, CWI Quarterly 2, 3 (1989), 219-246. Tech. Memo MIT/LCS/TM-373, 1988.
[41] Martinelli, F., M. Petrocchi, and A. Vaccarelli, Compositional Verification of Secure Streamed Data: a Case Study with EMSS, Proc. ICTCS'03, LNCS 2841, Springer, 2003, 383-396.
[42] Nipkow, T., L.C. Paulson, and M. Wenzel, “Isabelle/HOL-A Proof Assistant for Higher-Order Logic”, LNCS 2283, Springer, 2002. For an up-to-date description, see http://isabelle.in.tum.de/.
[43] Moskowitz, I.S., and O.L. Costich, A Classical Automata Approach to Noninterference Type Problems, Proc. CSFW'92, IEEE Press, 1992, 2-8.
[44] von Oheimb, D., Interacting State Machines-A Stateful Approach to Proving Security, Proc. FASec'02, LNCS 2629, Springer, 2003, 15-32.
[45] von Oheimb, D., and V. Lotz, Formal Security Analysis with Interacting State Machines, Proc. ESORICS'02, LNCS 2502, Springer, 2002, 212-228.
[46] Perrig, A., R. Canetti, J.D. Tygar, and D.X. Song, Efficient Authentication and Signing of Multicast Streams over Lossy Channels, Proc. S&P'00, IEEE Press, 2000, 56-73.
[47] Schneider, F.B., Enforceable Security Policies, ACM Transactions on Information and System Security 3, 1 (2000), 30-50.
[48] Segala, R., A Compositional Trace-Based Semantics for Proc. CONCUR'95, LNCS 962, Springer, 1995, 234-248.
[49] Tuttle, M.R., “Hierarchical Correctness Proofs for Distributed Algorithms”, Master's thesis, Dept. of Electrical Engineering and Computer Science, MIT, 1987. Tech. Rep. MIT/LCS/TR387, 1987.
[50] The TA webpage: http://fmt.isti.cnr.it/ mtbeek/TA.html. The TA bibliography: http://liinwww.ira.uka.de/bibliography/Theory/TA.html.
Metrics
Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:91251,
title = {Team automata for security - a survey},
author = {Ter Beek Mh and Lenzini G and Petrocchi M},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2004.11.044},
booktitle = {Electronic Notes in Theoretical Computer Science ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. London, 30 August 2004},
year = {2005}
}CNR authorsLaboratories
0000-0002-2930-6367