تحلیل صوری ویژگی وارسی پذیری میکس نت با استفاده از حساب پی کاربردی

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

کلیدواژه ها:

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