BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-00-1632
       ENTRY:: June 02, 2000
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Finite-State Analysis of Security Protocols
        TYPE:: Technical Report
      AUTHOR:: Shmatikov, Vitaly
        DATE:: June 2000
       PAGES:: 93
    ABSTRACT:: Security protocols are notoriously difficult to design and
               debug. Even if the cryptographic primitives underlying a
               protocol are secure, unexpected interactions between parts of
               the protocol or several instances of the same protocol can
               lead to catastrophic security breaches. Since protocol
               attacks tend to be very subtle, some computer assistance is
               desirable.

               The main contribution of this thesis is to demonstrate how
               fully automatic finite-state techniques can be used to
               analyze a wide variety of security protocols. We present
               several case studies in which we model security protocols as
               finite-state systems, then perform automatic exhaustive state
               search that either discovers an attack, or proves the
               protocol correct subject to the limitations of the model.

               In our first study, we analyze SSL 3.0, a widely used
               Internet security protocol. The second study focuses on
               contract signing protocols designed to guarantee properties
               such as fairness and accountability. All analyses were
               performed using a general-purpose finite-state tool called
               Murphi. To alleviate the state-space explosion problem, we
               develop several state reduction techniques that exploit
               fundamental properties of security protocols. These
               optimizations make analysis of large protocols feasible, and
               establish Murphi as a viable protocol analysis tool.
       NOTES:: [Adminitrivia V1/Prg/20000602]
         END:: STAN//CS-TR-00-1632