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

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

میکس نت، وارسی پذیری، روشهای صوری، حسابهای پی کاربردی، میلی میکس