Qualitative and Quantitative Proofs of Security Properties
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 2013
- Accession Number
- ADA583931
Entities
People
- Joseph Halpern
Organizations
- Cornell University