Abstract:
The symbol approach and the computational approach are two different approaches in security protocols' formal analysis, but the former is quite alien to the latter. The former regards protocols as a set of symbols and believes that cryptography has a secure property of “all-or-nothing”; the latter regards protocols as a set of strings, and considers that cryptography is not strong enough to resist adversary's attack. Because each approach has flaws and virtues, an idea is brought forward that is engaged in drawing virtues from both approaches and discarding their flaws to build a mature approach to analyze security protocols. A new analytic approach reconciling the two approaches is constructed following this idea. The new approach defines the security as the completeness and the correctness, through analyzing them. It not only can examine whether protocols could reach the expectant goals, but also can compute adversary's aggressive ability to protocols. The approach is the first one which puts forward the idea that analyzes security protocols from logistic reliability and cryptographic reliability.