Probabilistic polynomial-time semantics for a protocol security logic

Full textClick to download.
CitationIn Proceedings of 32nd International Colloquium on Automata, Languages and Programming, pp. 16-29, July 2005
AuthorsAnupam Datta
Ante Derek
John C. Mitchell
Vitaly Shmatikov
Mathieu Turuani


We describe a cryptographically sound formal logic for proving protocol security properties without explicitly reasoning about probability, asymptotic complexity, or the ations of a malicious attacker. The approach rests on a new probabilistic, polynomial-time semantics for an existing protocol security logic, replacing an earlier semantics that uses nondeterministic symbolic evauation. While the basic form of the protocol logic remains unchanged from previous work, there are some interesting technical problems involving the difference between efficiently recognizing and efficiently producing a value, and involving a reinterpretation of standard logical connectives that seems necessary to support certain forms of reasoning.

Back to publications
Back to previous page