Team automata for security: A survey
---
paper_title: Team Automata for Security Analysis of Multicast/Broadcast Communication

paper_content:

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.
---
paper_title: Synchronizations in Team Automata for Groupware Systems

paper_content:

Team automata have been proposed in Ellis (1997) as a formal framework for modeling both the conceptual and the architectural level of groupware systems. Here we define team automata in a mathematically precise way in terms of component automata which synchronize on certain executions of actions. At the conceptual level, our model serves as a formal framework in which basic groupware notions can be rigorously defined and studied. At the architectural level, team automata can be used as building blocks in the design of groupware systems.
---
paper_title: Interacting state machines: A stateful approach to proving security

paper_content:

We introduce Interacting State Machines (ISMs), a general formalism for abstract modeling and verification of reactive systems. We motivate and explain the concept of ISMs and describe their graphical representation with the CASE tool AutoFocus. The semantics of ISMs is defined using Higher-Order Logic within the theorem prover Isabelle. ISMs can be seen as high-level variants of Input/Output Automata, therefore we give also a semantic translation from ISMs to IOAs. By the benchmark example of Lowe's fix of the Needham-Schroeder protocol we demonstrate the strengths of the ISM approach to express and prove security properties in a both elegant and machine-checked way.
---
paper_title: Role based specification and security analysis of cryptographic protocols using asynchronous product automata

paper_content:

Cryptographic protocols are formally specified as a system of protocol agents using asynchronous product automata (APA). APA are a universal and very flexible operational description concept for communicating automata. Their specification, analysis and verification is supported by the SH-verification tool (SHVT). The local state of each agent is structured in several components describing its knowledge of keys, its "view" of the protocol and the goals to be reached within the protocol. Communication is modeled by adding messages to and removing them from a shared state component network. Cryptography is modeled by symbolic functions with certain properties. In addition to the regular protocol agents an intruder is specified, which has no access to the agents' local states but to the network. The intruder may intercept messages and create new ones based on his initial knowledge and on what he can extract from intercepted messages. Violations of the security goals can be found by state space analysis performed by the SHVT. The method is demonstrated using the symmetric Needham-Schroeder protocol, and an attack is presented that does not involve compromised session keys. Our approach defers from others in that protocol specifications do not use implicit assumptions, thus protocol security does not depend on whether some implicit assumptions made are reasonable for a particular environment. Therefore, our protocol specifications explicitly provide relevant information for secure implementations.
---
paper_title: Team Automata for Spatial Access Control

paper_content:

Team automata provide a framework for capturing notions like coordination, collaboration, and cooperation in distributed systems. They consist of an abstract specification of components of a system and allow one to describe different Interconnection mechanisms based upon the concept of "shared actions" This document considers access control mechanisms in the context of the team automata model. It demonstrates the model usage and utility for capturing information security and protection structures, and critical coordinations between these structures. On the basis of a spatial access metaphor, various known access control strategies are given a rigorous formal description in terms of synchronizations in team automata.
---
paper_title: A Uniform Approach for the Definition of Security Properties

paper_content:

We present a uniform approach for the definition and the analysis of various security properties. It is based on the general idea that a security property should be satisfied even in the presence of an hostile environment. This principle determines a family of strong properties which are resistant to every external attack, but are quite impractical to check. For this reason, we find some general conditions that permit to check a property only against a "most powerful" intruder. We show that the results of our theory can be easily applied to a number of existing security properties that can be rephrased in our setting. This shows the generality of the approach and permits to find some interesting relations among properties which have been proposed for different security issues.
---
paper_title: Efficient authentication and signing of multicast streams over lossy channels

paper_content:

