Foundations of Security Protocol Analysis

DSpace/Manakin Repository

Foundations of Security Protocol Analysis

Show simple item record

dc.contributor.author Suresh, S. P.
dc.date.accessioned 2009-09-09T05:22:09Z
dc.date.available 2009-09-09T05:22:09Z
dc.date.issued 2009-09-09T05:22:09Z
dc.date.submitted 2003
dc.identifier.uri http://hdl.handle.net/123456789/105
dc.description.abstract One of the central problems in the automatic verification of security protocols is that of verifying whether a given protocol leaks secrets or not. It identifies syntactic subclasses of protocols for which the secrecy problem is decidable. It also concerns reasoning about protocols. The author introduces a logic using which interesting properties of protocols can be specified and reasoned about. A formal model of security protocols is set up, and several important properties about the model are proved. In particular the properties relating to synth and anlz proofs which formalise the way the agents running a protocol derive new information from the old. The secrecy problem is considered and shown that it is undecidable both when the set of nonces is infinite and when the length of messages is unbounded. Relatively simple and uniform proofs for both these results are proved. Then the secrecy problem is considered in the setting of infintely many nonces, but bounded message length. It is proved that for a syntactic subclass of protocols called 'tagged protocols' the secrecy problem in this setting is decidable. It is also proved that the tagged protocol has a leaky run iff it has a leaky run containing only bounded length messages; And further the secrecy problem for tagged protocols is decidable even in the setting where both message length and number of nonces is unbounded. About reasoning, a logic is defined in which one can easily specify several interesting security properties like secrecy, authenticity, etc., Some examples are given to illustrate how to reason about protocols. Some of the undecidability and decidability results are extended to the verification problem of logic. en_US
dc.subject Security Protocol Analysis en_US
dc.subject Verification-Secrecy, Authenticity en_US
dc.subject Logics en_US
dc.title Foundations of Security Protocol Analysis en_US
dc.type.degree Ph.D en_US
dc.type.institution University of Madras en_US
dc.description.advisor Ramanujam, R.
dc.description.pages ix; 141p. en_US
dc.type.mainsub Computer Science en_US

Files in this item

Files Size Format View
suresh_sp_phd.pdf 885.4Kb PDF View/Open

This item appears in the following Collection(s)

Show simple item record

Search DSpace


Advanced Search

Browse

My Account