Paper Info
Title
Authentication and authorization protocol security property analysis with trace inclusion transformation and online minimization
Abstract
A major hurdle of formal analysis of protocol security properties is the well-known state explosion - a protocol system usually contains infinitely many or a formidable number of states. As a result, most of the analysis resorts to heuristics, such as state space pruning. Given the temporal property of authentication and authorization protocols, we introduce trace inclusion transformation of protocol specification to reduce significantly the state space. We further cut down the number of states by online minimization for obtaining a model of a manageable size for a formal and rigorous analysis. However, the two state space reduction procedures may result in false negative and false positives. We show that our trace inclusion transformation and online minimization do not introduce any false negative. On the other hand, we design an efficient algorithm for ruling out all the possible false positives. Therefore, our analysis is sound and complete. For a case study, we analyze OAuth, a standardization of API authentication protocols. Our automated analysis identifies a number of attacks in the original specification, including the one that has been detected. We also analyze the second version of OAuth and prove it is secure if the API interface is secure.
Year
DOI
Venue
2010
10.1109/ICNP.2010.5762765
ICNP
Keywords
Field
DocType
rigorous analysis,false positive,analysis resort,authorization protocol security property,state space,state space pruning,online minimization,formal analysis,trace inclusion transformation,possible false positive,automated analysis,authorisation,minimization,protocols,authentication protocol,authorization,authentication protocols,algorithm design and analysis,application programming interface,extended finite state machine,authentication
Authentication,Algorithm design,Computer science,Computer network,Theoretical computer science,Authentication protocol,Heuristics,Minification,Application programming interface,State space,False positive paradox
Conference
Citations 
PageRank 
References 
2
0.38
20
Authors
2
Name
Order
Citations
PageRank
Ya-Ting Hsu1304.32
David Lee219521.40