Assured Remote Execution for a device is the ability of suitably authorized parties to construct secure channels to processes executing known code running on that device. Assured remote execution requires hardware support including cryptographic primitives. Cryptographically Assured Information Flow (CAIF) is a hardware mechanism to enable Assured Remote Execution. It is akin to existing Trusted Execution Environments, but securely implements an ideal functionality for logging and confidential escrow. Symbolic protocol analysis demonstrates that Assured Remote Execution is achieved even against a strong adversary able to modify our programs and execute unauthorized programs on the device. Assured remote execution allows trustworthy remote attestation, and a core part of secure remote reprogramming.11Copyright © 2024, The MITRE Corporation. All rights reserved.

In complex networks, filters may be applied at different nodes to control how packets flow. In this paper, we study how to locate filtering functionality within a network. We show how to enforce a set of security goals while allowing maximal service subject to the security constraints. To implement our results we present a tool that given a network specification and a set of control rules automatically localizes the filters and generates configurations for all the firewalls in the network. These configurations are implemented using an extension of Mignis - an open source tool to generate firewalls from declarative, semantically explicit configurations. Our contributions include a way to specify security goals for how packets traverse the network, an algorithm to distribute filtering functionality to different nodes in the network to enforce a given set of security goals, and a proof that the results are compatible with a Mignis-based semantics for network behavior.

We view a distributed system as a graph of active locations with unidirectional channels between them, through which they pass messages. In this context, the graph structure of a system constrains the propagation of information through it. Suppose a set of channels is a cut set between an information source and a potential sink. We prove that, if there is no disclosure from the source to the cut set, then there can be no disclosure to the sink. We introduce a new formalization of partial disclosure, called blur operators, and show that the same cut property is preserved for disclosure to within a blur operator. A related compositional principle ensures limited disclosure for a class of systems that differ only beyond the cut.

Many protocols use Diffie-Hellman key agreement, combined with certified long-term values or digital signatures for authentication. These protocols aim at security goals such as key secrecy, forward secrecy, resistance to key compromise attacks, and various flavors of authentication. However, these protocols are challenging to analyze, both in computational and symbolic models. An obstacle in the symbolic model is the undecidability of unification in many theories in the signature of rings. In this paper, we develop an algebraic version of the symbolic approach, working directly within finite fields, the natural structures for the protocols. The adversary, in giving an attack on a protocol goal in a finite field, may rely on any identity in that field. He defeats the protocol if there are attacks in infinitely many finite fields. We prove that, even for this strong adversary, security goals for a wide class of protocols are decidable.

We take a model-theoretic viewpoint on security goals and how to establish them. The models are (possibly fragmentary) executions. Security goals such as authentication and confidentiality are geometric sequents, i.e. implications Φ→Ψ where Φ and Ψ are built from atomic formulas without negations, implications, or universal quantifiers. Security goals are then statements about homomorphisms, where the source is a minimal (fragmentary) model of the antecedent Φ. If every homomorphism to a non-fragmentary, complete execution factors through a model in which Ψ is satisfied, then the goal is achieved. One can validate security goals via a process of information enrichment. We call this approach enrich-by-need protocol analysis. This idea also clarifies protocol transformation. A protocol transformation preserves security goals when it preserves the form of the information enrichment process. We formalize this idea using simulation relations between labeled transition systems. These labeled transition systems formalize the analysis of the protocols, i.e. the information enrichment process, not the execution behavior of the protocols.

