Cyber & formal methods publications

A system for private stream searching, introduced by Ostrovsky and Skeith, allows a client to provide an untrusted server with an encrypted search query.

Given a theory 𝕋T, a set of equations E, and a single equation e, the uniform word problem (UWP) is to determine if 𝐸⇒𝑒E⇒e in the theory 𝕋T.

We present a novel alert correlation approach based on the factor analysis statistical technique for malware characterization. Our approach involves mechanically computing a set of abstract quantities, called factors, for expressing…

This paper argues for the development of a formal framework for constructing “digital artifacts” that can serve as proxies for physical evidence; a system so imbued would facilitate sound digital…

This paper introduces novel features of Maude 2.4 including support for unification and narrowing. Unification is supported in Core Maude, the core rewriting engine of Maude, with commands and metalevel…

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.

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 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.

In this paper, we design a model-based intrusion detection system (IDS) for sensor networks used for PCS.