@PhdThesis{Compagna-PhD05,
 author  = {Compagna, L.},
 title   = {{SAT-based Model-Checking of Security Protocols}},
 school  = {Universit\`a degli Studi di Genova and the University of Edinburgh (joint programme)},
 year    = {2005},
 month   = {September},
 summary = {Security protocols are communication protocols that aim at
            providing security guarantees through the application of
            cryptographic primitives.  Since these protocols are at
            the core of security-sensitive applications in a variety
            of domains (e.g.\@ health-care, e-commerce, and
            e-government), their proper functioning is crucial as a
            failure may undermine the customer and, more in general,
            the public trust in these applications.  In spite of their
            apparent simplicity, security protocols are notoriously
            error-prone.  It is thus of utmost importance to have
            tools and specification languages that support the
            activity of finding flaws in protocols.  
            This thesis presents an high level protocol specification
            language accessible to protocol designers and easily
            translatable into a lower-level formalism for protocol
            insecurity problems.
            This thesis shows that automatic SAT-based model-checking
            techniques based on a reduction of protocol insecurity
            problems to propositional satisfiability problems (SAT)
            can be used effectively to find attacks on security
            protocols.  The approach results from the combination of a
            reduction of protocol insecurity problems into planning
            problems and SAT-encoding techniques developed for
            planning.  A model-checker, SATMC, based on these ideas
            has been developed and experimental results obtained by
            running SATMC against industrial-scale security protocols
            confirm the effectiveness of the approach.},
}