Jump to content United States-English
HP.com Home Products and Services Support and Drivers Solutions How to Buy
» Contact HP

hp.com home


Technical Reports


printable version
» 

HP Labs

» Research
» News and events
» Technical reports
» About HP Labs
» Careers @ HP Labs
» Worldwide sites
» Downloads
Content starts here

  Click here for full text: PDF

Introducing ASPECT - a tool for checking protocol security

Monahan, Brian

HPL-2002-246

Keyword(s): security protocols; software tools; strand spaces; formal methods

Abstract: We have developed an efficient proof-of-concept prototype tool for security protocol validation called ASPECT. This prototype is designed to demonstrate the feasibility of our approach to security protocol checking and validation. Our approach can be characterised in terms of "flaw-detection for security protocols", much in the same way that programs in a programming language can be type checked. However, we go beyond approaches based solely upon static analysis by combining an initial static, passive analysis with an active search that attempts to uncover attacks upon the given protocol. Naturally, a successful attack indicates the presence of a security flaw in the protocol. More precisely, ASPECT takes a conventional security protocol description given in terms of message sequences between several parties, and analyses this statically in terms of defined high- level security goals (e.g. confidentiality, authorisation) to derive a number of conjectured security properties for the given protocol. ASPECT then attempts to find protocol flaws, if any, by trying to dynamically construct active attack patterns to disprove these conjectures. The question of whether the checking techniques used within ASPECT are complete is currently open and the subject of further research. In this introductory report, we illustrate what ASPECT does in terms of a worked example, where we develop a simple authentication protocol. This protocol is revised several times and ASPECT used to examine these revisions. As you would anticipate, ASPECT finds no flaws with the final revision of this protocol.

33 Pages

Back to Index

»Technical Reports

» 2009
» 2008
» 2007
» 2006
» 2005
» 2004
» 2003
» 2002
» 2001
» 2000
» 1990 - 1999

Heritage Technical Reports

» Compaq & DEC Technical Reports
» Tandem Technical Reports
Privacy statement Using this site means you accept its terms Feedback to HP Labs
© 2009 Hewlett-Packard Development Company, L.P.