Multicast stream authentication and signing is an important and challenging problem. Applications include the continuous authentication of radio and TV Internet broadcasts, and authenticated data distribution by satellite. The main challenges are fourfold. First, authenticity must be guaranteed even when only the sender of the data is trusted. Second, the scheme needs to scale to potentially millions of receivers. Third, streamed media distribution can have high packet loss. Finally the system needs to be efficient to support fast packet rates. We propose two efficient schemes, TESLA and EMSS, for secure lossy multicast streams. TESLA (Timed Efficient Stream Loss-tolerant Authentication), offers sender authentication, strong loss robustness, high scalability and minimal overhead at the cost of loose initial time synchronization and slightly delayed authentication. EMSS (Efficient Multi-chained Stream Signature), provides nonrepudiation of origin, high loss resistance, and low overhead, at the cost of slightly delayed verification.
---
paper_title: Formal Security Analysis with Interacting State Machines

paper_content:

We introduce the ISM approach, a framework for modeling and verifying reactive systems in a formal, even machine-checked, way. The framework has been developed for applications in security analysis. It is based on the notion of Interacting State Machines (ISMs), sort of high-level Input/Output Automata. System models can be defined and presented graphically using the AutoFocus tool. They may be type-checked and translated to a representation within the theorem prover Isabelle or defined directly as Isabelle theories. The theorem prover may be used to perform any kind of syntactic and semantic checks, in particular semi-automatic verification. We demonstrate that the framework can be fruitfully applied for formal system analysis by two classical application examples: the LKW model of the Infineon SLE66 SmartCard chip and Lowe's fix of the Needham-Schroeder Public-Key Protocol.
---
paper_title: New Directions in Cryptography

paper_content:

Two kinds of contemporary developments in cryptography are examined. Widening applications of teleprocessing have given rise to a need for new types of cryptographic systems, which minimize the need for secure key distribution channels and supply the equivalent of a written signature. This paper suggests ways to solve these currently open problems. It also discusses how the theories of communication and computation are beginning to provide the tools to solve cryptographic problems of long standing.
---
paper_title: Enforceable security policies

paper_content:

A precise characterization is given for the class of security policies that can be enforced using mechanisms that work by monitoring system execution, and a class of automata is introduced for specifying those security policies. Techniques to enforce security policies specified by such automata are also discussed. READERS NOTE: A substantially revised version of this document is available at http://cs-tr.cs.cornell.edu:80/Dienst/UI/1.0/Display/ncstrl.cornell/TR99-1759
---
paper_title: I/O automaton models and proofs for shared-key communication systems

paper_content:

The combination of two security protocols, a simple shared-key communication protocol and the Diffie-Hellman key distribution protocol, is modeled formally and proved correct. The modeling is based on the I/O automaton model for distributed algorithms, and the proofs are based on invariant assertions, simulation relations, and compositional reasoning. Arguments about the cryptosystems are handled separately from arguments about the protocols.
---
paper_title: Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR

paper_content:

In this paper we analyse the well known Needham-Schroeder Public-Key Protocol using FDR, a refinement checker for CSP. We use FDR to discover an attack upon the protocol, which allows an intruder to impersonate another agent. We adapt the protocol, and then use FDR to show that the new protocol is secure, at least for a small system. Finally we prove a result which tells us that if this small system is secure, then so is a system of arbitrary size.
---
paper_title: Weak bisimulation for probabilistic timed automata and applications to security

paper_content:

We are interested in describing timed systems that exhibit probabilistic behaviors. To this purpose, we define a model of probabilistic timed automata and give a concept of weak bisimulation together with an algorithm to decide it. We use this model for describing and analyzing a probabilistic non-repudiation protocol in a timed setting.
---
paper_title: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach

paper_content:

Preface Introduction 2 Boolean Algebra 3 L-matrix 4 L-language 5 String Acceptors 6 [omega]-theory: L-automaton/L-process 7 The Selection/Resolution Model 8 Reduction of Verification 9 Structural Induction 10 Binary Decision Diagrams Appendices Bibliography Glossary Index
---
paper_title: Team automata : a formal approach to the modeling of collaboration between system components

paper_content:

This thesis studies formal aspects of team automata, a mathematical framework introduced in 1997 by C.A. Ellis to model components of groupware systems and their interconnections. ::: We focus on the flexibility that team automata offer when modeling collaboration between system components
---
paper_title: Hierarchical correctness proofs for distributed algorithms

