Team for Research in
Ubiquitous Secure Technology

Citation
"ASPIER: An Automated Framework for Verifying Security Protocol Implementations". S. Chaki, A. Datta (eds.), 22nd IEEE Computer Security Foundations Symposium, July, 2009.

Abstract
We present ASPIER – the first framework that combines software model checking with a standard protocol security model to automatically analyze authentication and secrecy properties of protocol implementations in C. The technical approach extends the iterative abstraction-refinement methodology for software model checking with a domainspecific protocol and symbolic attacker model. We have implemented the ASPIER tool and used it to verify authentication and secrecy properties of a part of an industrial strength protocol implementation – the handshake in OpenSSL – for configurations consisting of up to 3 servers and 3 clients. We have also implemented two distinct methods for reasoning about attacker message derivations, and evaluated them in the context of OpenSSL verification. ASPIER detected the “version-rollback” vulnerability in OpenSSL 0.9.6c source code and successfully verified the implementation when clients and servers are only willing to run SSL 3.0.

Electronic downloads

• chaki-datta-csf09.pdf · application/pdf · 260 kbytes

• HTML

   <a
  href="http://www.truststc.org/pubs/752.html"
  ><i>ASPIER: An Automated Framework for Verifying
  Security Protocol Implementations</i></a>, S.
  Chaki, A. Datta (eds.), 22nd IEEE Computer Security
  Foundations Symposium, July, 2009.

• Plain text

   "ASPIER: An Automated Framework for Verifying Security
  Protocol Implementations". S. Chaki, A. Datta (eds.),
  22nd IEEE Computer Security Foundations Symposium, July,
  2009.

• BibTeX

  @proceedings{ChakiDatta09_ASPIERAutomatedFrameworkForVerifyingSecurityProtocol,
      title = {ASPIER: An Automated Framework for Verifying
                Security Protocol Implementations},
      editor = {S. Chaki, A. Datta},
      organization = {22nd IEEE Computer Security Foundations Symposium},
      month = {July},
      year = {2009},
      abstract = {We present ASPIER � the first framework that
                combines software model checking with a standard
                protocol security model to automatically analyze
                authentication and secrecy properties of protocol
                implementations in C. The technical approach
                extends the iterative abstraction-refinement
                methodology for software model checking with a
                domainspecific protocol and symbolic attacker
                model. We have implemented the ASPIER tool and
                used it to verify authentication and secrecy
                properties of a part of an industrial strength
                protocol implementation � the handshake in
                OpenSSL � for configurations consisting of up to
                3 servers and 3 clients. We have also implemented
                two distinct methods for reasoning about attacker
                message derivations, and evaluated them in the
                context of OpenSSL verification. ASPIER detected
                the �version-rollback� vulnerability in
                OpenSSL 0.9.6c source code and successfully
                verified the implementation when clients and
                servers are only willing to run SSL 3.0.},
      URL = {http://www.truststc.org/pubs/752.html}
  }
  

Posted by Jessica Gamble on 5 May 2010.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.