| | | Document Type | : | Latin Dissertation | | Language of Document | : | English | | Record Number | : | 53185 | | Doc. No | : | TL23139 | | Call number | : | 3276378 | | Main Entry | : | Shahabuddin Muhammad | | Title & Author | : | Extending distributed temporal protocol logic to a proof based framework for authentication protocolsShahabuddin Muhammad | | College | : | University of Central Florida | | Date | : | 2007 | | Degree | : | Ph.D. | | student score | : | 2007 | | Page No | : | 136 | | Abstract | : | Running critical applications, such as e-commerce, in a distributed environment requires assurance of the identities of the participants communicating with each other. Providing such assurance in a distributed environment is a di The Distributed Temporal Protocol Logic (DTPL) provides a language for formalizing both local and global properties of distributed communicating processes. The DTPL can be effectively applied to security protocol analysis as a model checker. Although, a model checker can determine flaws in a security protocol, it can not provide proof of the security properties of a protocol. In this research, we extend the DTPL language and construct a set of axioms by transforming the unified framework of SVO logic into DTPL. This results into a deductive style proof-based framework for the verification of authentication protocols. The proposed framework represents authentication protocols and concisely proves their security properties. We formalize various features essential for achieving authentication, such as message freshness, key association, and source association in our framework. Since analyzing security protocols greatly depends upon associating a received message to its source, we separately analyze the source association axioms, translate them into our framework, and extend the idea for public-key protocols. Developing a proof-based framework in temporal logic gives us another verification tool in addition to the existing model checker. A security property of a protocol can either be verified using our approach, or a design flaw can be identified using the model checker. In this way, we can analyze a security protocol from both perspectives while benefiting from the representation of distributed temporal protocol logic. A challenge-response strategy provides a higher level of abstraction for authentication protocols. Here, we also develop a set of formulae using the challenge-response strategy to analyze a protocol at an abstract level. This abstraction has been adapted from the authentication tests of the graph-theoretic approach of strand space method. First, we represent a protocol in logic and then use the challenge-response strategy to develop authentication tests. These tests help us find the possibility of attacks on authentication protocols by investigating the originator of its received messages. Identifying the unintended originator of a received message indicates the existence of possible flaws in a protocol. We have applied our strategy on several well-known protocols and have successfully identified the attacks. | | Subject | : | Applied sciences; Distributed temporal logic; Distributed systems; Computer security; Proof-based; Authentication protocols; Computer science; 0984:Computer science | | Added Entry | : | R. K. Guha | | Added Entry | : | University of Central Florida |
| | | | | |
| | |  |
http://lib.clisel.com/site/catalogue/53185
| | | |
| | | |
|