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