paper_content:

This thesis introduces a new model for distributed computation in asynchronous networks, the input-output automaton. This simple, powerful model captures in a novel way the game-theoretical interaction between a system and its environment, and allows fundamental properties of distributed computation such as fair computation to be naturally expressed. Furthermore, this model can be used to construct modular, hierarchical correctness proofs of distributed algorithms. This thesis defines the input-output automaton model, and presents an interesting example of how this model can be used to construct such proofs.
---
paper_title: An access control framework for multi-user collaborative environments

paper_content:

A vital component of any application or environment is security, and yet this is often one of the lower priorities, losing out to performance and functionality issues, if it is considered at all. This paper considers a spatial approach to enabling, understanding and managing access control that is generally applicable across a range of collaborative environments and applications. Access control is governed according to the space within which subjects and objects reside, and the ability to traverse space to get close to an object. We present a framework that enables the SPACE access model [4], previously presented as an access model solely for collaborative virtual environments, to be applied across a number of collaborative systems. This framework is exemplified through mappings of the model to 3D and 2D collaborative environments, namely Spline [1], TeamRooms [19] and Orbit [16]. One particularly interesting feature of the model is the way in which it handles group access by considering how group credentials are determined. These credentials are presented to the model in the usual manner. We conclude by presenting some limitations of our approach, and workarounds.
---
paper_title: Team Automata for Spatial Access Control

paper_content:

Team automata provide a framework for capturing notions like coordination, collaboration, and cooperation in distributed systems. They consist of an abstract specification of components of a system and allow one to describe different Interconnection mechanisms based upon the concept of "shared actions" This document considers access control mechanisms in the context of the team automata model. It demonstrates the model usage and utility for capturing information security and protection structures, and critical coordinations between these structures. On the basis of a spatial access metaphor, various known access control strategies are given a rigorous formal description in terms of synchronizations in team automata.
---
paper_title: Team Automata for Security Analysis of Multicast/Broadcast Communication

paper_content:

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.
---
paper_title: Efficient authentication and signing of multicast streams over lossy channels

paper_content:

Multicast stream authentication and signing is an important and challenging problem. Applications include the continuous authentication of radio and TV Internet broadcasts, and authenticated data distribution by satellite. The main challenges are fourfold. First, authenticity must be guaranteed even when only the sender of the data is trusted. Second, the scheme needs to scale to potentially millions of receivers. Third, streamed media distribution can have high packet loss. Finally the system needs to be efficient to support fast packet rates. We propose two efficient schemes, TESLA and EMSS, for secure lossy multicast streams. TESLA (Timed Efficient Stream Loss-tolerant Authentication), offers sender authentication, strong loss robustness, high scalability and minimal overhead at the cost of loose initial time synchronization and slightly delayed authentication. EMSS (Efficient Multi-chained Stream Signature), provides nonrepudiation of origin, high loss resistance, and low overhead, at the cost of slightly delayed verification.
---
paper_title: Compositional Verification of Secure Streamed Data: A Case Study with EMSS

paper_content:

We consider an instance of the EMSS protocol proposed in [19], authenticating streamed data in the presence of packet loss. We formally prove the integrity property of the instance by applying a compositional proof rule that allows us to check a specification with an arbitrary number of parallel processes. We argue that our approach may be applied to a wider class of stream signature protocols.
---
paper_title: Secrecy in Security Protocols as Non Interference

paper_content:

Abstract Non Interference [8] has been proposed for modelling and analysing information flow in systems. In [4,7] we have indeed shown that the Non Interference property called NDC can be applied also in the area of network security, for the analysis of typical cryptographic protocol properties (e.g., authentication, non-repudiation). In this paper we extend the results of [4,7] by showing that NDC can be also easily adapted to detect secrecy attacks over networks.
---
paper_title: A Uniform Approach for the Definition of Security Properties

paper_content:

