Skip to main content
SUPERVISOR
Mohamadreza Raofi,Mojtaba Aghaei
محمد رضا رئوفی (استاد مشاور) مجتبی آقائی فروشانی (استاد راهنما)
 
STUDENT
Mohammad Sobhanian
محمد سبحانیان

FACULTY - DEPARTMENT

دانشکده ریاضی
DEGREE
Master of Science (MSc)
YEAR
1387

TITLE

Permission to Speak: A Logic for Access Control and Conformance
In this thesis we consider access control logics and checking conformance for regulatory documents, together. In chapter 3, operator says is represented with notion “saying” for access control. Here, says is a modal with the system K , and it is idempotent, commutative, and associative. In chapter 5, regulatory conformance is considered. There is a system with some principals and predicates, and many laws. There is maybe a body of regulations that has complex reference. A system has conformance if obligations are satisfied. The conformance checking needs reasoning for determining obligations. This reasoning is non-monotonic and for a state of predicates, and a body of regulations might have several possible worlds. There is an algorithm for computing these possible worlds, and these possible worlds are called fixed points; because they are arose from using an inflationary function, and these possible worlds are its fixed points. In chapter 6, an interaction between “saying” and formalization of regulatory documents is expressed. There is an axiomatize for this interaction and its reasoning. Its semantics is upon Kripke’s semantics. This logic is called “Permission to Speak” and for it, theorems “soundness”, “completeness”, and “decidability” are proved. In this thesis, we consider “Paradox of the Court” that is between Protagors and his student Euathlus. We try to study this paradox in this approach, by our formalization in this logic (Permission to Speak). It seems that this logic can be equipped with quantification over formulas in future works for giving a better formalization for this paradox.
در این پایان نامه به صورت بندی و بیان یک سیستم استنتاجی برای یک منطق کنترل دسترسی پرداخته ایم که هم برای کنترل دسترسی و هم برای بررسی تطابق با قوانین مفید است. این سیستم منطقی قابلیت بیان سیستم های کنترل دسترسی، به عنوان یک دستگاه حقوقی و قانونی را دارد. نخست عملگر says ، از منطق های کنترل دسترسی را مورد توجه قرار داده ایم. عملگر says مفهوم «گفتن» به عنوان یک وجه در منطق موجهاتی بیان می شود. در این دیدگاه عملگر says مفهوم «گفتن» را به صورت شهودی مدل سازی می کند. سپس با بیان آن براساس حساب لاندای نوع دار، نشان داده شده که سیستم استنتاجی شهودگرایانه، بر استدلال بر محرمانگی، با توجه به سطوح محرمانگی، مطابقت دارد. برای عملگر says سه تعبیر درخواست، تأیید و اعلان معرفی شده است. از جمله مفاهیم مهمی که با استفاده از عملگر says قابل بیان است، وکالت و نقل قول هستند. سپس عملگر says را با بردن به سیستم های حقوقی تکمیل کرده و به آن امکان داده شده که بنا به کاربرد آن در جمله تعبیر شود. سیستم های حقوقی برای بیان و صورت بندی قوانین و بیان سیستم استنتاجی مربوط به آن ارائه شده اند. سیستم های حقوقی به علت پیچیدگی های خاص خود، ما را به سیستم های استنتاجی غیر یکنوا راهنمایی می کنند. در این پایان نامه سیستم استنتاجی مورد نظر را به تفصیل بیان کرده ایم که با استفاده از ارزش نامشخص برای برخی جملات، توانمند شده است. در سیستم های استنتاجی غیریکنوا ممکن است از یک مجموعه فرضیات، چند جواب بدست آید. علاوه بر این در «اجازه سخن گفتن» با استفاده از وظایف تودرتو توانسته ایم قابلیت های زبانی بالایی را در اختیار بگیریم. در انی منطق «وظیفه» و «مجوز» به عنوان دوگان یکدیگر معرفی شده اند و این ساختار زبانی و استنتاجی به زبان و استنتاج معمولی بشری بسیار نزدیک است. با بیان چند مثال، قابلیت های زبانی و استنتاجی ارائه شده را تشریح کرده و در نهایت با بیان و بررسی پارادکس پروتاگوراس نشان داده ایم که سیستم معرفی شده قابلیت بررسی سیستم های حقوقی پیچیده را نیز دارد. در این پایان نامه به ارائه یک سیستم منطقی به همراه اصول موصوعه مناسب آن پرداخته شده که با مدل های کریپکی معناشناسی شده و برای آن قضایای سلامت، تمامیت و تصمیم پذیری نیز اثبات شده و با استفاده از زیرفرمول ها تصمیم پذیری بررسی هماهنگی با قوانین، برای یک سیستم، اثبات شده است. رده بندی موضوی : 03B45 و 03B70.

ارتقاء امنیت وب با وف بومی