An increasing number of security protocols are becoming more important. These protocols are being developed extremely rapidly as well, and it's hard to get these protocols right. We would like to automate the protocol-checking process to save time and gain more confidence in the results. There are several approaches to verifying that a protocol is correct. Handwritten proofs are easy to get wrong. Another approach which is effective, though tedious, is to reason about a protocol in high-order logic and use theorem proving software to verify correctness. Finally, small logics have been developed for reasoning about parts of protocols, e.g. BAN. The usual answer from such logics is limited to yes, no, or cannot decide.
The focus of this work is on improving automated support for using small logics. In such logics, a protocol message is represented as a logic formula reflecting the result of the message being received, a set of assumptions, and a set of inference rules to express familiar concepts. Usually, the premises of the rules are larger than the conclusions. Thus, the process of generating conclusions will terminate eventually.
We can exhaustively produce all truths in the protocol. With these truths, we can check that properties hold and explore what effect changes in the protocol will have on the truths generated.
A logic checker was implemented which can verify that a logic satisfies certain restrictions. In the actual checker, there are three types of rules: shrinking, growing, and rewrites. The checker uses shrinking rules to generate truths, only applying other rules when no more shrinking rules can be applied. This method does not generate all truths, but typically, interesting truths are generated. We can also check whether a specific formula is derivable.
Currently, the logic checker should be useful for protocol developers; it is automatic and fast, with most runs being on the order of one to two minutes. In the future, more logics will be developed to reason about other properties such as anonymity or safety from man-in-the-middle attacks, and support for temporal logics will be added.
Nevin Heintze was curious as to whether, given a property, a system could work backwards, giving changes to a protocol which would be required for the property to hold. Darrell pointed to model checking, which gives a counter-example when a property does not hold, and said that getting the smallest set of changes to a protocol that would make a property hold would be possible.