Formal Methods Section
Code 5543 is the Formal Methods Section in the Center for High Assurance Computer Systems Branch of the Information Technology Division.
The mission of the Formal Methods Section is to perform research on extensible and adaptable foundational theories that can be applied to present and emerging security problems. Our current areas of interest are listed below.
Cryptographic Protocol and Analysis
Theory and Design
- Applications of rewriting logic and unification to cryptographic protocol analysis
- Logical and mathematical techniques for verifying security of authentication in pervasive computing
Products and Applications
- The Maude-NRL Protocol Analyzer (Maude-NPA). Learn more here.
- Secure Network Localization Protocol (SNLP), a protocol for securely determining and distributing location information in a wireless network
- Security analyses of proximity verification protocols
Information Hiding
Theory and Design
- Area of computer science dealing with metrics to assess how well private information is hidden, and how to hide it
- Areas being addressed include covert channels, traffic analysis, steganography and watermarking, and neuron models
Inventions
- U.S. Patent for the NRL Network Pump®
- U.S. Patent for Phasemark digital watermarking system
- Topological approach to image steganography: methods J1 and J2
- Stego scrubbing
Anonymous Communication
Theory and Design
- Mathematical modeling and analysis of anonymity, privacy, and routing security in communication systems
- Building blocks, cryptographic primitives, and designs for anonymous and route-secure communication
- Economic, usability, and incentive analysis of anonymous and route-secure communication systems
Inventions
- Unlinkable Serial Transaction for subscription services to manage subscription sharing but prevent a service from tracking client transactions
- Onion Routing network overlay approach to general low-latency communication resistant to traffic analysis
- Original design and deployment of Tor, the widely-used anonymous communication application network and test bed
- Hidden servers for survivable and location-protected services
- REP, RFID Enhancer Proxy device for improving the privacy and usability of RFID tags
Mathematical & Logical Analysis of Distributed Systems
Theory and Design
- Constructing new logical methods for distributed systems
- Formalization of fundamental principles underlying hardware/software co-design
- New logical methods for functional programming using monads
- Generalization of logic principles implicit in models for security
Applications
- Information channel separation in FPGA designs
Informatic Phenomena
Theory and Design
- Domain theory
- Quantum information
- Causal structure in relativity
Applications
- New mathematical representations making it easier to analyze communication process in realistic environments
- Methods for increasing bandwidth in communication