چكيده
چكيده
ماشين‌هاي خودپرداز بانكي، ارائه سرويس¬هاي بانكي را در همه زمان¬ها و مكان¬ها براي مشتريان فراهم مي¬كنند. علاوه بر اين، بانك¬ها فقط يك‌بار هزينه خريد و راه¬اندازي اين ماشين¬ها را متحمل شده ولي مدت¬ها از منافع آن از قبيل: استخدام كاركنان كمتر، كاهش ارباب‌رجوع و رضايت مشتري¬ها بهره¬مند مي-گردند. با اين وجود، استفاده از خودپردازهاي بانكي چالش¬هايي را نيز با خود به همراه داشته است، به عنوان مثال اطمينان از امنيت تراكنش¬هاي بانكي انجام شده يكي از مشكلات پيش روي بانك¬ها است. به‌منظور تأمين امنيت تراكنش¬هاي بانكي، بانك¬ها بايد سرويس¬هاي امنيتي همچون محرمانگي اطلاعات، احراز هويت، اصالت پيام و غيره را فراهم آورند. براي ارائه اين سرويس¬ها، بانك¬ها بايد پروتكل¬هاي امنيتي طراحي كرده و از صحت آن‌ها اطمينان حاصل نمايند.
در اين پايان¬نامه، صحت سه پروتكل¬ امنيتي كه براي انجام تراكنش¬هاي بانكي پيشنهاد شده¬اند، با استفاده از ابزار Casper/FDR به صورت صوري مورد وارسي قرار گرفته¬اند. از سه پروتكل بررسي شده، يكي از پروتكل¬ها پيشنهادي است. در گام نخست، پروتكل اول با استفاده از ابزار Casper كامپايل شده و سپس با استفاده از بررسي كننده مدل FDR، امنيت اين پروتكل مورد بررسي قرار گرفته است. در گام آخر، نشان داده شده است كه اين پروتكل ويژگي‌هاي امنيتي همچون محرمانگي پيام¬ها و احراز هويت را تأمين نمي-كند. به صورت مشابه، امنيت پروتكل دوم وارسي شده و نشان داده شده است كه گرچه اين پروتكل سرويس¬هاي امنيتي مورد نياز را تأمين مي¬كند اما كامل نيست چرا كه موجوديت بانك را در نظر نمي-گيرد.
در نهايت، پروتكل پيشنهادي كه تركيبي از دو پروتكل مذكور است، از لحاظ امنيت با استفاده از ابزار Casper/FDR مورد وارسي قرار گرفته است. همچنين نشان داده شده است كه اين پروتكل نيازمندي¬هاي امنيتي محرمانگي اطلاعات، احراز هويت موجوديت¬ها و اصالت پيام¬ها را برآورده مي¬سازد، بنابراين مي¬تواند به عنوان يك پروتكل پايه به طراحي پروتكل¬هاي بهينه براي تأمين تراكنش¬هاي بانكي از طريق خودپرداز كمك كند.
واژه‌هاي كليدي: خودپردازهاي بانكي، پروتكل¬هاي امنيتي، وارسي صوري، Casper/FDR.
