Description_of_Services.docx

Advanced Support for Protocol Analysis - Algorithms and GUI The Naval Research Laboratory (NRL) has a defined need for the development and improvement of software that is used by NRL experiments with formal analysis of cryptographic protocols. The tasking includes:

1) Provide and improve features offered by the Maude language in which NRL’s experimental tool, Maude-NPA, is implemented: variant generations, associative unification, narrowing, and reasoning about group protocols

2) Develop a graphical user interface (GUI) for Maude-NPA that will make it easier for NRL and its collaborators to run experiments and to teach other users how to use the tool.

The potential contractor must be an expert in and have substantial experience with the development of the Maude programming language.

This project has three main task areas

I Advanced Maude support for protocol analysis II GUI development III Formal analysis of n-party protocols

Task I. Advanced Maude support for protocol analysis.

This task involved extending Maude support for variant generation, associative unification and narrowing.

1. Variant generation for the non-finite case will be supported by providing functionality to get all variants at depth n.

2 Associative unification will be extended to handle more cases. The ability to stop with incomplete notification will be implemented. The unification combination algorithm will be revised to handle incomplete algorithms.

3 One step narrowing modulo supported theories. Narrowing search will be extended with user definable strategies.

Task II. Graphical User Interface (GUI) development.

The GUI development task includes developing and implementing a protocol specification input language; designing a property language and implementing and interface for input of properties; and engineering (optimization, support for mac and linux platforms, and developing a client server version.)

Task III. Formal analysis of n-party protocols.

The objective is to develop methods for formal specification and proof of security properties of n-party protocols parametric in the number of parties. Challenges include uniform formal specification of protocol strands, reasoning about message patterns with term variables and formalization of agreement on session.

Deliverables

Task I. Maude extensions and documentation

Task II. GUI implementation and documentation. Delivered as downloadable code.

Task III. Formalizations in PVS and accompanying documentation