کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10329775 | 685519 | 2005 | 18 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
In previous work we showed that automatic SAT-based model-checking techniques based on a reduction of protocol (in)security problems to a sequence of propositional satisfiability problems can be used to effectively find attacks on protocols. In this paper we present an optimized intruder model that may lead in many cases to shorter attacks which can be detected in our framework by generating smaller propositional formulae. The key idea is to assume that some of the abilities of the intruder have instantaneous effect, whereas in the previously adopted approach all the abilities of the intruder were modeled as state transitions. This required non trivial extensions to the SAT-reduction techniques which are formally described in the paper. Experimental results indicate the advantages of the proposed optimization.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 125, Issue 1, 3 March 2005, Pages 91-108
Journal: Electronic Notes in Theoretical Computer Science - Volume 125, Issue 1, 3 March 2005, Pages 91-108
نویسندگان
Alessandro Armando, Luca Compagna,