A Formal Framework for Security Analysis of NFC Mobile Coupon Protocols by Ali Alshahri

علي الشهري: بسم الله الرحمن الرحيم هذا ملخص لورقتي العلمية بعنوان A Formal Framework for Security Analysis of NFC Mobile Coupon Protocols و التي بفضل الله تم قبولها مؤخرا بمجلة Journal of Computer Security والتي تعتبر من أرقى المجلات العلمية في أمن المعلومات. واستغرقت حوالي السنة من التعديلات و المراجعات. ———مقدمة——— ———- لفهم الموضوع بالشكل الامثل نحتاج لفهم موضوعين رئيسين وهما أمن البروتوكولات التشفيرية و تقنية NFC: 1- امن البروتوكوات التشفيرية: الهجوم ضد التشفير اما ان يكون : – أ-ضد اللوغارثم التشفيري نفسه – ب -او الهجوم ضد البروتوكول التشفيري Security Protocol(بمعنى الطريقة التي تم استخدام التشفير بها في الرسائل الواردة و الصادرة). الورقة تتحدث عن النوع الثاني وهو الهجوم ضد البروتوكولات التشفيرية والتي تفترض ان اللوغارثم غير قابل للكسر وان المتطفل (الهكر) لديه تحكم كامل بالشبكة (ارسال / اعتراض /– ايقاف /– اعادة ارسال الرسائل) لكن لا يستطيع فتح رسالة بدون المفتاح التشفيري اللازم. و الاختبار يكون ان يقوم المتطفل باختراق المتطلبات الامنية للبروتوكول بهذة الشروط المقيدة. ويكون هذا عادة من خلال التحليل الرياضي للبروتوكول Security Protocol Verification. و هو علم مستقل بحد ذاته. 2- تقنية الاتصالات قريبة المدى NFC : تقنية الاتصالات قريبة المدى هي تقنية تسمح للاجهزة الذكية (جوالات، الايباد،..الخ) بالتواصل مع بعضها بمجرد الملامسة. والاشهر تكون في الجوالات لتكون قناة لعمليات الدفع من محفظة الجوال مثل: Apple Pay & Google wallet وهذا فيديو يوضح بعض تطبيقات هذه التقنية (مرفق) ———ملخص الورقة——— ——— هذه الورقة قامت بتحليل أحد اهم التطبيقات في هذه التقنية وهي الكوبونات Coupon او قسائم الشراء و التسويق. حيث قام بعض الباحثون بتصميم بعض البروتوكولات التشفيرية املا بالحصول على نظام امن لهذا التطبيق و تحقيق بعض المتطلبات الأمنية. من أمثلة المتطلبات الأمنية: عدم السماح بالاستخدام المتعدد للكوبون او عدم السماح بنسخة لشخص اخر وهكذا. وقمنا نحن بتحليل هذه البروتوكولات بطرق تحليلية رياضية و بالأخص اداة ‘كاسبر’. وقد تم ايجاد ثغرات في جميع البروتوكولات السابقة مع عرض حلول لها. وفي الأخير قمنا بتصميم بروتوكول مستفيدين من الدروس السابق. (الى هنا تم نشر 5 اوراق علمية مسبقا بهذا الخصوص) الاسهام العلمي في هذه الورقة هو تصميم General Framework تكون كدليل و مرجع قوي مثبت رياضيا لاي شخص يحاول ان يصمم NFC Mobile Coupon Security protocol والذي تم اخضاع جميع البروتوكولات السابقة تحته (بما فيهم ما صممناه). الاسهامات الاخرى كانت من زوايا اخرى وهي طريقة مبتكرة لتمثيل بعض اجزاء احد البروتوكولات الجديدة والتي يصعب تمثيلها باداة التمثيل الرياضي مباشرة. بالاضافة لاكتشاف بعض جوانب الضعف في اداة كاسبر التحليلية نفسها و التي لم تكن تعرف من قبل. ——— الخاتمة ——— ما قد تم شرحة مسبقا هو خلاصة ٨٠٪ من بحثي بالدكتوراه. اما ال ٢٠٪ فهو عبارة عن حل لهجوم Relay Attack والذي ما زالت تعاني منه تقنية NFC و ال RFID عموما، وهو ايضا منشور في مجلة محكمة ولله الحمد. ولعله تتاح فرصة مستقبلا لمناقشته. د. علي الشهري استشاري أمن معلومات في شركة HP https://www.linkedin.com/profile/view?id=44989924 ——— النهاية ———   2- المناقشة: ١- هل ممكن مشاركة الورقة نفسه لانها ستكون اسهل كلغة علمية ومصطلحات؟ هي الان في حالة التنقيح النهائي، وباذن الله عند الانتهاء سوف أقوم بإرسالها لايميلات الأشخاص المهتمين. ٢- ماذا اضافت ابل عندما استخدمت NFC مع البصمة في عمليات الشراء ، هل استخدمت برتوكول خاص ام ان البصمة كانت اضافة أمنية لاستخدام ال NFC؟ تم استخدام البصمة كإضافة أمنية للتحقق من المستخدم وتعمل عمل الكلمة السرية بالضبط. هنالك استخدام متقدم لها من ناحية اخرى داخل الجوال حيث يتم من خلالها معرفة البطاقة المنشودة و ماهية صلاحيتها. لكن لا يتم استخدامها في البروتوكول خارج الجوال لانه ستاندرد EMV ان كنت قريبا أصبحت شاكا في ان الجميع يستخدم EMV وخصوصا أمريكا ! ٣-ابل وش اضافه لحمايه المعلومات؟ بالاضافة للبصمة، فإنها تلافت إرسال رقم البطاقة الكامل كما كانت تفعل Google Wallet لكن تداركت قوقل هذا. لان هذه المعلومات ممكن ان تستخدم في الاصدياد الالكتروني. ٤- كم عدد البروتوكولات التي تم اختبارها، و ماهي المعايير التي اتبعتها لاختيار البروتوكولات؟! اختبرت ٤ بروتوكولات موجودة حيث انها تتدرج في مقدار تغطية المتطلبات الأمنية Secuity requirements بالنسبة لمعايير الأختيار فكان المعيار الوحيد هو من حاول تصميم NFC mobile coupon protocol وقام بنشرة علميا فهو تحت الاختبار. ولان هذا المجال جديد فلم اجد الا هؤلاء الأربعة. ٥- بالنسبة للثغرات، ذكرت أنكم وجدتو في كل بروتوكول ثغرات.. يا ليت توضح هنا عدة جوانب.. أ- هل الثغرات المكتشفة تعتبر متكررة و مشتركة بين البروتوكلات؟! ابتداءا فالباحثون يعذرون (بعضهم و ليس كلهم) في هذه الثغرات لصعوبة تصميم البروتوكولات التشفيرية في الأساس. وتوجد بعضها متكرر اما لإساءة التصميم او إساءة التعريف للمتطلب الأمني. ب- ما هي أهم الثغرات المكتشفة؟ و ما مدى استغلالها في الهجمات؟! المتطلب الأمني الأكثر صعوبه للتحقيق كان التحقق الاضافي لصاحب الكوبون قبل الاستخدام مباشرة من الكاشير وهذا كان في البروتوكولات الجيدة. لكن بعضها كان سيئ للغاية لدرجة انه باستطاعتك ان تصمم بوستر (موزع الكوبونات) بنفسك. بالنسبة للقدرة المهاجم على استغلالها تختلف. فالأغلب قابل للتطبيق لكن البعض أنا أراه صعب للتطبيق بينما اختلفوا معي محكموا الورقة و يقولون انه يبقى خطرا يلزم التعامل معه. الثغرة المختلف فيها هي هجوم على مستوى تركيب البت وليس البروتوكول وهذا محل الخلاف. ج- تقييم بروتوكلك المقترح بين البروتوكولات الأخرى؟! بناءا على معايير الاختبار و المواصفات المقترحة من الباحثين من قبلي، فيعتبر هو الأصلب و متوسط السرعة. ٦- ما هي الأسس التي بني عليها الفريمورك؟! ان امثل رياضيا الطريقة الصحيحة التي يتم التحقق من الخاصية الأمنية، ومن ثم اي شخص يدعي تحقيق خاصية أمنية ل NFC coupon مستخدما التشفير يستطيع ان يختبر هذا عن طريق الفريمورك. ٧- لماذا يصعب تمثيل البروتوكلات الجديدة بالتمثيل الرياضي المباشر؟ و ماهي تبعات ذلك؟! لعلي أوضحها اكثر هنا. اللغة الرياضية الاساسية هي CSP و الأداه المستخدمة هي كاسبر و هي فوق ال CSP ومتخصصه لتسهيل عملية التمثيل بدون الحاجة لفهم رياضي كبير. لكن التمثيل بكاسبر محدود، ولهذا عادة يجب ان تزل ل CSP اذا تعذر التمثيل بكاسبر مباشرة. في حالتي أنا كان مطلوب ان امثل بعض اجزاء البروتوكول والتي تستلزم النزول ل CSP لكن اقترحت ان نمثلها بالطرق المتوفرة حاليا في كاسبر ووفقت في هذا. ٨- قلت في معرض كلامك، اكتشاف ضعف في أداة كاسبر.. السؤال: ماهو أثر ذلك على نتائج تحليلك للبروتوكولات حيث أنه تم استخدام نفس الأداة؟! لم يؤثر كثيرا ولله الحمد. لان الضعف كان سوء فهم بيني و بين الاداة فيما يتعلق بالتعريف في حاله واحدة و هي تقسيم الرسائل الطويلة الى عدة رسائل. هذا ينتج عنه في العادة هجوم كاذب. ٩- ماشاء الله عرض جميل ، بالنسبة للcoupon هل تعتبر loyalty cards منها اذا نعم، فايضا ابل ستدعمها في iOS 9 وتعمل تحت خدمة ApplePay‬ نفس الفكرة لكن مختلفه قليلا. الكوبون هو عرض من المحل بتخفيض او شيئ مجاني. وال loyalty card تعطيك نقاط مع كل شراء كسر التشفير ١٠ اسمح لي اخ علي بطرح سوالي من وجهه نظر تخصصي؛ تعد الملفات المنشئه باسلوب فن الاخفاء ( steganography ) من أصعب التحديات واكثرها تعقيدا والتي تواجه المحقق الرقمي،، وفي حاله تم كشف الإخفاء باساليب متخصصه ( steganalysis) عاده تكون الملفات المخفيه مشفره ايضا وهذا بالطبع يدل على مؤشرات أهمها احترافيه الهدف وأهميه وحساسيه الملف المشتبه به بما يخدم مصلحه القضيه. سؤالي كالتالي؛ اذا كان لدى جهه التحقيق موارد مفتوحه ( اقصد ان التكلفه لا تهمهم بقدر أهميه معرفه محتوى الملفات المشتبه بها المخفيه والمشفره وذلك في وقت قياسي) هل يوجد حلول سريعه بغض النظر عن تكلفتها ماديا بحيث تساعد في مهاجمه التشفير وفكه آنيا (لان بعض حلول فك التشفير على حد علمي تستمر لفتره طويله والوقت مهم جدا) هل هناك شركات متخصصه تقدم هذا النوع من الخدمه؟ شاكر ومقدر لك مقدما…. باسل العمير: اسمح لي اجاوب على السؤال مع انه غير موجه لي. لوغاريثمات التشفير المصممة تصميماً جيداً لا يمكن فكها لا آنيا ولا بعد وقت طويل (الإ اذا كان لديك القدرة على للانتظار لملايين السنين)‬ علي الشهري: هلا اخوي سعد. صراحه ليس لدي فكرة قوية عن هذا الموضوع. لكن اعرف باحثة دكتوراه في ال steganography و ال watermarking ممكن تفيدنا. كسر التشفير في العموم كما تفضل اخوي باسل صعب لان فلسفة التصميم الحديث أصبحت مكشوفة و التحدي ان تكسرها دون وجود المفتاح. لكن هذا الذي تعلمناه في الكتب! حسين الجحدلي: لكن انا برجعكم لموضوع النقاش الأصلي… شدني تعليق اخوي باسل حول فك التشفير، و في اعتقادي ان اي لوغارثم يمكن فكه لان من وضعه بادئ ذي بدء هو بشر و لا يوجد كمال لأي مقترح.. لذلك إمكانية فك التشفير موجودة!! و لكن السؤال مدى تعقيدها… ثلاث أمور تحكم ذلك: ١- القدرة الحاسوبية. ٢- القدرة المعرفية. ٣- الوقت. اما النقطة ١ و ٢ فيمكن توفرها حالياً… و كذلك عند جمع عدد كاف من الرسائل المشفرة قد يسهم ذلك بتسريع فك التشفير.. أتمنى الحقيقة اسمع تعليق الشباب المختصين حول الموضوع.. باسل العمير: اسمح لي اعلق بالإنجليزي The security of encryption is exponentially increasing with the length of the key. That is, assuming the key is 128-bit long, the attacker will need resources (time and storage) proportional to 2^128. Now assume that you have computational power that can perform this much operations in one year (it is actually much more than that even for super computers). Then, by increasing the key by one bit, you will double this time. Imagine doubling the key to 256 bit long, then you will need to multiply this one year by 2^128. The bottom line is the computational capabilities improve in a much much much slower rate the the exponential complexity. Therefore, to prove that any encryption algorithm is secure, all you need to do is to show that it’s security is exponential in the length of the key. الكوانتم كمبيوتنق منيف بن نايف: الكوانتم كمبيوتنق لديه القدرة الموجودة في النقاط الثلاث التي ذكرتها الوقت كان هو العامل الرئيسي والقوة التي ترتكز عليها اغلب معادلات التشفير، على سبيل المثال تحتاج الى ثلاثين سنة على سبيل المثال لتخمن كلمة مكونة من حروف وأرقام علي الشهري: الكوانتم خطر فقط على ال public key encryption فقط وهو مدعى للقلق على كل حال! و يفيدنا ايضا الدكتور باسل وهو مختص بالتشفير ايضا. منيف بن نايف: كذلك يشكل خطر على ال symmetric لكن بشكل اقل الكوانتم الان في بداياته باسل العمير: صحيح. هناك ما يسمى shor’s algorithm that can solve the discrete log and the integer factorization problems in polynomial time using quantum computers, thus breaking RSA and Elgamal public key crypto. However, its effectiveness on symmetric crypto is just slashing the key by half. So it’s not very damaging to AES, for example. It’s worth mentioning that there are new “post-quantum” public key systems that are secure even with quantum computers. They are very inefficient, however. Very active research area in crypto nowadays. مفتاح التشفير حسين الجحدلي: يعطيك العافيه يا باسل، واضح الكلام هذا على اعتبار انه نظري… لكن ما اثر زيادة حجم مفتاح التشفير على عملية التشفير؟؟ يعني ماهو حل منطقي أني اقعد أزيد حجم المفتاح..! كذلك كسر التشفير يأثر عليه عوامل أخرى، فجمع عدد من الرسائل المشفرة يسرع عملية الكسر.. وزي ما قال منيف، كل ما زاد القدرات الحاسوبية يتقلص الزمن اللازم لفك التشفير.. الموضوع شيق و جميل… و اشكر الاخوان على مداخلاتهم.. و أعيد شكري لباسل على توضيح نقطته.. باسل العمير: The idea is that performing the encryption is polynomial to the length of the key, wile breaking it is exponential to the key. For example, AES-256 a little slower than AES-128, while breaking the former requires 3.4028236692094e+38 times the time needed to break the latter. Collecting messages should not affect secure algorithms. هل المفتاح الخاص يستخدم فقط مره خلال العمليه او يتغير. Does the private key used only during the current session or in the all operation? If it is used only once, it would be hard to break it due to time limitation.” الجواب: عادة المفتاح الخاص ينشئ لفترات طويلة، ويتم توليد مفاتيح مؤقتة منه ل sessions ويتم هذا بطرق عديدة. والسبب هو كما تفضلت عند انتهاء السشن يصبح المفتاح عديم الفائدة. الا اذا طحت في واحد فاااااضي و قاعد يجمع كل المفاتيح المتولدة و حاول يربطها ببعض لكي يعرف الطريقة المتبعة لجعلها عشوائية ، فأنت في مشكلة اذ لم يكن طريقة التوليد شبه عشوائية قوية و متينة. لاحظ لا يوجد على حد علمي لوغاريتم لإنشاء ارقام عشوائية ١٠٠٪ لان هذا ما يحقق التعريف النظري الكامل ل “التشفير الأمن ” وهو غير موجود في الواقع. لوغاريتم لإنشاء ارقام عشوائية منيف بن نايف: سؤال للدكتور علي حول عدم وجود لوغاريتم يولد أرقام عشوائية بنسبة ١٠٠ ؟ مارايك في لوغاريتميات توليد الأرقام العشوائية من خلال الاستفادة من المحيط والطبيعة كالأصوات في لحظة ما، شدة الإضاءة في مكان ما وفي لحظة زمنية معينه او شدة الازدحام من خلال التقاط صورة عشوائية لموقع ما عام ومكتظ يشهد حركة وتحليلها والخروج برقم معين الخ.. بحسب خبرتي في تحليل الصور، عند التقاطك لصورتين من نفس المكان ومن نفس الكاميرا فانت لن تحصل عل نسبة تشابه عاليه جدا نتيجة ال Image noise الا تعتبر هذه الطرق عشوائية ١٠٠ ٪ كون كل رقم لا يعتمد على ماقبله وبهذا تعتبر أمنه ومن الصعوبة كسرها؟ علي الشهري: امممم صراحة من الممكن ان يكون هذا التوجه جيد مما يزيد من تعقيد الوصول الى المصدر الأساسي للأرقام العشوائية. وهي كثيرة مثل ايضا الاعتماد على تحريك الماوس العشوائي وهكذا. لكن انشاء رقم عشوائي بكل ما تحملة الكلمة من معنى مستحيل نظريا والذي لا يعتمد على شيئ فطالما هو معتمد على شيئ فهو ليس عشوائي. ‪باسل العمير:‬‬‬‬ هناك بحوث كثيرة لإنتاج ارقام عشوائية. قد تستخدم خصائص فيزيائية لإنتاج ارقام عشوائية حقيقية، مثل حركة الإلكترونات او الفوتونات او ما شابه. مثل هذه قد تنتج ارقام عشوائية حقيقية. ام ما يستخدم في الأغلب فهي ارقام ناتجة من software وهذه لا يمكن ان تكون عشوائية حقيقية. الموضوع طويل وشيق وموضوع مهم للبحوث في أمن المعلومات. علي الشهري: شكرًا باسل. احتمال فعلا في هذه الحاله تصبح عشوائيه اذا كانت معتمدة على هذه الخصائص الفيزيائية العشوائية. شكرًا للاخوة على هذه الأسئلة الجميلة ونامل بان غطينا بعض التساؤلات. الي حاب يطّلع على الاطروحة ككل يرسلي إيميله على الخاص.