Cyber & formal methods publications

We present new techniques for achieving adaptive security in broadcast encryption systems. Previous work on fully collusion resistant broadcast encryption systems with very short ciphertexts was limited to considering only static security.

We formalize the problem of defending honeynets from systematic mapping (a serious threat to their viability) as a simple two-person game.

Abstract This talk discusses some of the challenges of building a usable theorem prover. These include the chasm between theory and code, conflicting requirements, feature interaction, and competitive performance. The…

Here we demonstrate additional applications that enjoy strong security properties and a high level of efficiency.

Our approach involves a multilayer security architecture for monitoring process control systems to achieve accurate and effective situational awareness.

We present a unifying framework that extends the CP formalism in both model and solutions, to tackle ill-defined combinatorial problems with incomplete or erroneous data.

We explore the theoretical limits for doing automatic invariant checking and show that invariant checking is decidable for a large class of programs that includes some recursive programs.

We give an overview of algorithms that we have been developing in the DARPA disruption-tolerant networking program, which aims at improving communication in networks with intermittent and episodic connectivity.

This paper describes RSR in the context of a general vulnerability management cycle (VMC), familiarizes the reader with the applicable information assurance (IA) properties, and discusses how to use existing…

We argue that trust need not be achieved at the expense of automation, and outline a lightweight approach where the results of untrusted verifiers are checked by a trusted offline…