Dr. Catherine Meadows
Naval Research Laboratory
12:00 noon–1pm
Friday, November 15, 2019
ITE 227
Abstract:
The ability to guarantee timing properties, and in turn to use assumption about time to guarantee the security of protocols, is important to many of the applications we rely upon. For example, to compute locations, GPS depends on time synchronization between entities. Blockchain protocols require loose time synchronization to guarantee agreement on block timestamps. Distance-bounding protocols use the roundtrip time of an RF signal to enforce constraints on location. To analyze these types of protocols formally, it is necessary to reason about time.
This talk describes recent research in extending the Maude-NPA cryptographic protocol analysis tool to reason about cryptographic protocols that rely on or enforce timing properties. We describe the timing model we have created for the tool. We show how we represent timing properties as constraints, whose solution is outsourced to an SMT solver. We also discuss our experimental results.
About the Speaker:
Catherine Meadows is a senior researcher in computer security at the Center for High Assurance Systems at the Naval Research Laboratory and heads that group's Formal Methods Section. She was the principal developer of the NRL Protocol Analyzer (NPA), which was one of the first software tools to find previously undiscovered flaws in cryptographic protocols, and was used successfully in the analysis of a number of protocol standards. She is also leading or has recently led, a number of projects related to the design and analysis of cryptographic protocols, including one focused on the development of an analysis tool, Maude-NPA, that takes into account the complex algebraic properties of cryptosystems, another that is focusing on the automatic generation of secure cryptosystems, and another devoted to formal methods for the design of cyber-physical systems with legacy components. This work was supported by ONR 311.
Email: catherine.meadows@nrl.navy.mil
Host:
Alan T. Sherman, sherman@umbc.edu
Support for this event was provided in part by the National Science Foundation under SFS grant DGE-1753681.