2004
Journal article
Restricted
On competence in CD grammar systems
Ter Beek M, Csuhajvarju E, Holzer M, Vaszil G
We investigate the generative power of cooperating distributed grammar systems (CDGSs), if the cooperation protocol is based on the level of competence on the underlying sentential form. A component is said to be =k-competent (=k-competent, resp.) on a sentential form if it is able to rewrite exactly k (at most k, at least k, resp.) different nonterminals appearing in that string. In most cases CDGSs working according to the above described cooperation strategy turn out to give new characterizations of the language families based on random context conditions, namely random context (context-free) languages and the biologically motivated family of languages generated by ET0L systems with random context. Thus, the results presented in this paper can shed new light on some longstanding open problems in the theory of regulated rewriting.
Ter Beek M, Csuhajvarju E, Holzer M, Vaszil G
We investigate the generative power of cooperating distributed grammar systems (CDGSs), if the cooperation protocol is based on the level of competence on the underlying sentential form. A component is said to be =k-competent (=k-competent, resp.) on a sentential form if it is able to rewrite exactly k (at most k, at least k, resp.) different nonterminals appearing in that string. In most cases CDGSs working according to the above described cooperation strategy turn out to give new characterizations of the language families based on random context conditions, namely random context (context-free) languages and the biologically motivated family of languages generated by ET0L systems with random context. Thus, the results presented in this paper can shed new light on some longstanding open problems in the theory of regulated rewriting.
See at:
CNR IRIS 
| CNR IRIS | www.springerlink.com
2004
Journal article
Open Access
Teams of Pushdown Automata
Ter Beek Mh, Csuhajvarju E, Mitrana V
We introduce team pushdown automata (PDAs) as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team PDAs are obtained by augmenting distributed PDAs with the notion of team cooperation or, alternatively, by augmenting team automata with pushdown memory. In a team PDA, several PDAs work as a team on the input word placed on a common one-way input tape. At any moment in time one team of PDAs, each with the same symbol on top of its stack, is active: each PDA in the active team replaces the topmost symbol of its stack and changes state, while the current input symbol is read from the input tape by a common reading head. The teams are formed according to the team cooperation strategy of the team PDA and may vary from one moment to the other. Based on the notion of competence, we introduce a variety of team cooperation strategies. If all stacks are empty when the input word has been completely read, then this word is part of the language accepted by the team PDA. Here we focus on the accepting capacity of team PDA.Source: INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, vol. 81 (issue 2), pp. 141-156
DOI: 10.1080/00207160310001650099
DOI: 10.1007/978-3-540-39866-0_32
Metrics:
Ter Beek Mh, Csuhajvarju E, Mitrana V
We introduce team pushdown automata (PDAs) as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team PDAs are obtained by augmenting distributed PDAs with the notion of team cooperation or, alternatively, by augmenting team automata with pushdown memory. In a team PDA, several PDAs work as a team on the input word placed on a common one-way input tape. At any moment in time one team of PDAs, each with the same symbol on top of its stack, is active: each PDA in the active team replaces the topmost symbol of its stack and changes state, while the current input symbol is read from the input tape by a common reading head. The teams are formed according to the team cooperation strategy of the team PDA and may vary from one moment to the other. Based on the notion of competence, we introduce a variety of team cooperation strategies. If all stacks are empty when the input word has been completely read, then this word is part of the language accepted by the team PDA. Here we focus on the accepting capacity of team PDA.Source: INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, vol. 81 (issue 2), pp. 141-156
DOI: 10.1080/00207160310001650099
DOI: 10.1007/978-3-540-39866-0_32
Metrics:
See at:
International Journal of Computer Mathematics 
| doi.org | International Journal of Computer Mathematics | CNR IRIS | CNR IRIS | www.scopus.com | www.tandfonline.com
2005
Journal article
Open Access
Modularity for teams of I/O automata
Ter Beek M. H., Kleijn J.
NoneSource: INFORMATION PROCESSING LETTERS, vol. 95 (issue 5), pp. 487-495
DOI: 10.1016/j.ipl.2005.05.012
Metrics:
Ter Beek M. H., Kleijn J.
NoneSource: INFORMATION PROCESSING LETTERS, vol. 95 (issue 5), pp. 487-495
DOI: 10.1016/j.ipl.2005.05.012
Metrics:
See at:
Information Processing Letters | Information Processing Letters | CNR IRIS | CNR IRIS | www.sciencedirect.com
2005
Journal article
Open Access
Synchronized shuffles
Ter Beek M. H., Martín-Vide C., Mitrana V.
We extend the basic shuffle on words and languages, a well-known operation in theoretical computer science, by introducing three synchronized shuffles. These synchronized shuffles have some relevance to molecular biology since they may be viewed as the formal representations of various forms of gene linkage during genome shuffling. More precisely, each synchronized shuffle preserves the genetic backbone of the organisms, as well as the linked genes, by requiring the synchronization of some predefined genes while all other genes are arbitrarily shuffled. As for their mathematical properties, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied here. Finally, based on this result, we present an algorithm for deciding whether a given regular language is synchronized shuffle closed.Source: THEORETICAL COMPUTER SCIENCE, vol. 341 (issue 1-3), pp. 263-275
DOI: 10.1016/j.tcs.2005.04.007
Metrics:
Ter Beek M. H., Martín-Vide C., Mitrana V.
We extend the basic shuffle on words and languages, a well-known operation in theoretical computer science, by introducing three synchronized shuffles. These synchronized shuffles have some relevance to molecular biology since they may be viewed as the formal representations of various forms of gene linkage during genome shuffling. More precisely, each synchronized shuffle preserves the genetic backbone of the organisms, as well as the linked genes, by requiring the synchronization of some predefined genes while all other genes are arbitrarily shuffled. As for their mathematical properties, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied here. Finally, based on this result, we present an algorithm for deciding whether a given regular language is synchronized shuffle closed.Source: THEORETICAL COMPUTER SCIENCE, vol. 341 (issue 1-3), pp. 263-275
DOI: 10.1016/j.tcs.2005.04.007
Metrics:
See at:
Theoretical Computer Science | CNR IRIS | CNR IRIS | www.sciencedirect.com
2007
Journal article
Open Access
Infinite unfair shuffles and associativity
Ter Beek M. H., Kleijn J.
We consider a general shuffling operation for finite and infinite words which is not necessarily fair. This means that it may be the case that in a shuffle of two words, from some point onwards, one of these words prevails ad infinitum even though the other word still has letters to contribute. Prefixes and limits of shuffles are investigated, leading to a characterization of general shuffles in terms of shuffles of finite words, a result which does not hold for fair shuffles. Associativity of shuffling is an immediate corollary.Source: THEORETICAL COMPUTER SCIENCE, vol. 380 (issue 3), pp. 401-410
DOI: 10.1016/j.tcs.2007.03.030
Metrics:
Ter Beek M. H., Kleijn J.
We consider a general shuffling operation for finite and infinite words which is not necessarily fair. This means that it may be the case that in a shuffle of two words, from some point onwards, one of these words prevails ad infinitum even though the other word still has letters to contribute. Prefixes and limits of shuffles are investigated, leading to a characterization of general shuffles in terms of shuffles of finite words, a result which does not hold for fair shuffles. Associativity of shuffling is an immediate corollary.Source: THEORETICAL COMPUTER SCIENCE, vol. 380 (issue 3), pp. 401-410
DOI: 10.1016/j.tcs.2007.03.030
Metrics:
See at:
Theoretical Computer Science | CNR IRIS | CNR IRIS | www.sciencedirect.com
2007
Journal article
Restricted
On Competence in CD Grammar Systems with Parallel Rewriting
Ter Beek M H, Csuhajvarju E, Holzer M, Vaszil G
We continue our investigation of the generative power of cooperating distributed grammar systems (CDGSs), using the previously introduced <=k-, =k-, and >=k-competence-based cooperation strategies and context-free components that rewrite the sentential form in a parallel manner. This leads to new characterizations of the languages generated by (random context) ET0L systems and recurrent programmed grammars.Source: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, vol. 18 (issue 6), pp. 1425-1439
DOI: 10.1142/s0129054107005467
Metrics:
Ter Beek M H, Csuhajvarju E, Holzer M, Vaszil G
We continue our investigation of the generative power of cooperating distributed grammar systems (CDGSs), using the previously introduced <=k-, =k-, and >=k-competence-based cooperation strategies and context-free components that rewrite the sentential form in a parallel manner. This leads to new characterizations of the languages generated by (random context) ET0L systems and recurrent programmed grammars.Source: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, vol. 18 (issue 6), pp. 1425-1439
DOI: 10.1142/s0129054107005467
Metrics:
See at:
International Journal of Foundations of Computer Science | CNR IRIS | CNR IRIS | www.worldscinet.com
2003
Conference article
Restricted
Team automata satisfying compositionality
Ter Beek M, Kleijn J
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation of the conditions under which team automata satisfy compositionality, we study their computations and behaviour in relation to those of their constituting component automata. We show that the construction of team automata according to certain natural types of synchronization guarantees compositionality.DOI: 10.1007/978-3-540-45236-2_22
Metrics:
Ter Beek M, Kleijn J
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation of the conditions under which team automata satisfy compositionality, we study their computations and behaviour in relation to those of their constituting component automata. We show that the construction of team automata according to certain natural types of synchronization guarantees compositionality.DOI: 10.1007/978-3-540-45236-2_22
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
2003
Conference article
Open Access
Teams of Pushdown Automata
Ter Beek M H, Csuhajvarju E, Mitrana V
We introduce team pushdown automata as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team pushdown automata are obtained by augmenting distributed pushdown automata with the notion of team cooperation or - alternatively - by augmenting team automata with pushdown memory. Here we study their accepting capacity.DOI: 10.1007/978-3-540-39866-0_32
DOI: 10.1080/00207160310001650099
Metrics:
Ter Beek M H, Csuhajvarju E, Mitrana V
We introduce team pushdown automata as a theoretical framework capable of modelling various communication and cooperation strategies in complex, distributed systems. Team pushdown automata are obtained by augmenting distributed pushdown automata with the notion of team cooperation or - alternatively - by augmenting team automata with pushdown memory. Here we study their accepting capacity.DOI: 10.1007/978-3-540-39866-0_32
DOI: 10.1080/00207160310001650099
Metrics:
See at:
International Journal of Computer Mathematics | doi.org | International Journal of Computer Mathematics | CNR IRIS | CNR IRIS | www.scopus.com
2009
Journal article
Restricted
Associativity of Infinite Synchronized Shuffles and Team Automata
Ter Beek Mh, Kleijn J
Motivated by different ways to obtain team automata from synchronizing component automata, we consider various definitions of synchronized shuffles of words. A shuffle of two words is an interleaving of their symbol occurrences which preserves the original order of these occurrences within each of the two words. In a synchronized shuffle, however, also two occurrences of one symbol, each from a different word, may be identified as a single occurrence. In case at least one of the words involved is infinite, a (synchronized) shuffle can also be unfair in the sense that an infinite word may prevail from some point onwards even when the other word still has occurrences to contribute to the shuffle. We prove that for the synchronized shuffle operations under consideration, every (fair or unfair) synchronized shuffle can be obtained as a limit of synchronized shuffles of the finite prefixes of the words involved. In addition, it is shown that with the exception of one, all synchronized shuffle operations that we consider satisfy a natural notion of associativity, also in case of unfairness. Finally, using these results, some compositionality results for team automata are established.Source: FUNDAMENTA INFORMATICAE, vol. 91 (issue 3-4), pp. 437-461
DOI: 10.3233/fi-2009-0051
Metrics:
Ter Beek Mh, Kleijn J
Motivated by different ways to obtain team automata from synchronizing component automata, we consider various definitions of synchronized shuffles of words. A shuffle of two words is an interleaving of their symbol occurrences which preserves the original order of these occurrences within each of the two words. In a synchronized shuffle, however, also two occurrences of one symbol, each from a different word, may be identified as a single occurrence. In case at least one of the words involved is infinite, a (synchronized) shuffle can also be unfair in the sense that an infinite word may prevail from some point onwards even when the other word still has occurrences to contribute to the shuffle. We prove that for the synchronized shuffle operations under consideration, every (fair or unfair) synchronized shuffle can be obtained as a limit of synchronized shuffles of the finite prefixes of the words involved. In addition, it is shown that with the exception of one, all synchronized shuffle operations that we consider satisfy a natural notion of associativity, also in case of unfairness. Finally, using these results, some compositionality results for team automata are established.Source: FUNDAMENTA INFORMATICAE, vol. 91 (issue 3-4), pp. 437-461
DOI: 10.3233/fi-2009-0051
Metrics:
See at:
Fundamenta Informaticae | CNR IRIS | iospress.metapress.com | CNR IRIS
2009
Book
Restricted
Preface - Architecting Dependable Systems VI
De Lemos R, Fabre J, Gacek C, Gadducci F, Ter Beek M
As software systems become increasingly ubiquitous, issues of dependability become ever more crucial. Given that solutions to these issues must be considered from the very beginning of the design process, it is reasonable that dependability and security are addressed at the architectural level. This book has originated from an effort to bring together the research communities of software architectures, dependability and security. This state-of-the-art survey contains expanded and peer-reviewed papers based on the carefully selected contributions to two workshops: the Workshop on Architecting Dependable Systems (WADS 2008), organized at the 2008 International Conference on Dependable Systems and Networks (DSN 2008), held in Anchorage, Alaska, USA, in June 2008, and the Third International Workshop on Views On Designing Complex Architectures (VODCA 2008) held in Bertinoro, Italy, in August 2008. It also contains invited papers written by recognized experts in the area. The 13 papers are organized in topical sections on dependable service-oriented architectures, fault-tolerance and system evaluation, and architecting security.DOI: 10.1007/978-3-642-10248-6
Metrics:
De Lemos R, Fabre J, Gacek C, Gadducci F, Ter Beek M
As software systems become increasingly ubiquitous, issues of dependability become ever more crucial. Given that solutions to these issues must be considered from the very beginning of the design process, it is reasonable that dependability and security are addressed at the architectural level. This book has originated from an effort to bring together the research communities of software architectures, dependability and security. This state-of-the-art survey contains expanded and peer-reviewed papers based on the carefully selected contributions to two workshops: the Workshop on Architecting Dependable Systems (WADS 2008), organized at the 2008 International Conference on Dependable Systems and Networks (DSN 2008), held in Anchorage, Alaska, USA, in June 2008, and the Third International Workshop on Views On Designing Complex Architectures (VODCA 2008) held in Bertinoro, Italy, in August 2008. It also contains invited papers written by recognized experts in the area. The 13 papers are organized in topical sections on dependable service-oriented architectures, fault-tolerance and system evaluation, and architecting security.DOI: 10.1007/978-3-642-10248-6
Metrics:
See at:
CNR IRIS | CNR IRIS | www.springerlink.com
2006
Journal article
Metadata Only Access
A team automaton scenario for the analysis of security properties in communication protocols
Ter Beek M H, Lenzini G, Petrocchi M
Formal methods are a popular means to specify and verify security properties of a variety of communication protocols. In this article we take a step towards the use of team automata for the analysis of security aspects in such protocols. To this aim, we define an insecure communication scenario for team automata that is general enough to encompass various communication protocols. We then reformulate the Generalized Non-Deducibility on Compositions schema - originally introduced in the context of process algebrae - in terms of team automata. Based on the resulting team automata framework, we subsequently develop two analysis strategies that can be used to verify security properties of communication protocols. Indeed, the paper concludes with two case studies in which we show how our framework can be used to prove integrity and secrecy in two different settings: We show how integrity is guaranteed in a team automaton model of a particular instance of the Efficient Multi-chained Stream Signature protocol, a communication protocol for signing digital streams that provides some robustness against packet loss, and we show how secrecy is preserved when a member of a multicast group leaves the group in a particular run of the complementary variable approach to the N-Root/Leaf pairwise keys protocol.
Ter Beek M H, Lenzini G, Petrocchi M
Formal methods are a popular means to specify and verify security properties of a variety of communication protocols. In this article we take a step towards the use of team automata for the analysis of security aspects in such protocols. To this aim, we define an insecure communication scenario for team automata that is general enough to encompass various communication protocols. We then reformulate the Generalized Non-Deducibility on Compositions schema - originally introduced in the context of process algebrae - in terms of team automata. Based on the resulting team automata framework, we subsequently develop two analysis strategies that can be used to verify security properties of communication protocols. Indeed, the paper concludes with two case studies in which we show how our framework can be used to prove integrity and secrecy in two different settings: We show how integrity is guaranteed in a team automaton model of a particular instance of the Efficient Multi-chained Stream Signature protocol, a communication protocol for signing digital streams that provides some robustness against packet loss, and we show how secrecy is preserved when a member of a multicast group leaves the group in a particular run of the complementary variable approach to the N-Root/Leaf pairwise keys protocol.
See at:
CNR IRIS
2005
Conference article
Open Access
Infinite Unfair Shuffles and Associativity
Ter Beek M, Kleijn J
We consider a general shuffling operation for finite and infinite words which is not necessarily fair. This means that it may be the case that in a shuffle of two words, from some point onwards, one of these words prevails ad infinitum even though the other word still has letters to contribute. Prefixes and limits of shuffles are investigated, leading to a characterization of general shuffles in terms of shuffles of finite words, a result which does not hold for fair shuffles. Associativity of shuffling is an immediate corollary.
Ter Beek M, Kleijn J
We consider a general shuffling operation for finite and infinite words which is not necessarily fair. This means that it may be the case that in a shuffle of two words, from some point onwards, one of these words prevails ad infinitum even though the other word still has letters to contribute. Prefixes and limits of shuffles are investigated, leading to a characterization of general shuffles in terms of shuffles of finite words, a result which does not hold for fair shuffles. Associativity of shuffling is an immediate corollary.
See at:
CNR IRIS | lacim.uqam.ca | ISTI Repository | CNR IRIS | CNR IRIS
2005
Conference article
Open Access
Team automata for security - a survey
Ter Beek Mh, Lenzini G, Petrocchi M
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
DOI: 10.1016/j.entcs.2004.11.044
Metrics:
Ter Beek Mh, Lenzini G, Petrocchi M
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
DOI: 10.1016/j.entcs.2004.11.044
Metrics:
See at:
Electronic Notes in Theoretical Computer Science | CNR IRIS | CNR IRIS
2008
Conference article
Open Access
A Calculus for Team Automata
Ter Beek M H, Gadducci F, Janssens D
Team automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patterns among systems, thus extending I/O automata. Furthermore, for some patterns the language recognized by a team automaton can be specified via those languages recognized by its components. We introduce a process calculus tailored over team automata. Each automaton is described by a process, such that its associated (fragment of a) labeled transition system is bisimilar to the original automaton. The mapping is moreover denotational, since the operators defined on processes are in a bijective correspondence with a chosen family of coordination patterns and that correspondence is preserved by the mapping. We thus extend to team automata a few classical results on I/O automata and their representation by process calculi. Moreover, besides providing a language for expressing team automata, we widen the family of coordination patterns for which an equational characterization of the language associated to a composite automaton can be provided. The latter result is obtained by providing a set of axioms, in ACP-style, for capturing bisimilarity in our calculus.Source: Electronic Notes in Theoretical Computer Science ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, pp. 41-55. Natal, Rio Grande do Norte, Brazil, 17-23 Settembre 2006
DOI: 10.1016/j.entcs.2007.08.022
Metrics:
Ter Beek M H, Gadducci F, Janssens D
Team automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patterns among systems, thus extending I/O automata. Furthermore, for some patterns the language recognized by a team automaton can be specified via those languages recognized by its components. We introduce a process calculus tailored over team automata. Each automaton is described by a process, such that its associated (fragment of a) labeled transition system is bisimilar to the original automaton. The mapping is moreover denotational, since the operators defined on processes are in a bijective correspondence with a chosen family of coordination patterns and that correspondence is preserved by the mapping. We thus extend to team automata a few classical results on I/O automata and their representation by process calculi. Moreover, besides providing a language for expressing team automata, we widen the family of coordination patterns for which an equational characterization of the language associated to a composite automaton can be provided. The latter result is obtained by providing a set of axioms, in ACP-style, for capturing bisimilarity in our calculus.Source: Electronic Notes in Theoretical Computer Science ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, pp. 41-55. Natal, Rio Grande do Norte, Brazil, 17-23 Settembre 2006
DOI: 10.1016/j.entcs.2007.08.022
Metrics:
See at:
Electronic Notes in Theoretical Computer Science | CNR IRIS | CNR IRIS
2006
Contribution to conference
Open Access
A calculus for team automata
Ter Beek M, Gadducci F, Janssens D
eam automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patterns among systems, thus extending I/O automata. Furthermore, for some patterns the language recognized by a team automaton can be specified via those languages recognized by its components. We introduce a process calculus tailored over team automata. Each automaton is described by a process, and such that its associated (fragment of a) labeled transition system is bisimilar to the original automaton. The mapping is furthermore denotational, since the operators defined on processes are in a bijective correspondence with a chosen family of coordination patterns and that correspondence is preserved by the mapping. We thus extend to team automata a few classical results on I/O automata and their representation by process calculi. Moreover, besides providing a language for expressing team automata, we widen the family of coordination patterns for which an equational characterization of the language associated to a composite automaton can be provided. The latter result is obtained by providing a set of axioms, in ACP-style, for capturing bisimilarity in our calculus.
Ter Beek M, Gadducci F, Janssens D
eam automata are a formalism for the component-based specification of reactive, distributed systems. Their main feature is a flexible technique for specifying coordination patterns among systems, thus extending I/O automata. Furthermore, for some patterns the language recognized by a team automaton can be specified via those languages recognized by its components. We introduce a process calculus tailored over team automata. Each automaton is described by a process, and such that its associated (fragment of a) labeled transition system is bisimilar to the original automaton. The mapping is furthermore denotational, since the operators defined on processes are in a bijective correspondence with a chosen family of coordination patterns and that correspondence is preserved by the mapping. We thus extend to team automata a few classical results on I/O automata and their representation by process calculi. Moreover, besides providing a language for expressing team automata, we widen the family of coordination patterns for which an equational characterization of the language associated to a composite automaton can be provided. The latter result is obtained by providing a set of axioms, in ACP-style, for capturing bisimilarity in our calculus.
See at:
fmt.isti.cnr.it | CNR IRIS | ISTI Repository | CNR IRIS
2007
Other
Open Access
Modelling and analysing an identity federation protocol: federated network providers scenario
Ter Beek M H, Moiso C, Petrocchi M
We continue our work on modelling and analysing security issues of an identity federation protocol for convergent networks. This protocol was proposed by Telecom Italia as a solution to allow end users access to services on the web through different access networks, without explicitly providing any credentials, while the service providers can trust the user's identity information provided by the access networks and access some user data. As an intermediate step towards a full-blown formal security analysis of this protocol, we specify one specific user scenario in the process algebra Crypto-CCS and verify its vulnerability w.r.t. a man-in-the-middle attack with the model checker PaMoChSA.
Ter Beek M H, Moiso C, Petrocchi M
We continue our work on modelling and analysing security issues of an identity federation protocol for convergent networks. This protocol was proposed by Telecom Italia as a solution to allow end users access to services on the web through different access networks, without explicitly providing any credentials, while the service providers can trust the user's identity information provided by the access networks and access some user data. As an intermediate step towards a full-blown formal security analysis of this protocol, we specify one specific user scenario in the process algebra Crypto-CCS and verify its vulnerability w.r.t. a man-in-the-middle attack with the model checker PaMoChSA.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2007
Book
Restricted
Preface to Second international workshop on views on designing complex architectures
Ter Beek Mh, F Gadducci
The second international workshop on Views On Designing Complex Architectures (VODCA 2006) was held in Bertinoro, Italy, on the 16th and 17th of September 2006, as a satellite event to the sixth international school on Foundations of Security Analysis and Design (FOSAD 2006). Security and management of information are key issues in informatics, and they have been for several years now among its fastest developing fields. Such a synergetic combination calls for a continuous attention of computer science researchers to the most recent developments in the area, in order to bring forth novel ideas and insights and thus to contribute to the growth of those fields. The VODCA workshop series aims to provide a platform for young computer scientists to present their research views on all areas related to the design of complex architectures, with a special focus on the security and management of information. A total of 20 papers were submitted and after a regular refereeing process only 13 of them were selected for a presentation. In addition to the presentations of original research results, the programme included 2 invited lectures. We believe that the most important result of any workshop should be the fostering and establishing of collaborations, as well as the sharing of techniques and their cross-fertilisation. These words sound truer for a workshop like VODCA: We hope that the meeting has helped its participants to focus on original 'views on the design of complex architectures,' especially as far as the security and management of information issues are concerned.
Ter Beek Mh, F Gadducci
The second international workshop on Views On Designing Complex Architectures (VODCA 2006) was held in Bertinoro, Italy, on the 16th and 17th of September 2006, as a satellite event to the sixth international school on Foundations of Security Analysis and Design (FOSAD 2006). Security and management of information are key issues in informatics, and they have been for several years now among its fastest developing fields. Such a synergetic combination calls for a continuous attention of computer science researchers to the most recent developments in the area, in order to bring forth novel ideas and insights and thus to contribute to the growth of those fields. The VODCA workshop series aims to provide a platform for young computer scientists to present their research views on all areas related to the design of complex architectures, with a special focus on the security and management of information. A total of 20 papers were submitted and after a regular refereeing process only 13 of them were selected for a presentation. In addition to the presentations of original research results, the programme included 2 invited lectures. We believe that the most important result of any workshop should be the fostering and establishing of collaborations, as well as the sharing of techniques and their cross-fertilisation. These words sound truer for a workshop like VODCA: We hope that the meeting has helped its participants to focus on original 'views on the design of complex architectures,' especially as far as the security and management of information issues are concerned.
See at:
CNR IRIS | CNR IRIS | www.sciencedirect.com
2003
Other
Open Access
Synchronized shuffles
Ter Beek Mh, Martinvide C, Mitrana V
We introduce and investigate three synchronized shuffle operations on words and languages. We show how such operations come into play when proving compositionality of automata-based specification models, by demonstrating their usage in the context of team automata. As far as the mathematical properties of these operations are concerned, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied in this paper. Finally, based on this result, we present an algorithm for deciding whether or not a given regular language is synchronized shuffle closed.
Ter Beek Mh, Martinvide C, Mitrana V
We introduce and investigate three synchronized shuffle operations on words and languages. We show how such operations come into play when proving compositionality of automata-based specification models, by demonstrating their usage in the context of team automata. As far as the mathematical properties of these operations are concerned, we prove that in a trio the closure under shuffle is equivalent to the closure under any of the synchronized shuffles studied in this paper. Finally, based on this result, we present an algorithm for deciding whether or not a given regular language is synchronized shuffle closed.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2003
Other
Open Access
Team automata satisfying compositionality
Ter Beek Mh, Kleijn J
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation of the conditions under which team automata satisfy compositionality, we study their computations and behaviour in relation to those of their constituting component automata. We show that the construction of team automata according to certain natural types of synchronization guarantees compositionality.
Ter Beek Mh, Kleijn J
A team automaton is said to satisfy compositionality if its behaviour can be described in terms of the behaviour of its constituting component automata. As an initial investigation of the conditions under which team automata satisfy compositionality, we study their computations and behaviour in relation to those of their constituting component automata. We show that the construction of team automata according to certain natural types of synchronization guarantees compositionality.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2003
Other
Open Access
Team automata for security analysis of multicast/broadcast communication
Ter Beek Mh, Lenzini G, Petrocchi M
We show that team automata (TA) are well suited to model secure multicast/broadcast communication with possible packet loss. This is a consequence of the natural way in which one-to-many (one-to-all) transmissions typical of multicast (broadcast) sessions can be modelled as communications between the component automata (CA) constituting a TA. To this aim, we use TA to model an instance of the EMSS multicast protocol family. In addition, we investigate a formulation of the Generalized Non-Deducibility on Compositions (GNDC) schema in terms of TA with the aim to embed TA in this well-established analysis framework. We intend to use this new setting for the formal verification of security properties for stream signature protocols.
Ter Beek Mh, Lenzini G, Petrocchi M
We show that team automata (TA) are well suited to model secure multicast/broadcast communication with possible packet loss. This is a consequence of the natural way in which one-to-many (one-to-all) transmissions typical of multicast (broadcast) sessions can be modelled as communications between the component automata (CA) constituting a TA. To this aim, we use TA to model an instance of the EMSS multicast protocol family. In addition, we investigate a formulation of the Generalized Non-Deducibility on Compositions (GNDC) schema in terms of TA with the aim to embed TA in this well-established analysis framework. We intend to use this new setting for the formal verification of security properties for stream signature protocols.
See at:
CNR IRIS | ISTI Repository | CNR IRIS