بخشی از مقاله
*** این فایل شامل تعدادی فرمول می باشد و در سایت قابل نمایش نیست ***
آنالیز پروتکل تصدیق هویت متقابل EBH توسط منطق BAN
چکیده
سیستم شناسایی از طریق امواج رادیویی ، یکی از فناوریهای محاسباتی فراگیر میباشد که وجود مزایای فراوان آن، باعث گردیده است تا جایگزین سایر فناوری های شناسایی خودکار گردد. با این وجود، این فناوری دارای آسیب پذیری های ذاتی بوده و در معرض طيف گسترده ای از تهدیدات امنیتی می باشد. تا کنون پروتکل های تصدیق هویت زیادی در رابطه با امنیت و محرمانگی سیستم شناسایی با امواج رادیویی، ارائه گردیده است، اما متأسفانه بیشتر آنها برخلاف ادعایشان، انتظارات امنیتی لازم را برآورده نکرده اند. با توجه به بررسی های صورت گرفته روی پروتکل ها، این نتیجه حاصل شد که پروتکل تصدیق هویت متقابل Eslamnezhad , Badihiyeh ) EBH Aghdam , Hosseinzadeh ، ۲۰۱۱)، نسبت به پروتکل های دیگر نه تنها از امنیت بیشتری برخوردار می باشد، بلکه دارای کارایی بالایی بوده و سریع نیز میباشد.
احتیاج ضروری برای اثبات نتایج امنیتی ادعا شده ی این پروتکل باعث گردید تا در این مقاله، امنیت این پروتکل به صورت ساختار یافته، مورد بررسی واقع شود. لذا از میان منطقهای معتبری که برای ارزیابی پروتکل های تصدیق هویت وجود دارد، منطق BAN به دلیل قدرتمند بودن و بیان ساده، به عنوان ابزاری مهم برای بررسی ساختاریافته ی امنیت پروتکل مذکور استفاده گردید. در حقیقت توسط منطق BAN، پروتکل تصدیق هویت EBH با در نظر گرفتن تمام فرضیات اولیه اش به صورت گام به گام توصیف گردید و ملاحظه شد که پروتکل پیشنهادی توانسته نگرانی های امنیتی و محرمانگی موجود در سیستم شناسایی از طریق امواج رادیویی را برطرف نماید
واژه های کلیدی :
منطق BAN، سیستم شناسایی از طریق امواج رادیویی، تهدید امنیتی، تصدیق هویت، امنیت .
۱- مقدمه
در زمینه ی پروتکل های امنیتی در سیستم شناسایی از طریق امواج رادیویی، تحقیقات زیادی انجام گرفته است که هریک در راستای ایمن کردن سیستم در برابر تهدیدات ممکن ۱۱-۶]، می باشد. در مقاله ی قبلی، پروتکل تصدیق هویت دو طرفهی جدیدی برای سیستم های شناسایی از طریق امواج رادیویی، با در نظر گرفتن محدود بودن امکانات موجود در برچسب ها و همچنین کاهش کارایی سیستم در هنگام بروز انبوه درخواست های تصدیق هویت، ارائه گردید [۷]. از این پس برای سهولت، این پروتکل با حروف اول نویسندگانش، به نام EBH مشخص می گردد. طبق ادعای پروتکل EBH، این پروتکل توانست نقاط ضعف امنیتی موجود در پروتکل های قبلی یعنی پروتکل های HM ، OSK ، WSREو Tsu [ ۸، ۹ ، ۱۰ ، ۱۱ ] را بر طرف نماید. بنابراین لازم آمد امنیت این پروتکل به صورت ساختار یافته، تحلیل و اثبات گردد.
جهت بررسی امنیت پروتکل های تصدیق هویت، روشهای مختلفی وجود دارد که از بین آنها، منطق BAN [۱۲] مطمئن ترین و پرکاربردترین روشی است که در اکثر کارهای تحقیقاتی، جهت بررسی امنیت پروتکل ها مورد استفاده قرار می گیرد و لذا در این مقاله از این منطق، جهت آنالیز امنیت پروتکل مذکور بهره خواهیم برد. بنابراین در ساختار این مقاله، ابتدا منطق BAN، نمادها، قوانین مربوطه و مراحل آنالیز توسط این منطق توصیف می گردد و سپس پروتکل EBH شرح داده شده و مراحل آنالیز پروتکل توسط منطق BAN نشان داده میشود. در پایان مقاله، مقایسه ای بین این مقاله با یکی از کارهای مشابه انجام شده در زمینه ی امنیت پروتکل های تصدیق هویت سیستم شناسایی از طریق امواج رادیویی [۱۳]، انجام می گیرد.
٢- منطق BAN [۱۲] نام BAN ترکیب اسامی نویسندگان این منطق يعنی ,Burrows) ( Abadi , Needham می باشد. منطق BAN یکی از ابزارهای مهم برای بررسی ساختاریافته ی پروتکل های امنیتی می باشد تا بتوان به این طریق از امنیت پروتکل ها اطمینان حاصل نمود. در این منطق، پیام های ارسالی و دریافتی در پروتکل با سه دسته علائم نمایش داده میشود که عبارتند از علائم مربوط به بخش های اصلی، رمزهای مشترک بین بخش های اصلی و نمادهای مربوط به روابط منطقی. بایستی توجه داشت که بخش های اصلی، مبدأ و مقصد پیام های ارسالی می باشند که برای این پروتکل، شامل برچسب و برچسب خوان می گردند. این منطق براساس روابط و قوانین منطقی می باشد. اگرچه منطقهای معتبر دیگری نیز برای ارزیابی پروتکل های تصدیق هویت وجود دارد ولی به دلیل قدرتمند بودن و بیان ساده ی منطق BAN، در این مقاله از آن برای ارزیابی امنیتی پروتکل پیشنهادی استفاده گردیده است. برای شناخت بهتر روابط بین بخش ها، نمادهای مربوط به آنها تعریف شده است و در ادامه قوانین منطقی و مراحل آنالیز پروتکل تصدیق هویت برای سیستم های شناسایی از طریق امواج رادیویی شرح داده میشود.
۱ - ۲- نمادهای مربوط به روابط در منطق BAN [۱۲]
در منطق BAN از نمادها و ساختارهای ذیل برای نشان دادن روابط منطقی استفاده می گردد (Burrows و همکاران، ۱۹۹۰):
:بخش اصلی p پیام X را باور دارد. به این معنی که بخش اصلی p در صورتی عمل می نماید که پیام x صحیح باشد. در حقیقت، این رابطه قلب منطق BAN می باشد.
بخش اصلی P، پیام X را می بیند. مثلا P پیامی حاوی مقدار XP را دریافت می کند.
بخش اصلی P یکبار پیام X را ارسال کرده است ولی مشخص نیست در چه زمانی
: بخش اصلی P بر پیام X صلاحیت و قدرت قانونی دارد. مثلا P
P به توانایی سرور در تولید و ارسال امن کلید مشترک X اعتقاد دارد.
: پیام X جدید است. X به جز در فرایند جاری پروتکل در هیچ زمان قبلی ارسال نشده است.
برای ارتباطات خود از کلید مشترک K استفاده می کنند.
: کلید عمومیP است. کلید خصوصی مطابق با این کلید، با 'K نشان داده میشود.
یک رمز است که تنها توسط P و Q شناخته میشود. این پیام محرمانهی مشترک، همانند کلمه عبور، بین آنها به اشتراک گذاشته شده است تا بتوانند هویت همدیگر را تصدیق نمایند.
این ساختار نشان دهنده این است که عبارت X توسط کلید k رمزگذاری شده است
نشان میدهد که عبارت X با y ترکیب شده است که در آن y یک پیام محرمانه می باشد.
۲ - ۲ - قوانین اصلی در منطق BAN [۱۲]
در این بخش، از میان قوانین منطقی موجود در منطق BAN، آن دسته که برای اثبات امنیت پروتکل تصدیق هویت EBH به کار رفته است، توضیح داده میشود (Burrows و همکاران، ۱۹۹۰).
(۱) قانون مفهوم پیام: این قانون بیان ریاضی این مطلب است که اگر بخش اصلی P باور داشته باشد که پیام محرمانه k را با بخش Q به اشتراک دارد و پیام X را در حالی که با k ترکیب شده، دریافت کند، به این باور خواهد رسید که بخش Q زمانی پیام X را فرستاده است.
(۲) قانون تأیید: اگر بخش اصلی P باور داشته باشد که پیام X تازه است و بداند که زمانی بخش Q آن را فرستاده، به این باور می رسد که بخش Q هم پیام X را در همین زمان باور دارد.
و (۳) قانون هشینگ: یا اگر بخش اصلیP باور داشته باشد که بخش اصلی Q تابع هشی از چندین پیام را فرستاده، بطوریکه خود P تک تک این پیام ها را به طور جداگانه دریافت نموده باشد، به این باور می رسد که بخش Q آن پیام ها را فرستاده است.
(۴) قانون مربوط به عملگر تازگی: اگر بخش اصلی P باور داشته باشد که بخشی از یک پیام تازه است، به این باور می رسد که کل پیام تازه می باشد.
(۵) قانون مربوط به عملگر باور در بخش اصلی P باور داشته باشد که بخش اصلی مجموعه ای از پیامها را باور دارد، P به این باور خواهد رسید که بخش Q به تک تک پیام ها به طور جداگانه نیز باور دارد.
3- آنالیز پروتکل در منطق BAN آنالیز پروتکل در منطق BAN طی چهار مرحله انجام می پذیرد که عبارتند از: ایده آل سازی پروتکل، در نظر گرفتن فرضیات اولیه، تعیین هدف آنالیز و اعمال قوانین منطقی روی فرضیات اولیه تا زمان اثبات نمودن هدف از پیش تعیین شده.
در ادامه ی مقاله، بعد از تشریح پروتکل تصدیق هویت EBH، هر یک از این مراحل آنالیز برای این پروتکل شرح داده میشود.
۴- پروتکل تصديق هویت متقابل EBH [۷] مسئله ی مهمی که در پروتکل های تصدیق هویت دیگر [ ۸، ۹ ، ۱۰ ، ۱۱ ] برای سیستم شناسایی با امواج رادیویی وجود داشت، عدم توجه به بار محاسباتی اعمال شده به پایگاه داده در هر بار فرایند تصدیق هویت بود. باید توجه داشت که هزینه ی جستجوی مقدار هش شده از جدول مقادیر در پایگاه داده برای تصدیق هویت هر برچسب برابر (O ( n میباشد که این مسئله می تواند کارایی سیستم را هنگامی که تعداد زیادی برچسب باید تصدیق هویت شوند، به شدت افزایش دهد. این پروتکل، ضمن برطرف کردن نگرانی های امنیتی، مشکل بار اعمالی به برچسب خوان و پایگاه داده را نیز برطرف نموده است.
۱ - ۴- علائم به کار رفته در این پروتکل
K: رمز مشترک بین برچسب خوان و تمام برچسبها می باشد.
r: متغیر تصادفی مشترک در بین برچسب خوان و تمام برچسبها می باشد.
X: نشان دهنده مقدار قدیم یا جدید می باشد.
آخرین مقدار مهر زمانی، که در انتهای فرایند تصديق هویت برچسب، در آن ذخیره می شود.
مقدار مهر زمانی فعلی میباشد. TSold: مقدار قدیمی مهر زمانی که در برچسب خوان ذخیره شده
است.
مقدار جدید مهر زمانی که در برچسب خوان ذخیره شده است.
بیشترین مقدار مجاز برای مهر زمانی می باشد.
آدرس مربوط به رکورد مرتبط با هر برچسب میباشد. در هر رکورد اطلاعات برای برچسب مربوطه، نگهداری میشود.
D: شماره شناسایی منحصر به فرد مربوط به هر برچسب می باشد. در برچسب اطلاعات در پایگاه داده اطلاعات نگهداری میشود.
۲ - ۴ - دو فاز تشکیل دهنده ی این پروتکل ۱) فاز مقدار دهی اولیه: در این مرحله که توسط سازنده انجام می گردد، رمز مشترک k، متغیر تصادفی r و همچنین یک مقدار اولیه مهر زمانی در بین برچسب و برچسب خوان به اشتراک گذاشته میشود.
۲) فاز تصدیق هویت: مراحل چهارگانه این فاز در شکل (۱) نشان داده شده است و در ادامه این مراحل شرح داده میشوند. گام اول - برچسب خوان به برچسب: برچسب خوان مقدار مهر زمانی را تولید و را محاسبه نموده و به عنوان درخواست تصدیق هویت آنها را به برچسب ارسال می کند.
گام دوم - برچسب به برچسب خوان: برچسب، مهر زمانی را بررسی می کند. اگر این مهر زمانی از مهر زمانی قبلی کوچک تر باشد یا از TSmax بزرگ تر باشد، عمل تصدیق هویت متوقف می شود. در غیر این صورت، برچسب 'TS دریافتی را با مقدار رمز k و متغیر تصادفی r، هش نموده و حاصل را با مقدار دریافت شده مقایسه می نماید. در صورت برابر بودن این دو مقدار، برچسب یک مقدار هش را با استفاده از مهر زمانی دریافتی از برچسب خوان، شناسه برچسب، رمز kو مهر زمانی موجود در خود، تولید می کند و آن را به همراه آدرس برچسب که با مقدار هش شده مهر زمانی دریافتی و متغیر تصادفی Xor
،r شده است، به برچسب خوان ارسال می کند.
گام سوم - برچسب خوان به برچسب: برچسب خوان آدرس رکورد مربوط به برچسب در پایگاه داده اش را، از رابطه ی ( به دست می آورد. با استفاده از مقادیر رکورد برچسب، را محاسبه، و با مقدار U دریافتی از برچسب مقایسه می کند. اگر هیچ یک از مقادیر تولید شده با U برابر نباشد فرایند تصديق هویت قطع می شود و برچسب غیرقانونی تشخیص داده میشود. در غیر این صورت با توجه به اینکه کدام یک از مقادیر تولید شده با U برابر است به X مقدار old یا new اختصاص داده میشود. مقدار new بیانگر این است که فرایند تصديق هویت برچسب در مرحله قبل به صورت کامل صورت پذیرفته است و مقدار ldه نشان دهنده این است که پیغام A در فرآیند تصدیق هویت قبلی برچسب، یا گم شده و یا اینکه به وسیله افراد سودجو از رسیدن آن به برچسب جلوگیری شده است. در ادامه اگر X = new باشد، برچسب خوان مقدار TSold را با TSnew و مقدار به روز رسانی می کند؛ در غیر این صورت فقط مقدار TSnewرا با "TS به روز رسانی می کند. در آخر مقدار را به عنوان تصدیق هویت برچسب تولید و آن را در پیام A، به برچسب ارسال می نماید.
گام چهارم: برچسب مقداررا تولید می کند و با مقدار دریافتی از برچسب خوان مقایسه می کند، در صورت برابر بودن، مقدار TS را با 'TS به روز رسانی می کند.
۵- بررسی امنیت پروتکل EBH
در این قسمت امنیت پروتکل EBH، مورد ارزیابی قرار می گیرد. حمله ی محرمانگی: از آنجایی که در پروتکل پیشنهادی از تابع هشینگ برای ارسال شماره شناسه و کلیدهای رمز مشترک استفاده میشود عملا امکان دسترسی تهدید گران به این اطلاعات غیرممکن است. در نتیجه این حمله ی امنیت مکان: با توجه به اینکه مقادير ID و AR ارسالی توسط برچسب با استفاده از تابع هشینگ و مقادیر مهر زمانی، رمز مشترک و عدد تصادفی پوشش داده می شود، بنابر این، تهديدگر نمی تواند توسط شنود داده های ارسالی از برچسب، موقعیت برچسب را شناسایی کند. در نتیجه می توان گفت که این پروتکل در برابر حمله تشخیص موقعیت، ایمن می باشد.
حمله ی تکرار: با توجه به اینکه در پروتکل EBH، برچسب خوان در هربار خواندن برچسب، مهر زمانی را به روزرسانی می نماید، در نتیجه حتی اگر تهدید گر بتواند به داده های ارسالی از برچسب دسترسی یابد، در تصدیق هویت بعدی، به دلیل به روز نبودن مهر زمانی نمی تواند اطلاعات را مجددا در غیاب برچسب قانونی به برچسب خوان ارسال کند. برچسب، مهر زمانی ارسال شده از برچسب خوان را بررسی می کند و اگر این مهر زمانی از مهر زمانی قبلی کوچکتر باشد یا اینکه از بزرگتر باشد، برچسب درخواست تصدیق هویت را غیر مجاز دانسته و ارتباطی بین آنها صورت نمی گیرد.
حملهی انکار سرویس: برچسب خوان همواره مقدار قبلی مهر زمانی را نگه می دارد. حتی اگر به هر دلیلی از ارسال A جلوگیری گردد و برچسب نتواند TS خود را به روز رسانی نماید، با توجه به اینکه برچسب خوان را در خود نگه می دارد، مانع از بروز غیر همزمانی بین برچسب خوان و برچسب می گردد؛ بدین ترتیب که اگر برچسب در واکنش به درخواست برچسب خوان، مهر زمانی به روز رسانی نشده را ارسال نماید، برچسب خوان با فرض اینکه فرایند تصدیق هویت برچسب در مرحله قبلی به صورت کامل انجام نپذیرفته، با استفاده از ، هویت برچسب را تصدیق می کند و فقط را به روز رسانی می نماید ولی مقدار را تغییر نمیدهد. در نتیجه مانع از ایجاد حمله انکار سرویس می گردد. حمله ی جعل هویت: تهدید گر برای اینکه بتواند هویت برچسب را به طور کامل جعل نماید نیازمند به دست آوردن شماره شناسه و مهر زمانی و دیگر داده های محرمانهی برچسب می باشد. با توجه به اینکه این مقادیر توسط تابع هشینگ و همچنین رمزهای مشترک K و r محافظت می شود، در نتیجه تهدید گر عملا قادر به یافتن این مقادیر نمی باشد. حتی اگر تهدیدگر بتواند از طریق شنود ارتباط بین برچسب و برچسب خوان، مقدار مهر زمانی را به دست آورد، به دلیل اینکه به مقادیر r،K و ID دسترسی ندارد، نمی تواند هویت برچسب را جعل نماید.
۶- آنالیز پروتکل EBH در منطق BAN
به منظور آنالیز این پروتکل در منطق BAN، همان چهار مرحلهی بیان شده را به ترتیب انجام میدهیم.
۱ - ۶- مرحله ی نخست:
ایده آل سازی پروتکل در این مرحله، پیامهای رمزنگاری نشده از پروتکل پیشنهادی حذف می گردند تا پروتکل به شکل ایده آل در آید، مطابق با آنچه در شکل (۲) دیده میشود. برچسب خوان با R و برچسب با T نشان داده شده است و پیام رمزنگاری نشدهی 'TS از پروتکل حذف می گردد.
۲ - ۶ - مرحله ی دوم:
فرضيات اولیه در این مرحله با استفاده از نمادهای منطق BAN، فرضيات اولیه پروتکل EBH نشان داده میشود.
۳ - ۶ - مرحله ی سوم، تعیین اهداف امنیتی
در مورد اینکه چه چیزی باید به عنوان اهداف پروتکل های تصدیق هویت در نظر گرفته شود، تا نتایج مطلوبی حاصل گردد، نظريات زیادی وجود دارد. در اغلب پروتکل ها، ارتباطات به وسیله ی کلیدها و رمزهای به اشتراک گذاشته شده، حفاظت می شوند. بنابر این فرایند تصدیق هویت را زمانی می توان کامل دانست که کلید یا رمزی همانند k در بین بخش های اصلی A و B وجود داشته باشد و بتوان نتایج را کسب نمود. همچنین برخی از پروتکل های تصدیق می توانند چیزی فراتر از این اهداف را نیز تضمین کرده و نتایج کسب شوند. بنابر این، بر این اساس، اهداف پروتکل پیشنهادی شامل موارد ذیل می گردد.
