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