We present a uniform approach for the definition and the analysis of various security properties. It is based on the general idea that a security property should be satisfied even in the presence of an hostile environment. This principle determines a family of strong properties which are resistant to every external attack, but are quite impractical to check. For this reason, we find some general conditions that permit to check a property only against a "most powerful" intruder. We show that the results of our theory can be easily applied to a number of existing security properties that can be rephrased in our setting. This shows the generality of the approach and permits to find some interesting relations among properties which have been proposed for different security issues.
---
paper_title: The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties

paper_content:

The Compositional Security Checker (CoSeC for short) is a semantic-based tool for the automatic verification of some compositional information flow properties. The specifications given as inputs to CoSeC are terms of the Security Process Algebra, a language suited for the specification of concurrent systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by CoSeC are some of those classified in (Focardi and Gorrieri, 1994). They are derived from some classic notions, e.g., noninterference. The tool is based on the same architecture as the Concurrency Workbench, from which some modules have been imported unchanged. The usefulness of the tool is tested with the significant case-study of an access-monitor, presented in several versions in order to illustrate the relative merits of the various information flow properties that CoSeC can check. Finally, we present an application in the area of network security: we show that the theory (and the tool) can be reasonably applied also for singling out security flaws in a simple, yet paradigmatic, communication protocol.
---
paper_title: On the security of public key protocols

paper_content:

Recently the use of public key encryption to provide secure network communication has received considerable attention. Such public key systems are usually effective against passive eavesdroppers, who merely tap the lines and try to decipher the message. It has been pointed out, however, that an improperly designed protocol could be vulnerable to an active saboteur, one who may impersonate another user or alter the message being transmitted. Several models are formulated in which the security of protocols can be discussed precisely. Algorithms and characterizations that can be used to determine protocol security in these models are given.
---
paper_title: A Classification of Security Properties for Process Algebras

paper_content:

Several information flow security definitions, proposed in the literature, are generalized and adapted to the model of labelled transition systems. This very general model has been widely used as a semantic domain for many process algebras, e.g. CCS. As a by-product, we provide a process algebra similar to CCS with a set of security notions, hence relating these two areas of concurrency research. A classification of these generalized security definitions is presented, taking into account also the additional property of input totality, which can influence this taxonomy. We also show that some of these security properties are composable w.r.t. the operators of parallelism and action restriction.
---
paper_title: Compositional Verification of Secure Streamed Data: A Case Study with EMSS

paper_content:

We consider an instance of the EMSS protocol proposed in [19], authenticating streamed data in the presence of packet loss. We formally prove the integrity property of the instance by applying a compositional proof rule that allows us to check a specification with an arbitrary number of parallel processes. We argue that our approach may be applied to a wider class of stream signature protocols.
---
paper_title: Team Automata for Security Analysis of Multicast/Broadcast Communication

paper_content:

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.
---
paper_title: Synchronizations in Team Automata for Groupware Systems

paper_content:

Team automata have been proposed in Ellis (1997) as a formal framework for modeling both the conceptual and the architectural level of groupware systems. Here we define team automata in a mathematically precise way in terms of component automata which synchronize on certain executions of actions. At the conceptual level, our model serves as a formal framework in which basic groupware notions can be rigorously defined and studied. At the architectural level, team automata can be used as building blocks in the design of groupware systems.
---
paper_title: A universally configurable architecture for taskflow-oriented design of a distributed collaborative computing environment

paper_content:

