کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
9952281 1444316 2018 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Formal analysis of a security protocol for e-passports based on rewrite theory specifications
ترجمه فارسی عنوان
تجزیه و تحلیل رسمی یک پروتکل امنیتی برای پاسپورت الکترونیکی بر اساس مشخصات تئوری بازنویسی
کلمات کلیدی
احراز هویت، گذرنامه الکترونیکی، مبادله کلیدی، مادرم، چک کردن مدل، بازنویسی، 00-01، 99-00،
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر شبکه های کامپیوتری و ارتباطات
چکیده انگلیسی
We report on a case study in which Password Authentication Connection Establishment (PACE) protocol has been formally analyzed based on its rewrite theory specification with Maude, a rewriting logic-based computer language and system. Dominik Klein has formally verified with interactive theorem proving that PACE enjoys the key secrecy property under the condition that the password shared by a passport chip C and a terminal T would be never leaked to the third party. In contrast, our analysis supposes that the password is leaked to an intruder once it has been used in a session completed. Under the condition, the analysis unveils some security weakness that PACE does not enjoy the correspondence (or authentication or agreement) properties from both C and T points of view. Then, we propose that one-time password is used in PACE. We have formally analyzed that the revised version enjoys the correspondence properties under the latter condition. We have used the Maude search command that can be used to conduct reachability analysis because the correspondence properties can be formalized as invariant properties.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Information Security and Applications - Volume 42, October 2018, Pages 71-86
نویسندگان
, , ,