Quantum Cryptography and Autoformalization in Lean

في عالم الاتصالات الآمنة، لا تُصنع الأقفال الأكثر موثوقية من الفولاذ، بل من القوانين الأساسية للفيزياء. هذا هو مجال توزيع المفاتح الكمومية، وهي طريقة يقوم من خلالها شخصان، يُطلق عليهما تقليديًا أليس وبوب، بتوليد رمز سري مشترك لحماية رسائلهما. وخلافًا للتشفير التقليدي، الذي يعتمد على صعوبة حل المسائل الرياضية المعقدة، يعتمد هذا النهج على حقيقة أن قياس جسيم ضوئي صغير، أو فوتون، يغيره حتمًا. إذا حاولت طرف ثالث، متلصصة تُدعى إيف، التنصت، فإنها تترك أثرًا يمكن اكتشافه لتدخلها. لعقود من الزمن، طور العلماء بروتوكولات لإنشاء هذه المفاتيح، لكن إثبات أن هذه الأنظمة آمنة حقًا كان عملية هشة. غالبًا ما اعتمدت البراهين على سلسلة من الحجج الرياضية المنسوجة معًا من أوراق بحثية مختلفة، لكل منها مجموعة من الافتراضات الخاصة بها. وإذا كانت إحدى حلقات تلك السلسلة غير متطابقة تمامًا مع أخرى، أو إذا تم التغاضي عن افتراض خفي، فقد تتعرض ضمانة الأمان بأكملها للخطر دون أن يلاحظ أحد ذلك.

قام فريق من الباحثين في معهد ماساتشوستس للتكنولوجيا الآن بمعالجة هذه الهشاشة من خلال بناء برهان أمني من الصفر باستخدام برنامج حاسوبي مصمم للتحقق من المنطق الرياضي. لقد ركزوا على طريقة محددة واسعة الاستخدام تسمى بروتوكول BB84، والذي يستخدم أزواجًا من الجسيمات المتشابكة لتوليد المفاتيح. وبدلاً من الوثوق بإنسان للتحقق من أن كل خطوة من خطوات المنطق متماسكة، قاموا بترجمة الحجة الأمنية بأكملها إلى لغة رسمية يمكن للحاسوب قراءتها والتحقق منها بدقة مطلقة. والنتيجة هي برهان تم التحقق منه آليًا لا يترك مجالًا للفجوات الخفية أو الافتراضات غير المتطابقة. وهو يؤكد أن البروتوكول يظل آمنًا حتى عندما يكون عدد الجسيمات المتبادلة محدودًا، وهو قيد واقعي شائع غالبًا ما يضعف تقديرات الأمان. علاوة على ذلك، استُخدم نفس النظام الحاسوبي الذي تحقق من البرهان لاكتشاف حد رياضي جديد وأكثر إحكامًا، مما يقلل من عقوبة الحجم المحدود على معدل المفتاح.

بدأ الباحثون بإنشاء لغة رقمية داخل النظام الحاسوبي تفرض بصرامة قواعد العمليات المحلية والاتصال الكلاسيكي. وفي سياق التشفير الكمومي، يعني هذا أن الحاسوب يضمن أن أليس وبوب يمكنهما فقط إجراء عمليات على جسيماتهما الخاصة ولا يمكنهما مشاركة المعلومات إلا عبر قنوات عامة، دون الوصول سحريًا إلى البيانات الخاصة لبعضهما البعض. تعمل هذه اللغة كحاجز حماية، مما يمنع أنواع الأخطاء المنطقية التي قد تفلت من المراجعين البشر. فعلى سبيل المثال، في محاولات سابقة لصياغة هذه البراهن، اقترح وكيل ذكاء اصطناعي ذات مرة طريقة يتم فيها إنشاء المفتاح النهائي عن طريق دمج سلاسل لا يمتلكها أي من الطرفين فعليًا. وقد رصد الحاسوب، من خلال قواعده الصارمة، هذا الأمر فورًا باعتباره مستحيلاً، مما أجبر الفريق على تحسين نهجهم. ومن خلال بناء البروتوكول خطوة بخطوة داخل هذه البيئة المقيدة، ضمن الفريق أن مبرهن الأمان النهائي يصف بالضبط العملية الفيزيائية التي يقصدون حمايتها.

