What is the best way to prove a cryptographic protocol correct?

In this paper, we identify that protocol verification using invariants have significant limitations such as inapplicability to some protocols, non-standard attacker inferences and non-free term algebras. We argue that constraint solving for bounded process analysis can be used in conjunction with decidability of context-explicit protocols as a verification tool and can overcome those limitations. However, this is possible only when new decidability results are obtained for protocol security, especially in presence of non-standard inferences and non-free term algebras. Those results are under progress and will be soon submitted for publication. Keywords – Cryptographic protocols, Formal methods, Theorem proving, Invariants, Constraint solving, Decidability.

• Type: Conference
• Year: 2008
• Where: IPPS
• Authors: Sreekanth Malladi, Gurdeep S. Hura
• Keywords: Constraint Solving, Distributed And Parallel Computing, IPPS 2008, Non-free Term Algebras, Non-standard Attacker Inferences