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.