Cryptographic Protocol Verification Based on the Extension Rule

The design of cryptographic protocols is error-prone. People have found serious security flaws in major cryptographic protocols. In recent years, people use formal methods to guarantee the correctness of cryptographic protocols in a strong sense. Resolution-based theorem proving is a widely-used formal method, but there are other techniques as well. For example, the extension rule is another technique used to prove things formally. In this paper, we propose to prove the correctness of cryptographic protocols based on the extension rule. We show that this is an effective technique, which can help to find the security flaws in major cryptographic protocols.