عنوان پایان‌نامه
بررسی و بهبود الگوریتم های تصادفی در مسئله صدق پذیری توسعه یافته با بکار گیری آن درسیستم های رمز نگاری ومقایسه با الگوریتم های بر اساسDPLL
- رشته تحصیلی
- مهندسی کامپیوتر- آلگوریتم ها و محاسبات
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه پردیس یک فنی شماره ثبت: 16..;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 47146
- تاریخ دفاع
- ۱۱ بهمن ۱۳۸۹
- دانشجو
- لیلا صمیمی دهکردی
- استاد راهنما
- علی معینی
- چکیده
- یکی از جالبترین مسائل علم ریاضیات گسسته، مسئله صدق¬پذیری می¬باشد که کاربردهای زیادی دارد و آن را پادشاه علم ریاضی گسسته نامیده¬اند. مسئله صدق¬پذیری شامل ترکیب عطفی تعدادی عبارت است که از ترکیب فصلی چند متغیر بولی ساخته شده¬اند و باید تخصیص مناسبی برای آنها یافت تا نتیجه صحیح بازگردانده شود. مسئله صدق¬پذیری برای بررسی کارایی و سرعت الگوریتمهای مختلف استفاده شده است، در اصل این مسئله روشی برای آنالیز و تحلیل الگوریتمها محسوب می¬شود. برای این مسئله در دو دهه اخیر راه¬حل¬های متعددی ارائه شده است و هر ساله این روشها بهبود می¬یابند. دراین رساله سعی داریم ابتدا این روشها رامورد بررسی قرار دهیم. پس از آن به ارائه یک روش جدید برای حل مسئله صدق¬پذیری خواهیم پرداخت که از ترکیب روشهای تصادفی و تکاملی حاصل شده است. از آنجایی که روشهای متفاوتی برای مسئله صدق¬پذیری وجود دارد، مسائل دیگر را می¬توان با تبدیل به این مسئله حل کرد. یکی از کاربردهای مهم این مسئله در الگوریتم¬های رمزنگاری است. با استفاده از حلالهای صدق¬پذیریِ طراحی شده برای این مسئله، می¬توان به حل سیستم معادلات حاصل از رمز پرداخت. به این روش، "تحلیل رمزی منطقی" می¬گویند که زیرمجموعه حمله جبری قرار می¬گیرد. در این روش، یافتن یک مدل برای تبدیل یک الگوریتم رمز به فرمول بولی، هم¬ارز با، یافتن کلیدی برای حمله به سیستم رمزنگاری می¬باشد. مسئله صدق¬پذیری شامل عملگرهای بولی عطف و فصل منطقی می¬باشد، اما سیستم معادلات حاصل از الگوریتم رمز معمولاً شامل عملگر یای ضمنی نیز می¬شود. تبدیل هر عبارت با یای ضمنی منجر به افزایش نمایی عبارات صدقپذیری خواهد شد، اما در سالهای اخیر روشهایی برای حل این مشکل ارائه شده است که ما آنها را بررسی خواهیم کرد و در نهایت با توجه به این روشهای جدید، یک الگوی جامع برای "تحلیل رمزی منطقی" ارائه خواهیم داد. پس از آن این تحلیل را روی سیستم رمز آ5/1 مربوط به دستگاه ارتباطات بین المللی همراه که جز رمزهای دنباله¬ای محسوب می¬شود، اعمال خواهیم کرد و مزایا و معایب روشهای حل را نشان خواهیم داد.
- Abstract
- One of the most interesting discrete mathematics problems is Satisfiability problem that has several applications and is called the king of discrete Math science. SAT problem has two parts. First instance: a set U contain variables and a collection named C of clauses on these variables; and second question: Is there a truth assignment for variables of U that satisfies all the clauses in C? SAT problem is used to study on the performance and speedy of different algorithms. In fact, this problem is a way for analysis of algorithms. In two recent years, several methods are prepared for solving SAT, and every year these methods are improved. In this thesis, we first study them. Then we propose a new SAT solver which is combined randomized technique with imperialist competitive algorithm. Since there are different methods for solving SAT, real world problems can be converted to it as a result of Cook theorem and then will be solved. One the important application of SAT is cryptography algorithm. We can solve encryption system of equations with SAT solvers. This method is called logical cryptanalysis; it is a subset of algebraic attacks. SAT problem consists of Boolean operators like ? and ? but cipher system of equations may consists of xor operator, too. Conversion of each xor-clause to CNF clause increase number of variables exponentially. In recent years, some methods are proposed to solve this problem and we study them. Then we propose a new pattern for logical cryptanalysis. We also apply this pattern on A5/1, a stream cipher that is used in mobile communication and show advantages and disadvantages of this new method.
