CSE-MTECH-03-009




Formal Analysis of Cryptographic Protocols
Aldrin John DSouza, M.Tech, 03, 57 pp.
Department of Computer Science and Engineering
Indian Institute of Technology Bombay, Powai, Mumbai 400 076.
Supervisor(s): G.Sivakumar

The process of designing a correct cryptographic protocol does not end with getting the cryptographic primitives right. The literature is full of protocols which were initially believed to be correct, and were later found to have flaws. Interestingly, most of these are structural flaws, i.e. the intruder can subvert the goals of the protocol without breaking the underlying crypto-system. Given the wide range of operations which the intruder uses to compose these attacks, it is very difficult for the designer to intuitively reason about these attacks. Formal methods of analysis should thus be applied before the protocols are put to use. Such an analysis involves developing property preserving abstractions of protocols, specification languages to express goals and assumptions, and procedures to decide whether the protocol achieves its intent. The Strand Space Model is one of the existing cryptographic protocol analysis mechanisms. Here, we describe how proofs in the strand spaces formalism can be generalized and applied to a range of protocols. We formalize our generalization in PVS and describe how a protocol description in a common specification language can be translated to theories, which can be used to prove the correctness of protocol properties.