TALK: Reasoning about time in Crypto Protocol Analysis Tools
Dr. Catherine Meadows, Naval Research Laboratory
Friday, November 15, 2019 · 12 - 1 PM
In-Person
·
Information Technology/Engineering : 227
The UMBC Cyber Defense Lab presents
Reasoning About Time in a Crypto Protocol Analysis Tool
Dr. Catherine Meadows, Naval Research Laboratory
12:00–1:00pm Friday, 15 November 2019, ITE 227
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 round-trip time of an RF signal to enforce constraints on location. To analyze these types 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 we represent timing properties as constraints, whose solution is outsourced to an SMT solver. We also discuss our experimental results.
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 the development of an analysis tool, Maude-NPA, that takes into account the 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 321. 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 1753681.
The UMBC Cyber Defense Lab meets biweekly Fridays. All meetings are open to the public.
Upcoming CDL Events:
Reasoning About Time in a Crypto Protocol Analysis Tool
Dr. Catherine Meadows, Naval Research Laboratory
12:00–1:00pm Friday, 15 November 2019, ITE 227
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 round-trip time of an RF signal to enforce constraints on location. To analyze these types 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 we represent timing properties as constraints, whose solution is outsourced to an SMT solver. We also discuss our experimental results.
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 the development of an analysis tool, Maude-NPA, that takes into account the 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 321. 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 1753681.
The UMBC Cyber Defense Lab meets biweekly Fridays. All meetings are open to the public.
Upcoming CDL Events:
- December 6, Karl Henderson, Verisign
- 9am—5pm daily, January 13-17, UMBC SFS/CySP Research Study, ITE 456
- January 31, 2020, TBA, biweekly CDL talks resume