امنيت اثبات‌پذير در پروتكل‌هاي رمزنگاري

Provable Security in Cryptographic Protocols

هدف از يك پروتكل امنيتي (پروتكل رمزنگاشتي)، برآوردن مجموعه اي از نيازمندي هاي امنيتي است. ارزيابي امنيتي اين پروتكل ها بسيار حايز اهميت است، به طوري كه مي توان گفت ارايه يك پروتكل رمزنگاشتي بدون ارزيابي امنيتي عملاً فاقد ارزش است. در ارزيابي امنيتي پروتكل هاي رمزنگاري از سه رويكرد شهودي، صوري و اثبات پذير استفاده مي شود. از اين ميان اخيراً روش هاي اثبات پذير در تحليل امنيتي پروتكل ها بسيار مورد توجه قرار گرفته اند. اثبات امنيت يك پروتكل، بر مبناي روش هاي رياضي معمول در رمزنگاري صورت مي گيرد. در چنين اثبات هايي ابتدا توانمندي هاي دشمن در حمله به پروتكل و مفهوم شكستن پروتكل، در قالب يك مدل رياضي تعريف مي‌شود. سپس نشان داده مي شود كه در صورت پيروزي دشمن در حمله به پروتكل بر اساس مدل مطرح شده، مي توان مساله اي سخت در نظريه پيچيدگي محاسبات را حل ‌كرد؛ كه اين امر با سختي اين مسايل در نظريه پيچيدگي محاسبات در تناقض است. چنين روندي، كاهش به يك مساله سخت ناميده مي شود. در بحث امنيت اثبات پذير مفاهيمي از قبيل مدل اوراكل تصادفي، مدل استاندارد و مدل تركيب پذير جامع مطرح مي‌شود. اگر در فرآيند اثبات از فرض هاي ايده آل (مانند فرض تصادفي بودن خروجي توابع درهم ساز) استفاده شود، گفته مي شود كه اثبات در مدل هاي ايده آل (مانند مدل اوراكل تصادفي) انجام گرفته است؛ درغير اين صورت، اثبات در مدل استاندارد خواهد بود. اخيراً در فرآيند اثبات امنيت در پروتكل ها، مدلي تحت عنوان مدل تركيب پذير جامع مطرح شده است. اگر اثبات امنيت پروتكلي در مدل تركيب پذير جامع صورت گيرد، مي توان اطمينان داشت كه وقتي پروتكل به عنوان جزيي از يك سامانه بزرگ تر به كار مي رود، باز امنيت آن تضمين شده است. هدف از اين مقاله، معرفي و بررسي روش ها و رويكردها در بحث امنيت اثبات پذير است.

The goal of a security protocol (cryptographic protocol) is to satisfy a set of security requirements. The security analysis of these protocols has a great degree of importance, as in practice, proposing a cryptographic protocol without the security analysis is not valuable. There are three approaches in security analysis of cryptographic protocols: heuristic, formal and provable approaches. Recently, provable approaches have been of a great attention. The security proof of a protocol is based on usual mathematical methods in cryptography. In these proofs, first the adversarial power and the concept of breaking the protocol are defined in a formal model. Afterwards, it is shown that if the adversary can break the protocol in defined model, a hard problem in computational complexity theory can be solved. This approach is called reduction to a hard problem. The concepts such as random oracle model, standard model and universally composable model are discussed in the field of provable security. If ideal assumptions (such as the assumption of randomness of the output of hash functions) are considered in the process of the proof, the proof will be in ideal models (such as random oracle model), otherwise, the proof will be in the standard model. Recently, the concept of the universally composable (UC) model is defined in the proof of security. If the security of a protocol is proved in the UC model, its security will be guaranteed, even if the protocol is used in a larger and more complex system. The purpose of this paper is an introduction to approaches in provable security.