Distributed stream processing systems must function efficiently for data streams that fluctuate in their arrival rates and data distributions. Yet repeated and prohibitively expensive load re-allocation across machines may make these systems ineffective, potentially resulting in data loss or even system failure. To overcome this problem, we instead propose a load distribution (RLD) strategy that is robust to data fluctuations. RLD provides ϵ-optimal query performance under load fluctuations without suffering from the performance penalty caused by load migration. RLD is based on three key strategies. First, we model robust distributed stream processing as a parametric query optimization problem. The notions of robust logical and robust physical plans then are overlays of this parameter space. Second, our Early-terminated Robust Partitioning (ERP) finds a set of robust logical plans, covering the parameter space, while minimizing the number of prohibitively expensive optimizer calls with a probabilistic bound on the space coverage. Third, our OptPrune algorithm maps the space-covering logical solution to a single robust physical plan tolerant to deviations in data statistics that maximizes the parameter space coverage at runtime. Our experimental study using stock market and sensor networks streams demonstrates that our RLD methodology consistently outperforms state-of-the-art solutions in terms of efficiency and effectiveness in highly fluctuating data stream environments.

Secure initial trust establishment for multiple resource constrained devices is a fundamental issue underlying wireless networks. A number of protocols have been proposed for secure key deployment among nodes without prior shared secrets (ad hoc), however so far most of them rely on secure out-of-band (OOB) channels (e.g., audio, visual) which either only work with a small number of devices or require auxiliary hardware. In this paper, for the first time, we design a solution that enables secure initialization of a group of wireless devices, which works merely within the wireless band. Our proposed solution is based on a novel physical-layer primitive for authenticated string comparison over the insecure wireless channel, called Chorus, which simultaneously compares the equality of fixed-length authentication strings held by multiple wireless devices within constant time. The Chorus achieves a key authentication property, which prevents an adversary from tricking each device to believe that all strings are equal when they are not, which is enabled by exploiting the infeasibility of signal cancellation and unidirectional error detection codes. Chorus can be employed as a foundation to provide in-band group message authentication (GMA) and group authenticated key agreement (GAKA), that does not require any prior shared secret. Specifically, we design two GAKA protocols based on Chorus and formally prove their security. The most appealing features of our proposed protocols include: minimal hardware requirement (a common radio interface and a button), minimal user effort (pressing a button on each device on average), nearly constant running time, thus they are scalable to a large group of constrained wireless devices. Through extensive analysis and experimental evaluation, we show the security and robustness of Chorus under a realistic attack model, and demonstrate the high scalability of our GAKA protocols.

