A procedure for deciding symbolic equivalence between sets of constraint systems

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