Formale Modellierung von Authentifizierung und Authorisierung infrastrukturen: Authentizität von deskriptiven Attributen und Privilegien auf der Basis digitaler Zertifikate

برنامه‌های رایانه‌ای مدرن که از یک شبکه باز مانند اینترنت استفاده می‌کنند، به امضای دیجیتالی قابل اعتماد، رمزگذاری و روش‌های مجوز نیاز دارند. مدل‌های رسمی قبلی بر زیرساخت‌های کلید عمومی تمرکز می‌کنند و اعتبار کلیدهای عمومی رمزنگاری در مرکز قرار می‌گیرد. با این حال، ابطال و مدت اعتبار گواهی های دیجیتال نادیده گرفته شده است.

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

Moderne Computeranwendungen, die ein offenes Netz wie das Internet nutzen, benötigen zuverlässige Methoden zur digitalen Signatur, zur Verschlüsselung und zur Autorisierung. Bisherige formale Modelle konzentrieren sich auf Public-Key-Infrastrukturen, wobei die Authentizität kryptographischer öffentlicher Schlüssel im Mittelpunkt steht. Rückruf und Gültigkeitsdauer digitaler Zertifikate werden jedoch vernachlässigt.

Thomas Wölfls Modell umfasst diese zeitlichen Aspekte und ermöglicht erstmals neben der Herleitung von Schlüsselauthentizität auch die Ableitung von Attributauthentizität. So kann die Echtheit von Zugriffsprivilegien und deskriptiven Attributen (z. B. biometrische Referenzmuster, organisatorische Rollen und Haftungserklärungen) für einen bestimmten Zeitpunkt formal bewiesen werden. Das vom Autor entwickelte PROLOG-Programm realisiert eine automatisierte Ableitung, liefert nachweislich korrekte Ergebnisse und terminiert. Die prädikatenlogischen Formeln des Modells sind widerspruchsfrei, sofern keine Rückrufschleife vorliegt.