## Grants - AWARD SUMMARY

### UNIVERSITY OF NEW MEXICO

Although much progress has been made on the theoretical understanding of cryptographic protocols, security vulnerabilities are still found in protocol standards and implementations long after they have been accepted and fielded. As in the case of software verification, some kind of automated assistance is highly desirable. Indeed, we have already seen how the use of automated methods can be of help in the evaluation of security standards. The usefulness of formal methods also depends on how faithfully they can represent the system they are being used to evaluate. Traditionally, the use of formal methods for crypto protocol verification has relied upon the use of the {\em free algebra} model originally proposed by Dolev and Yao. Principals engage in protocols by performing operations on data. However, there are a number of widely used operations whose essential properties cannot be represented in the free algebra model. Examples include associativity of concatenation, associativity and commutativity in modular exponentiation-based protocols such as Diffie-Hellman, and associativity, commutativity and self-cancellation in exclusive-or. Indeed, there have been cases, such as Paulson's analysis of the Bull recursive authentication protocol in which protocols using these sorts of operations have been proven secure in the free algebra model, but have been later found to be flawed. There is thus a great need for protocol reasoning techniques that take into account the different equational properties of cryptosystems. {\em Equational unification} is a technique that shows great promise for application to these problems. Briefly, equational unification gives a compact representation of all circumstances under which two different terms are equal. Thus, it has potential as a practical means for reasoning about protocols that use cryptosystems with different equational properties. Indeed, an earlier tool, the NRL Protocol Analyzer, made very successful use of equational unification, although it could only reason about a small class of theories. The project uses the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the analysis of cryptographic protocols using functions that obey different equational theories, is being further developed by Meadows and Meseguer at UIUC NRL, in cooperation with Santiago Escobar. Other PIs, Kapur, Lynch and Narendran, as well as their students, are learning about the tool so that the new unification algorithms can be implemented.

#### Clarification of Codes

Choose a quarter and click "Go."

## AWARD OVERVIEW

AWARD OVERVIEW
Award Number 0905222 Funding Agency National Science Foundation
Total Award Amount $240,000 Project Location - City Albuquerque Award Date 07/14/2009 Project Location - State NM Project Status More than 50% Completed Project Location - Zip 87131-0001 Jobs Reported 0.00 Congressional District 01 Project Location - Country US ## Recipient Information (Grants) Recipient Information (Grants) Recipient Name UNIVERSITY OF NEW MEXICO Recipient DUNS Number 868853094 Recipient Address 1700 LOMAS BLVD NE STE 2200 Recipient City ALBUQUERQUE Recipient State New Mexico Recipient Zip 87106-3807 Recipient Congressional District 01 Recipient Country USA Required to Report Top 5 Highly Compensated Officials No ## Projects and Jobs Information Projects and Jobs Information Project Title TC: Medium: Collaborative Research: Unification Laboratory: Increasing the Power of Cryptographic Protocal Analysis Tools Project Status More than 50% Completed Final Project Report Submitted No Project Activities Description Computer & Information Science Quarterly Activities/Project Description We have developed algorithms for combining asymmetric unification algorithms for theories with certain properties. This would help considerably in developing modular approaches to asymmetric unification algorithms as they are needed in cryptographic protocols based on the semantic properties of operators used in encoding/decoding. Two papers - one on asymmetric unification for the theory of exclusive and another one on hierarchical combination of unification algorithms were presented at the prestigious international conference on Automated Deduction (CADE) in Lake Placid in June 2013. The PI also met there other participants of this project and held numerous technical discussions. Jobs Created 0.00 Description of Jobs Created No jobs created/retained this quarter. ## Purchaser Information (Grants) Purchaser Information Contracting Office ID Not Reported Contracting Office Name Not Available Contracting Office Region Not Available TAS Major Program 49-0101 ## Award Information Award Information Award Date 07/14/2009 Award Number 0905222 Order Number Award Type Grants Funding Agency ID 49 Funding Agency Name National Science Foundation Funding Office Name Not Available Awarding Agency ID 49 Awarding Agency Name National Science Foundation Amount of Award$240,000
Funds Invoiced/Received $239,946 Expenditure Amount$239,946
Infrastructure Expenditure Amount $0 Infrastructure Purpose and Rationale Not Reported Infrastructure Point of Contact Name Not Reported Infrastructure Point of Contact Email Not Reported Infrastructure Point of Contact Phone Not Reported Infrastructure Point of Contact Address Not Reported Infrastructure Point of Contact City Not Reported Infrastructure Point of Contact State Not Reported Infrastructure Point of Contact Zip Not Reported ## Product or Service Information (Grants) Product or Service Information Primary Activity Code U03.02 Activity Description Computer & Information Science ## Sub-Awards Information Sub-Awards Information Sub-awards to Organizations 0 Sub-award Amounts to Organizations$0
Sub-Awards to Individuals 0
Sub-Award Amounts to Individuals $0 Number of Sub-awards less than$25,000/award 0
Amount of Sub-awards less than $25,000/award$0
Number of payments to vendors greater than $25,000 0 Total Amount of payments to vendors greater than$25,000/award $0 Number of payments to vendors less than$25,000/award 4
Total Amount of payments to vendors less than $25,000/award$3,056

## Project Location Detail

Location Information
Latitude, Longitude 35º 5' 22", -106º 37' 12"
Congressional District 01
Address 1 1 University of New Mexico