Toward Compositional Analysis of Security Protocols Using Theorem Proving
Oleg Sheyner, Wing, Jeannette · Defense Technical Information Center (DTIC) · 2000
Complex security protocols require a formal approach to ensure their correctness. The protocols are frequently composed of several smaller, simpler components. We would like to take advantage of the compositional nature of such protocols to split the large verification task into separate and more manageable pieces. Various formalisms have been used successfully for reasoning about large protocol compositions by hand. However hand proofs are prone to error. Automated proof systems can help make the proofs more rigorous. The goal of our work is to develop an automated proof environment for compositional reasoning about systems. This environment would combine the power of compositional reasoning with the rigor of mechanically-checked proofs. The hope is that the resulting system would be useful in verification of security protocols of real-life size and complexity. Toward this goal we present results of a case study in compositional verification of a private communication protocol with the aid of automated proof tool Isabelle/IOA.