Accession Number:

ADA583931

Title:

Qualitative and Quantitative Proofs of Security Properties

Descriptive Note:

Final rept.

Corporate Author:

CORNELL UNIV ITHACA NY

Personal Author(s):

Report Date:

2013-04-01

Pagination or Media Count:

9.0

Abstract:

The goal of this project has been to develop logics for reasoning about security at both the qualitative and quantitative level. Two approaches have been considered. The first builds on a logic designed by the PI that has a binary operator -, where p-q is interested as the probability of p given q goes to 1. The logic has been applied to proving the correctness of a variety of security protocols. Doing this required extending the original logic to include additional operators for reasoning about traces, essentially with features in the spirit of dynamic logic. A sound proof system for the extended logic was developed. The second approach involves a logic for reasoning about knowledge, probability and time. A special case, restricting to only probability 1 statements, gives a qualitative logic of belief. A key innovation in the logic is distinguishing between strings and message terms. This allows an agent receiving a string s that represents a message m encrypted by a key k to be uncertain about what message term the strings represents. It is shown that this approach deals with resource-bounded agents in a natural and powerful way.

Subject Categories:

  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE