مقاله آنالیز و بهبود پروتکل امنیتی Yahalom بوسیله ابزار Scyther

بخشی از مقاله

آنالیز و بهبود پروتکل امنیتی Yahalom بوسیله ابزار Scyther

چکیده - درستی پروتکلهای امنیتی برای شبکه های امن بسیار مهم است زیرا ممکن است عیوب و مشکلات بر سر ارتباط نه بدلیل مشکلات الگوریتمهای رمزنگاری بلکه بدلیل ساختاری که ارتباط براساس آن صورت گرفته است، باشد. پروتکل Yahalom یکی از پروتکلهای امن در احراز هویت است. در این مقاله به بررسی این پروتکل خواهیم پرداخت و توسط ابزار تخصصی بررسی مدل Scyther

میزان کارایی آنرا بررسی خواهیم کرد. نتایج بررسی حاکی از ضعف پروتکل در برابر حملات تکرار بود و سپس سعی شد که میزان موفقیت بهبود انجام گرفته برای برطرف کردن این ضعف بوسیله تغییر پیغام و اضافه کردن پیام (Hand Shake) توسط ابزار Scyther، بررسی شود. نتایج نشان دادند که بوسیله این بهبود، محدودیتهای پروتکل در برابر حملات تکرار و جعل هویت در Yahalom را میتوان

از بین برد. همچنین نتایج نشان خواهند داد که پروتکل توافق بر سر کلید را به خوبی پیاده میکند و کلید توزیع شده توسط سرور امن خواهد ماند.

کلید واژه- شبکه های کامپیوتری، پروتکل امنیتی Yahalom، ابزار Scyther، احراز هویت، محرمانگی

-1 مقدمه

پروتکلهای امنیتی مهمترین جز شبکه های امن محسوب میشوند.پروتکلهای احراز هویت روشهای دقیقی به منظور انجام کار احراز هویت و شناسایی افراد هستند. پروتکلهای احراز هویت روشهایی هستند که به رمزنگاری وابسته هستند و به طور خاص برای تضمین امنیت ارتباط استفاده میشوند.نیازمندی مهم دیگر این پروتکلها به منظور انجام کار احراز هویت ساختن یک مسیر امن بوسیله تبادل کلیدها بین طرفین ارتباط است.

بسیاری از پروتکهای احراز هویت مانند [1] Yahalom و کربروس
[2] و([3] Internet Key Exchange (IKEهمگی برای دستیابی

به دونیازمندی محرمانگی و احراز هویت استفاده میشوند.اگرچه طراحی این پروتکلها بسیار مشکل است زیرا دستیابی به این دونیازمندی مشکل است و مشکلات امنیتی پنهان دارند. به طور مثال در مقاله [1] به مشکلی در پروتکل Yahalom اشاره شده است که در آن این پروتکل نمیتواند در برابر حملات تکرار((Replay Attack مقاومت کند و پروتکل Ban-Yahalom

هم در برابر حملات جعل هویت (Impersonate Attack) شکست میخورد.

پروتکل Yahalom توسط [1] Yahalom با هدف احراز هویت دوطرف ارتباط بوسیله کلید جلسه توزیع شده از طریق سرور، طراحی شد.این پروتکل توسط [4]Gavin Lowe و [5] در سال 1998 و توسط [6] Paulson در سال 2001 بازبینی شد.در مرجع [7] سعی در بهبود این پروتکل شده .

در این مقاله سعی شده محرمانگی و احراز هویت این پروتکل بوسیله ابزار Scyther بررسی شده و میزان موفقیت بهینه سازی انجام شده توسط مرجع [7] برروی پروتکل Yahalom توسط ابزار Scyther مورد بررسی قرار گیرد.

در بخش 2 ابزار Scyther را شرح میدهیم. در بخش 3 پروتکل اصلی را توضیح میدهیم و مشکلات امنیتی آنرا شرح میدهیم.در بخش 4 پروتکل تغییر یافته را ارئه و آنرا از لحاظ امنیتی بررسی خواهیم کرد و در بخش 5 نتیجه گیری خواهیم داشت.

-2 ابزار Scyther

ابزار Scyther ابزاری است که به منظور بررسی صحت، خطایابی و آنالیز پروتکلهای امنیتی استفاده میشود.Scyther یک ابزار اتوماتیک چک کردن امنیت پروتکلها است که در شناسایی، خطایابی و آنالیز پروتکلهای امنیتی بسیار کارا عمل میکند.

Scyther میتواند از تکنیک جستجوی حالت سمبلیک عقبگرد

(Search backward symbolic state) برای آنالیز امنیت پروتکل
استفاده کند. تکنیک جستجوی عقبگرد از موتورArachne که بر پایه متد Athena پیاده سازی شده است، بهره میبرد. این روش با استفاده از ادعاهای امنیتی استفاده شده به صورت عقبگرد حملات را جستجو میکند.این تکنیک اجازه بررسی تمام و کمال معایب و جستجوی حالات متناهی از فضای حالات را میدهد.

این ابزار همچنین میتواند خصوصیات احراز هویت مانند هماهنگی (Synchronization) را شناسایی کند.هماهنگی به معنی آن است که پیامها دقیقا همانطور که در خصوصیات پروتکل قید شده اند منتقل شوند.یکی دیگر از امکانات Scyther توانایی در مدیریت کلیدهای با ساختار غیر اتمیک و کلیدهای چندگانه است.

Scyther بر پایه الگوریتمهای پالایش الگوها که باعث مختصر شدن کار شناسایی حالات نا محدود میشود، کار می کند.این الگوریتمها به ابزار اجازه میدهند که در انواع حملات و رفتارهای ممکنه، پروتکل را با بررسی درستی تعداد نامحدود جلسه بتواند بررسی کند.

ابزارScyther یک محیط گرافیکی فراهم میکند که از محیط خط فرمان و اسکریپتهای زبان Python بهره می برد.Scyther میتواند به تعداد نامحدودی جلسات را بررسی کند و خروجی خود را به شکل درختواره نمایش دهد ودر صورت یافتن حمله برای هر حمله گراف مربوط به آن را تولید و نمایش دهد و در صورتی که هیچ حمله ای یافت نشود اطلاع میدهد که نتوانسته در حالت محدود به نتیجه برسد.

ثانیا Scyther می تواند در آنالیز پروتکل بوسیله دسته بندی کردن رفتارهای پروتکل یا دسته بندی حملات به بررسی پروتکل ها بپردازد.

ثالثا Scyther امکان بررسی چند پروتکل را فراهم می کند.به این شکل که میتواند به بررسی ترکیبی دو پروتکل که درون یک پروتکل قرار دارند بپردازد.درScyther جزئیات پروتکلها به زبان SPDL پیاده سازی میشوند.((7

این ابزار میتواند به سه منظور استفاده گردد:
· بررسی صحت ادعاهای پروتکل

زبان ورودی برای Scyther اجازه تعیین خصوصیات امنیتی را به شکل ادعاها (claims) را میدهد.به عنوان مثال یک پروتکل میتواند ادعا کند که یک خصیصه محرمانه خواهد بود یا یک خصیصه برای طرفهای ارتباط به منظور احراز هویت استفاده میشود. Scyther میتواند این خصوصیات را بررسی کند یا عدم صحت آنرا اطلاع دهد.

· بررسی صحت ادعاهای اتوماتیک

اگر خصوصیات تعریف شده پروتکل شامل هیچ ادعایی نباشد، Scyther میتواند به طور اتوماتیک ادعاهایی را تولید کند.در آخر هرنقش ادعاهای احراز هویت اضافه شده و ادعا میکنند که طرفهای ارتباط در پروتکل آنطور که باید پیاده سازی شده اند وهمچنین ادعاهای امنیتی به منظور بررسی همه متغییرها و مقادیر تولید شده توسط پروتکل تولید میشوند.سپس ادعاهای تولید شده مانند حالت قبل بررسی میشوند.این روش، روشی سریعی برای بررسی خصوصیات یک پروتکل است.

· بررسی خصوصیات نقشها (Characterization)

در Scyther عاملها به صورت نقشهایی تعریف میشوند.برای بررسی پروتکل ،هر نقش در پروتکل میتواند شناسایی شود که این به معنای آن است که Scyther میتواند نقشهای موجود در پروتکل را دنبال کند و فعالیتهای آنها را بررسی کند و الگوهای ممکنه را به منظوریافتن مشکلات پروتکل دنبال کند.

ابزار Scyther برای پلتفرمهای windows وLinux و MacOS به

صورت آزاد و از طریق آدرس
http://people.inf.ethz.ch/cremersc/scyther در دسترس است.

در پروتکلهای امنیتی نیازمندیهای زیر باید برقرار باشند:

محرمانگی

محرمانگی که یکی از مهمترین خصوصیات پروتکلهای امنیتی است. این پروتکل از رمزنگاری متقارن برای ایجاد کلید جلسه استفاده می کند و نیاز از است که امنیت کلید اثبات شود وعدم فاش شدن کلید جلسه حتی در صورت دسترسی نفوذ کنندگان به کلید جلسه را تضمین میکند. بوسیله ادعای (1) میتوان عدم لو رفتن کلید جلسه را اثبات کرد.
(1) claim_I(I, Secret, Kir)
claim_R(R, Secret, Kir)

احراز هویت هدف احراز هویت شناسایی طرفین ارتباط و اطمینان از هویت آنهاست.

در اینجا بوسیله ادعاهای زیر هویت فرستنده و گیرنده پیام را تضمین میکنیم:

:Nisynch به معنی آن است که پیامهای ارسال شده از سمت طرفین توسط محاجم قابل رمزگشایی و ارسال دوباره نباشند و هر بار ارسال پیام توسط فرستنده برابر با دریافت پیام توسط گیرنده باشد. پروتکلهایی که Synchronies هستند میتوانند در برابر حملاتReplay مقاومت کنند. در این حملات محاجم بسته های خود را درون شبکه ارسال میکند بدون آنکه طرفین ارتباط از وجود محاجم باخبر باشند. [9] بوسیله ادعای (2) میتوان این موضوع را بررسی کرد.

(2) claim_I(I , Nisynch)
claim_R(R, Nisynch)

:Alive تضمین حفظ ترتیب انجام مراحل پروتکل بوسیله طرفین ارتباط را انجام میدهد. بوسیله این خصوصیت اثبات میکنیم که نفوذگر نمیتواند با ارسال دوباره پیام به فرستنده آن پروتکل را مختل کند. [10] بوسیله ادعای (3) میتوان این موضوع را بررسی کرد.

(3) claim_ I(I, Alive)
claim_R(R, Alive)

:Weakagree تضمین آنکه گیرنده پیام ،در زمان ارسال پیام توسط فرستنده آنرا دریافت کند. یک پروتکل ممکن است Alive باشد ولی Weakagree نباشد. بوسیله این خصوصیت نفوذگر نمیتواند خود را به عنوان فرستنده و یا گیرنده پیام معرفی کند.

[10]

( نفوذگر نمیتواند خود را برای فرستنده (I) ،گیرنده (R) و برای گیرنده (R)، فرستنده (I) معرفی کند. ) بوسیله ادعای (4) میتوان این موضوع را بررسی کرد.

(4) claim_I(I, Weakagree)
claim_R(R, Weakagree)

-3 مدلسازی و آنالیز پروتکل Yahalom

پروتکل :Yahalom این پروتکل ،یک پروتکل توزیع کلید است که همچنین کار احراز هویت را هم انجام میدهد. این پروتکل یک سیستم کلید مشترک را در نظر میگیرد و یک کلید اصلی با طرف مورد اعتماد و سرور توزیع کلید را به اشتراک میگذارد. پروتکل Yahalom به صورت روند (5) است:

(1) I - > R : I, Ni
( 2) R - > S : R, {I, Ni , Nr }Krs (3) S -> I ： {R, Kir, Ni , Nr } Kis, {I , Kir } Krs (4) I -> R ： {I, Kir } Krs, { Nr } Kir (5)

همانطور که در شکل 1 آمده در پروتکل Yahalom، I را به عنوان آغازکننده با نام "Alice" و شرکت کننده دیگر R که با نام "Bob" شناخته میشود را داریم. در آغاز Alice و Bob بترتیب کلیدهایKis وKrs را به ترتیب با سرور "S" به اشتراک میگذارند. Alice ابتدا شناسه خود (I) را به همراه عددی تصادفی (Nonce) را به Bob میفرستد. در پیغام بعدی Bob شناسه خود و یک قسمت رمز شده {I, Ni, Nr} Krsرا که در آن Nr عدد تصادفی Bob است را به سرور S ارسال میکند. در پیغام سوم

سرورS به Alice دو قسمت رمز شده {R, Kir, Ni,Nr }Kis و {I
, Kir}Krs را میفرستد. در قسمت رمز شده اول به Alice میگوید که Kir یک کلید نشست خوب برای ارتباط با Bob است و همچنین میگوید که Nr عدد تصادفی Bob است. قسمت رمزشده را به Bob ارسال میکند(بوسیله Nrای که توسط Kir رمزشده). Bob قسمت رمزشده اول را با Kir ای که گرفته باز میکند و آنرا برای رمزگشایی قسمت رمزشده دوم استفاده میکند اگر رمزگشایی دوم Nr خودش را به آن بدهد که نشان دهنده درستی Kir است و Kir یک کلید نشست خوب برای ارتباط با Alice است.

3