بمجرد بناء البروتوكول، طلب الفريق من الحاسوب التحقق من أمنه ضد نوع قوي من الهجمات يُعرف بالهجوم المتماسك، حيث يتفاعل المتلصص مع جميع الجسيمات في وقت واحد بدلاً من التفاعل معها واحدًا تلو الآخر. تحقق الحاسوب من كل خطوة منطقية، بدءًا من القياس الأولي للجسيمات وصولًا إلى الخطوات النهائية لتصحيح الأخطاء وتضخيم الخصوصية. وأكد أن البروتوكول آمن، مما يعني أنه إذا لم يتوقف النظام، فإن المفتاح الناتج يكون غير قابل للتمييز عن مفتاح سري عشوائي مثالي، حتى بالنسبة لمتلصص يمتلك قدرة حوسبة غير محدودة. والأهم من ذلك، أن البرهان أخذ في الاعتبار حقيقة أن الأنظمة الواقعية تعمل بعدد محدود من الجسيمات، وليس تيارًا لانهائيًا. وهذا التأثير المرتبط بالحجم المحدود يجبر العلماء عادةً على أن يكونوا متحفظين للغاية، حيث يتخلصون من المزيد من مواد المفاتيح المحتملة لضمان السلامة. ومع ذلك، قدم البرهان الجديد حسابًا دقيقًا لكمية مواد المفاتيح التي يمكن الاحتفاظ بها بأمان، مما يقلل العقوبة المفروضة بهذه الحدود المحدودة.

في تحول مفاجئ، استخدم الباحثون نفس المسار الحاسوبي ليس فقط للتحقق من عملهم، بل لتحسينه أيضًا. فبينما كان النظام يتحقق من المنطق، ساعد الفريق في تحديد حد أكثر إحكامًا لتباين الإنتروبيا الشرطية المستخدم لتقدير أمن هذه الأنظمة. كانت الصيغة الموجودة فضفاضة للغاية، مما أدى إلى تقليل غير ضروري في طول المفتاح السري. وبإرشاد من قدرة الحاسوب على اختبار ومقارنة الحدود الرياضية المختلفة، استنتج الفريق متباينة جديدة وأكثر دقة. هذه المتباينة الجديدة أكثر إحكامًا، مما يسمح للنظام بتوليد مفاتيح مع تقليل عقوبة الحجم المحدود مقارنة بما كانت ستسمح به الصيغة القديمة، دون التضحية بالأمن. لم يكن هذا الاكتشاف مجرد تخمين؛ بل كان نتيجة رياضية صارمة تحقق منها الحاسوب كحقيقة، مما يثبت أن محركات البرهان الرسمي يمكنها القيام بأكثر من مجرد التحقق من العمل — يمكنها أيضًا تسريع الاكتشاف العلمي بنشاط من خلال إيجاد حلول أفضل للمسائل القديمة.

كما يعد هذا العمل نموذجًا لكيفية التحقق من الأنظمة التشفيرية المستقبلية. ومن خلال إصدار المكتبة الأساسية للتعريفات والمبرهنات كمصدر مفتوح، قدم الباحثون مجموعة أدوات قابلة لإعادة الاستخدام للمجتمع العلمي. تتضمن هذه المكتبة التعريفات الرسمية للحالات الكمومية، والقنوات، واللغة المحددة لوصف البروتوكولات، مما يسمح للعلماء الآخرين بالبناء على هذا الأساس. وهذا يعني أن البراهن المستقبلية للبروتوكولات الكمومية المختلفة، أو حتى لمجالات أخرى من علوم المعلومات الكمومية، يمكن بناؤها بنفس المستوى من الصرامة. لقد أظهر الفريق أنه من خلال الجمع بين الرؤية البشرية والدقة المستمرة للمنطق الذي يتم التحقق منه آليًا، يمكن القضاء على حالات عدم اليقين الخفية التي لطالما أرقت هذا المجال. والنتيجة هي معيار جديد للحجج الأمنية، حيث لا تكون موثوقية المفتاح الكمومي مجرد ادعاء يقدمه باحث، بل حقيقة يتحقق منها آلة.