The issue took inspiration from the conference on Principles of Security and Trust (POST

The body area network (BAN) is a key enabling technology in e-healthcare. An important security issue is to establish initial trust relationships among the BAN devices before they are actually deployed and generate necessary shared secret keys to protect the subsequent wireless communications. Due to the ad hoc nature of the BAN and the extreme resource constraints of sensor devices, providing secure as well as efficient and user-friendly trust initialization is a challenging task. Traditional solutions for wireless sensor networks mostly depend on key predistribution, which is unsuitable for a BAN in many ways. In this article, we propose group device pairing (GDP), a user-aided multi-party authenticated key agreement protocol. Through GDP, a group of sensor devices that have no pre-shared secrets establish initial trust by generating various shared secret keys out of an unauthenticated channel. Devices authenticate themselves to each other with the aid of a human user who performs visual verifications. The GDP supports fast batch deployment, addition and revocation of sensor devices, does not rely on any additional hardware device, and is mostly based on symmetric key cryptography. We formally prove the security of the proposed protocols, and we implement GDP on a sensor network testbed and report performance evaluation results.

Cryptographic protocols are useful for trust engineering in Web transactions. The Cryptographic Protocol Programming Language (CPPL) provides a model wherein trust management annotations are attached to protocol actions, and are used to constrain the behavior of a protocol participant to be compatible with its own trust policy.

In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux

We describe a protocol design process, and illustrate its use by creating ATSPECT, an Authentication Test-based Secure Protocol for Electronic Commerce Transactions. The design process is organized around the authentication tests, a method for protocol verification based on the strand space theory. The authentication tests dictate how randomly generated values such as nonces may be combined with encryption to achieve authentication and freshness. ATSPECT offers functionality and security guarantees akin to the purchase request, payment authorization, and payment capture phases of SET, the secure electronic transaction standard created by the major credit card firms.

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable methods to determine many security properties of protocols. A separate line of work, initiated by Bellare and Rogaway, analyzes the way specific cryptographic primitives are used in protocols. It gives asymptotic bounds on the risk of failures of secrecy or authentication. In this paper we show how the Dolev–Yao model may be used for protocol analysis, while a further analysis gives a quantitative bound on the extent to which real cryptographic primitives may diverge from the idealized model. We illustrate this method where the cryptographic primitives are based on Carter–Wegman universal classes of hash functions. This choice allows us to give specific quantitative bounds rather than simply asymptotic bounds.

We describe a protocol design process, and illustrate its use by creating ATSPECT, an authentication test-based secure protocol for electronic commerce transactions. The design process is organized around the authentication tests, a method for protocol verification based on the strand space theory. The authentication tests dictate how randomly generated values such as nonces may be combined with encryption to achieve authentication and freshness. ATSPECT offers functionality and security guarantees akin to the purchase request, payment authorization, and payment capture phases of SET, the secure electronic transaction standard created by the major credit card firms.

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable methods to determine many security properties of protocols. A separate line of work, initiated by Bellare and Rogaway, analyzes the way specific cryptographic primitives are used in protocols. It gives asymptotic bounds on the risk of failures of secrecy or authentication.In this paper we show how the Dolev-Yao model may be used for protocol analysis, while a further analysis gives a quantitative bound on the extent to which real cryptographic primitives may diverge from the idealized model. We develop this method where the cryptographic primitives are based on Carter-Wegman universal classes of hash functions. This choice allows us to give specific quantitative bounds rather than simply asymptotic bounds.

One protocol (called the primary protocol) is independent of other protocols (jointly called the secondary protocol) if the question whether the primary protocol achieves a security goal never depends on whether the secondary protocol is in use. We use multiprotocol strand spaces to prove that two cryptographic protocols are independent if they use encryption in non-overlapping ways. This theorem applies even if the protocols share public key certificates and secret key "tickets". We use the method of Guttman et al. (2000) to study penetrator paths, namely sequences of penetrator actions connecting regular nodes (message transmissions or receptions) in the two protocols. Of special interest are inbound linking paths, which lead from a message transmission in the secondary protocol to a message reception in the primary protocol. We show that bundles can be modified to remove all inbound linking paths, if encryption does not overlap in the two protocols. The resulting bundle does not depend on any activity of the secondary protocol. We illustrate this method using the Neuman-Stubblebine protocol as an example.

Suppose a principal in a cryptographic protocol creates and transmits a message containing a new value v, which it later receives back in cryptographically altered form. It can conclude that some principal possessing the relevant key has transformed the message containing v. In some circumstances, this must be a regular participant of the protocol, not the penetrator. An inference of this kind is an authentication test. We introduce two main kinds of authentication test. An outgoing test is one in which the new value v is transmitted in encrypted form, and only a regular participant can extract it from that form. An incoming test is one in which v is received back in encrypted form, and only a regular participant can put it in that form. We combine these two tests with a supplementary idea, the unsolicited test, and a related method for checking that certain values remain secret. Together they determine what authentication properties are achieved by a wide range of cryptographic protocols. We introduce authentication tests and illustrate their power giving new and straightforward proofs of security goals for several protocols. We also illustrate how to use the authentication tests as a heuristic for finding attacks against incorrect protocols. Finally we suggest a protocol design process. We express these ideas in the strand space formalism and prove them correct elsewhere (Gullman and Thayer Fabrega, 2000).

Strand space analysis is a method for stating and proving correctness properties for cryptographic protocols. In this paper we apply the same method to the related problem of mixed protocols, and show that a protocol can remain correct even when used in combination with a range of other protocols. We illustrate the method with the familiar Otway-Rees protocol. We identify a simple and easily verified characteristic of protocols, and show that the Otway-Rees protocol remains correct even when used in combination with other protocols that have this characteristic. We also illustrate this method on the Neuman-Stubblebine protocol. This protocol has two parts, an authentication protocol (I) in which a key distribution center creates and distributes a Kerberos-like key, and a reauthentication protocol (II) in which a client resubmits a ticket containing that key. The re-authentication protocol II is known to be flawed. We show that in the presence of protocol II, there are also attacks against protocol I. We then define a variant of protocol II, and prove an authentication property of I that holds even in combination with the modified II.

A strand is a sequence of events; it represents either an execution by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol cor rectness claims may be expressed in terms of the connections between strands of different kinds. Preparing for a first example, the Needham–Schroeder–Lowe protocol, we prove a lemma that gives a bound on the abilities of the penetrator in any protocol. Our analysis of the example gives a detailed view of the conditions under which it achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham–Schroeder protocol fails. Before turning to a second example, we introduce ideals as a method to prove additional bounds on the abilities of the penetrator. We can then prove a number of correctness properties of the Otway–Rees protocol, and we clarify its limitations. We believe that our approach is distinguished from other work by the simplicity of the model, the precision of the results it produces, and the ease of developing intelligible and reliable proofs even without automated support.

In security protocol analysis, it is important to learn general principles that limit the abilities of an attacker and that can be applied repeatedly to a variety of protocols. The authors introduce the notion of an ideal-a set of messages closed under encryption and invariant under composition with arbitrary messages-to express such principles. In conjunction with the strand space formalism, they use the concept of ideals to prove bounds on a penetrator's capabilities, independent of the security protocol being analyzed. From this they prove a number of correctness properties of the Otway Rees protocol, using these results to explain the limitations of the protocol.

A strand is a sequence of events; it represents either the execution of an action by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the connections between strands of different kinds. In this paper, we develop the notion of a strand space. We then prove a generally useful lemma, as a sample result giving a general bound on the abilities of the penetrator in any protocol. We apply the strand space formalism to prove the correctness of the Needham-Schroeder-Lowe protocol (G. Lowe, 1995, 1996). Our approach gives a detailed view of the conditions under which the protocol achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham-Schroeder (1978) protocol fails. We believe that our approach is distinguished from other work on protocol verification by the simplicity of the model and the ease of producing intelligible and reliable proofs of protocol correctness even without automated support.

When packet filtering is used as a security mechanism, different routers may need to cooperate to enforce the desired security policy. It is difficult to ensure that they will do so correctly. We introduce a simple language for expressing global network access control policies of a kind that filtering routers are capable of enforcing. We then introduce an algorithm that, given the network topology, will compute a set of filters for the individual routers; these filters are guaranteed to enforce the policy correctly. Since these filters may not provide optimal service, a human must sometimes alter them. A second algorithm compares a resulting set of filters to the global network access control policy to determine all policy violations, or to report that none exist. A prototype implementation demonstrates that the algorithms are efficient enough to give quick answers to questions of realistic scale.

The verification work reported had three goals: (1) to develop a method for specifying components, which may be either software processes or hardware components, in terms of their possible event histories (also called traces); (2) to develop a method of verifying systems built from such components; and (3) to use these techniques to prove security properties about a realistic and substantial design. The approach to specification and verification is described. Although they do not yet have robust enough automated support to aid in the application described, the authors have devoted considerable attention to rigorously defining the logic suited to the method and exploring the type of software support needed. The main part of this study describes the use of the approach to specify and verify the security of the hardware architecture level of a hypothetical secure computing system. As far as the authors know, verification methods already in use are not suited to this sort of problem.>

A flaw in an operating system that had apparently been verified using the information flow technique indicates that the approach, as it has been practiced, is incomplete, The software tool that was used requires specifications to have a format prone to cause errors, so that a modification of the design of the tool is needed, Moreover, the verification process was logically incomplete, because flow analysis of a version of the specification free of errors yields formulas that can be proved only via invariant properties. This observation leads to an integration of two techniques for verifying security.