The major goal of this thesis is to create a powerful distributed computing environment and render it collaborative. A distributed computing environment supports four structures that create a program as a hierarchy of tasks: (1) task sequencing, (2) decisions, allowing data to control the task sequence, (3) iterations, repeating the same task sequence multiple times, (4) encapsulation, replacing a group of tasks with a name that denotes the group. In addition, the environment is rendered asynchronously collaborative by (1) ownership and locking of data, (2) ownership and authorized execution of tasks, and synchronously collaborative by (1) negotiated sharing of task sequencing, (2) coordinated execution of the entire sequence of tasks. ::: The distributed computing environment is implemented by way of a user configurable universal client (OmniFlow). The key to user configurability of the client is the simplicity of the underlying taskflow model that relies on user-defined compositions of two component types only: a blackbox component and a whitebox component, each encapsulated with an autonomous FSMD, (finite-state-machine with a datapath), with the blackbox/whitebox component representing an extension of the datapath itself. A task instance layer of such a component is formed by always accessing the encapsulated layer through a ControlJoin and ControlFork primitive. The interconnection of such task instances forms a taskflow or a whitebox component. A taskflow is an intersection of a task graph and data graph where the task graph is a directed acyclic graph, with two distinguished vertices, a source and a sink, where the source represents the first task (BeginFork), and the sink represents the last task (EndJoin). The task graph is thus a polar DAG of interacting asynchronous FSMDs with built-in synchronizing primitives that can be executed concurrently and readily synchronized, just as would any DAG of well-designed and well-matched hardware components. Encapsulated tasks and task instances are specified using XML schema and a collaborative distributed task mark-up language (cdtML). ::: We propose a new approach, based on a hybrid architecture, to render any single-user Tcl application collaborative. This approach consists of a centralized synchronous group server (SGS) and a distributed synchronous group client (SGC), both are written in Tcl. (Abstract shortened by UMI.)
---
paper_title: Team Automata for Spatial Access Control

paper_content:

Team automata provide a framework for capturing notions like coordination, collaboration, and cooperation in distributed systems. They consist of an abstract specification of components of a system and allow one to describe different Interconnection mechanisms based upon the concept of "shared actions" This document considers access control mechanisms in the context of the team automata model. It demonstrates the model usage and utility for capturing information security and protection structures, and critical coordinations between these structures. On the basis of a spatial access metaphor, various known access control strategies are given a rigorous formal description in terms of synchronizations in team automata.
---
paper_title: Input/Output Automata: Basic, Timed, Hybrid, Probabilistic, Dynamic,...

paper_content:

The term Input/Output Automata refers to a family of system modeling frameworks based on interacting infinite-state machines. The models come in several flavors, based on which features (fairness, time, continuous behavior, probability, etc.) they can express. In each of these frameworks, automata can be composed in parallel to form more complex automata, and automata can be related using levels of abstraction. Properties of automata can be proved by hand or with the assistance of theorem-proving programs.
---
paper_title: The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems

paper_content:

The new pale pink colored miniature rose with yellow tones, excellent hybrid tea-like exhibition form and excellent substance.
---
paper_title: A theory of timed automata

paper_content:

Alur, R. and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183-235. We propose timed (j&e) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Biichi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (II i-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.
---
paper_title: Weak bisimulation for probabilistic timed automata and applications to security

paper_content:

We are interested in describing timed systems that exhibit probabilistic behaviors. To this purpose, we define a model of probabilistic timed automata and give a concept of weak bisimulation together with an algorithm to decide it. We use this model for describing and analyzing a probabilistic non-repudiation protocol in a timed setting.
---

Title: Team Automata for Security: A Survey

Section 1: Introduction
Description 1: This section introduces Team Automata (TA) and their origin, context of use, and a broad overview of their application in the field of security.

Section 2: Team Automata
Description 2: This section informally describes the main characteristics of TA and how to use them, with references for more technical details.

Section 3: Access Control Policies
Description 3: This section discusses how TA can be used to model and verify various access control policies, including immediate versus delayed revocation and meta access control.

Section 4: Multicast/Broadcast Communication Protocols
Description 4: This section covers how TA can model secure multicast and broadcast communication protocols, including handling of packet loss.

Section 5: Towards a TA Framework for the Analysis of Security Properties
Description 5: This section outlines the development of an insecure communication scenario using TA and the formulation of the Generalized Non-Deducibility on Compositions (GNDC) schema to verify security properties.

Section 6: Conclusions and Future Work
Description 6: This section summarizes the survey findings, noting the versatility of TA in different fields of security, and proposes future research directions including automation of specification and verification, and extending TA with time and probability.

Section 7: Acknowledgements
Description 7: This section acknowledges the support and funding received for the research work presented in the paper.