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

هنا يأتي دور الورقة البحثية. لقد بنى المؤلفون ورشة عمل رقمية تسمى HOPSCOTCH (اسم مرح يعبر عن لعبة القفز) داخل برنامج كمبيوتر قوي يسمى Lean 4. فكر في HOPSCOTCH كأنه مدقق إثباتات آلي فائق الذكاء، لا يكتفي بفحص رياضياتك فحسب، بل يفهم "قصة" إثبات الأمان. وبدلاً من إجبار علماء التشفير على الكتابة بلغة غريبة ومحدودة، يتيح لهم HOPSCOTCH كتابة الإثباتات باستخدام نفس الأدوات التي يستخدمونها لكل رياضياتهم الأخرى. إنه يحول عملية "القفز بين الألعاب" — أي الانتقال من سيناريو أمني إلى آخر — إلى كائن واضح يمكن للكمبيوتر فحصه، والتحقق منه، وحتى المساعدة في أتمتته. لم يكتفِ المؤلفون ببناء الأداة فحسب؛ بل استخدموها بنجاح لإثبات أمان العديد من طرق التشفير الشهيرة، بما في ذلك بناء معقد يسمى GGM، مما يظهر أن هذا "المدقق الآلي" يمكنه التعامل مع تحديات التشفير في العالم الحقيقي دون ارتباك.

الصورة الكبيرة: لماذا نحتاج إلى روبوت لتدقيق الإثباتات؟

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

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

إذا استطعنا إثبات أن كل "قفزة" واحدة آمنة، فإن السلسلة بأكملها آمنة. وهذا ما يسمى "إثبات القفز بين الألعاب".

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

دخول HOPSCOTCH: المترجم العالمي

قرر مؤلفو هذه الورقة، ستيفان دزيمبوسكي، جرجي فابيا actually، دانييلي ميتشيانسيو، ورافال ستيفانسكي، بناء جسر. لقد أنشأوا HOPSCTOCH، وهو إطار عمل داخل Lean 4، وهو برنامج كمبيوتر شهير يستخدم للتحقق من البراهين الرياضية.

إليك سحر HOPSCOTCH:

• لا لغة جديدة: على عكس الأدوات الأخرى التي تجبرك على تعلم طريقة جديدة ومقيدة لكتابة الكود، يتيح لك HOPSCOTCH كتابة الإثباتات باستخدام لغة Lean القياسية. الأمر يشبه السماح للطاهي بالطبخ باستخدام سكاكينه المفضلة بدلاً من إجباره على استخدام سكاكين بلاستيكية.
• الإثباتات ككائنات: في HOPSCOTH، الإثبات ليس مجرد كومة من النصوص. إنه كائن مهيكل، مثل نموذج "ليجو". كل "قفزة" في اللعبة هي قطعة "ليجو" محددة. يمكنك تركيبها معًا، ويتحقق الكمبيوتر مما إذا كانت تتناسب تمامًا. إذا حاولت توصيل قطعتين لا تتطابقان، سيقول الكمبيوتر: "لا، هذا لا يعمل".
• خدعة "التجريد": أحد أصعب أجزاء هذه الإثباتات هو إظهار أن نظامين مختلفين في المظهر يتصرفان بنفس الطريقة تمامًا. يستخدم HOPSCOTCH خدعة ذكية تسمى "تجريد الحالة". تخيل أن لديك روبوتين؛ أحدهما لديه مخطط أسلاك داخلية فوضوي، والآخر لديه مخطط مرتب. يسمح لك HOPSCOTCH برسم خريطة (دالة التجريد) توضح كيف تتوافق الأسلاك الفوضوية مع الأسلاك المرتبة. إذا كانت الخريطة صحيحة، فإن الكمبيوتر يعرف أن الروبوتين متطابقان في السلوك، حتى لو بدا شكلهما مختلفًا من الداخل.

ما فعلوه بالفعل وما وجدوه

لم يكتفِ المؤلفون ببناء الأداة فحسب، بل وضعوها تحت الاختبار. استخدموا HOPSCOTCH للتحقق رسميًا من أمان أربعة مفاهيم تشفير رئيسية:

1. التشفير ثم الـ MAC (Encrypt-then-MAC): طريقة لجعل الرسائل سرية وغير قابلة للتلاعب في آن واحد. أثبتوا أنه إذا كان التشفير الأساسي و"الوسم" (MAC) آمنين، فإن النظام بأكمله آمن حتى ضد أمهر المخترقين.
2. تشفير ElGamal: طريقة شهيرة لإرسال رسائل سرية باستخدام مفاتيح عامة. أظهروا كيفية إثبات أمانه بناءً على مسألة رياضية صعبة تسمى فرضية "ديسيجنال ديفي-هلمان" (DDH).
3. السرية لمرة واحدة إلى IND-CPA: أثبتوا أنه إذا كان النظام آمنًا لرسالة واحدة، فيمكن جعله آمنًا لرسائل عديدة، وهي خطوة حاسمة في بناء تشفير قوي.
4. بناء GGM: هذا هو الجزء الأكبر. طريقة GGM تحول مولد أرقام عشوائية بسيط إلى "دالة شبه عشوائية" معقدة (مولد أرقام عشوائية مزيفة تبدو حقيقية). لم تتمكن إثباتات الكمبيوتر السابقة من التعامل إلا مع نسخ سطحية جدًا من هذا (مثل أشجار مكونة من 3 مستويات فقط). استخدم المؤلفون HOPSCOTCH لإثبات أمان GGM لـ العمق غير الثابت، مما يعني أنه يعمل لأشجار من أي حجم. وبحسب علمهم، يعد هذا أول مرة يتم فيها التحقق بنجاح من هذا البناء المعقد والمحدد بواسطة مساعد إثبات عام الأغراض.

كيف فعلوا ذلك (آليات "اللعبة")

تشرح الورقة أن HOPSCOTCH يعمل من خلال تقسيم الإثبات إلى خطوات محددة، أو "بُناة" (constructors):

• التكافؤ الملحوظ (Observational Equivalence): إثبات أن الألعاب تبدو متشابهة للمراقب الخارجي.
• الاختزال (Reductions): إظهار أنه إذا استطعت كسر اللعبة (أ)، فيمكنك كسر اللعبة (ب).
• تسلسلات الهجين (Hybrid Sequences): ربط العديد من الخطوات الصغيرة معًا.

يتضمن إطار العمل "تكتيكات" (مساعدات مؤتمتة) تحاول حل هذه الخطوات نيابة عنك. على سبيل المثال، إذا كنت بحاجة إلى إثبات أن "الأوراكل" (أنظمة اللعبة) متطابقة، فقد يحاول الكمبيوتر تلقائيًا العثور على خريطة "تجريد الحالة". وإذا لم يجدها، فإنه يترك الخطوة ليحلها الإنسان، لكنه يحافظ على الهيكل بحيث يعرف الإنسان بالضبط أين يقف.

كما أثبت المؤلفون "نظرية السلامة الحسابية". وهي طريقة منمقة للقول: "إذا قال الكمبيوتر إن هذا الإثبات صالح، فهو بالفعل صالح في العالم الحقيقي". لقد أظهروا أنه لكل كائن إثبات ينشئه HOPSCOTCH، يمكنك حسابيًا تحديد مقدار "الميزة" (advantage) التي سيحصل عليها المخترق بالضبط، بناءً على الافتراضات المستخدمة في الإثبات. وهذا يضمن أن الكمبيوتر لا يلعب لعبة مع نفسه فحسب، بل يقدم ضمانًا أمنيًا حقيقيًا وملموسًا.

الخلاصة

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

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