Qualitative and Quantitative Proofs of Security Properties
CORNELL UNIV ITHACA NY
Pagination or Media Count:
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.