Game Hopping in Lean

कल्पना कीजिए कि आप एक मास्टर लॉकस्मिथ (ताला बनाने वाले विशेषज्ञ) हैं जो यह साबित करने की कोशिश कर रहे हैं कि आपका नया वॉल्ट (तिजोरी) अटूट है। आप सिर्फ यह नहीं कहेंगे, "यह मजबूत है!" बल्कि आपको चरणों का एक क्रम दिखाना होगा: "यदि आप इस छोटे से ताले को नहीं तोड़ सकते, तो आप दरवाजे को नहीं तोड़ सकते; यदि आप दरवाजे को नहीं तोड़ सकते, तो आप वॉल्ट को नहीं तोड़ सकते।" आधुनिक क्रिप्टोग्राफी इसी तरह काम करती है। विशेषज्ञ सुरक्षा का परीक्षण करने के लिए "गेम्स" (खेलों) का उपयोग करते हैं, जहाँ एक हैकर किसी रहस्य का अनुमान लगाने की कोशिश करता है, और सिस्टम की सुरक्षा को यह दिखाकर सिद्ध किया जाता है कि इसे तोड़ना एक ज्ञात, असंभव पहेली को हल करने जितना ही कठिन है। लेकिन यहाँ एक पेच है: इन प्रमाणों को हाथ से करना ताश के पत्तों के घर को तूफान में संतुलित करने जैसा है। इसमें एक छोटी सी गलती करना, एक सूक्ष्म अंतर को छोड़ देना, या जटिलता में खो जाना बहुत आसान है, और यदि आप एक भी चरण चूक जाते हैं, तो पूरा प्रमाण ढह जाता है। इसीलिए वैज्ञानिक एक ऐसा तरीका खोजने की तलाश में रहे हैं जिससे कंप्यूटर हर एक पत्ते की जांच कर सके, यह सुनिश्चित करते हुए कि वह घर मजबूती से खड़ा रहे।

यहीं पर यह शोध पत्र आता है। लेखकों ने Lean 4 नामक एक शक्तिशाली कंप्यूटर प्रोग्राम के भीतर एक डिजिटल कार्यशाला बनाई है जिसे HOPSCOTCH (कूदने के खेल के लिए एक चंचल नाम) कहा जाता है। HOPSCOTCH को एक सुपर-स्मार्ट, रोबोटिक प्रूफ-रीडर (प्रमाण-पड़ताल करने वाला) समझें जो न केवल आपके गणित की जांच करता है; बल्कि यह सुरक्षा प्रमाण की कहानी को भी समझता है। विशेषज्ञों को मजबूर करने के बजाय कि वे एक अजीब, सीमित भाषा में लिखें, HOPSCHOTCH उन्हें अपने अन्य सभी गणित के लिए उपयोग किए जाने वाले उपकरणों का उपयोग करके प्रमाण लिखने की अनुमति देता है। यह "गेम-हॉपिंग" प्रक्रिया को—एक सुरक्षा परिदृश्य से दूसरे में कूदने को—एक स्पष्ट, चरण-दर-चरण वस्तु में बदल देता है जिसे कंप्यूटर निरीक्षण, सत्यापन और यहाँ तक कि स्वचालित (automate) भी कर सकता है। लेखकों ने केवल एक उपकरण नहीं बनाया; उन्होंने इसका उपयोग कई प्रसिद्ध एन्क्रिप्शन विधियों की सुरक्षा को सफलतापूर्वक सिद्ध करने के लिए किया, जिसमें GGM नामक एक जटिल निर्माण शामिल है, जो यह दर्शाता है कि यह "रोबोटिक प्रूफ-रीडर" बिना भ्रमित हुए वास्तविक दुनिया की क्रिप्टोग्राफिक चुनौतियों को कैसे संभाल सकता है।

बड़ी तस्वीर: हमें एक प्रूफ-रीडिंग रोबोट की आवश्यकता क्यों है?

डिजिटल सुरक्षा की दुनिया में, हम "प्रूवेबल सिक्योरिटी" (सिद्ध सुरक्षा) पर भरोसा करते हैं। इसका अर्थ यह है कि हम केवल यह उम्मीद नहीं करते कि हमारे कोड सुरक्षित हैं; हम इसे सिद्ध करने का प्रयास करते हैं। इसे करने का मानक तरीका "गेम-बेस्ड" (खेल-आधारित) दृष्टिकोण है। कल्पना कीजिए कि एक सुरक्षा गार्ड (सिस्टम) और एक चोर (एडवर्सरी/विरोधी) है। गार्ड के पास एक रहस्य है, और चोर उसका अनुमान लगाने की कोशिश करता है। गार्ड को सुरक्षित सिद्ध करने के लिए, हम केवल यह नहीं कहते कि "वह अच्छा है।" हम "गेम्स" या परिदृश्यों की एक श्रृंखला बनाते हैं।

1. असली खेल (The Real Game): चोर वास्तविक सिस्टम को तोड़ने की कोशिश करता है।
2. द हॉप (The Hop): हम एक थोड़ा अलग खेल की कल्पना करते हैं जो लगभग समान है लेकिन विश्लेषण करने में आसान है। हम यह सिद्ध करते हैं कि यदि चोर असली खेल जीत सकता है, तो वह इस नए, थोड़े अलग खेल को भी जीत सकता है।
3. द चेन (The Chain): हम एक खेल से दूसरे खेल की ओर कूदते रहते हैं, हर बार नियमों को थोड़ा सा बदलते हुए, जब तक कि हम एक अंतिम खेल तक नहीं पहुँच जाते जो स्पष्ट रूप से जीतना असंभव है (जैसे कि लगातार दस लाख बार सही कॉइन टॉस का अनुमान लगाना)।

यदि हम यह सिद्ध कर सकें कि प्रत्येक "हॉप" सुरक्षित है, तो पूरी श्रृंखला सुरक्षित है। इसे "गेम-हॉपिंग प्रूफ" कहा जाता है।

समस्या यह है कि मनुष्य इसे पूरी तरह से करने में बहुत खराब होते हैं। ये प्रमाण लंबे, अस्त-व्यस्त और सूक्ष्म विवरणों से भरे होते हैं। एक भी छूटा हुआ विवरण पूरे प्रमाण को गलत बना सकता है, और सिस्टम असुरक्षित हो सकता है। वर्षों से, शोधकर्ताओं ने इन प्रमाणों की जांच करने के लिए विशेष कंप्यूटर उपकरण बनाने की कोशिश की है, लेकिन ये उपकरण अक्सर गणितज्ञों की भाषा नहीं बोलते। वे एक ऐसे अनुवादक की तरह हैं जो केवल "सुरक्षा" बोलता है लेकिन "गणित" नहीं, जिससे विशेषज्ञों को अपने विचारों को इधर-उधर अनुवाद करने के लिए मजबूर होना पड़ता है, जो धीमा और त्रुटिपूर्ण है।

प्रवेश HOPSCOTCH: एक सार्वभौमिक अनुवादक

इस शोध पत्र के लेखक, स्टीफन ज़िएम्बोव्स्की, ग्रेगोज़ फबियान्स्की, डेनिएल मिकियानसिओ और राफ़ल स्टेफ़ांस्की ने एक सेतु बनाने का निर्णय लिया। उन्होंने Lean 4 के भीतर एक ढांचा तैयार किया, जो एक लोकप्रिय कंप्यूटर प्रोग्राम है जिसका उपयोग गणितीय प्रमाणों को सत्यापित करने के लिए किया जाता है।

HOPSCOTCH का जादू यहाँ है:

• कोई नई भाषा नहीं: अन्य उपकरणों के विपरीत जो आपको कोड लिखने का एक नया, प्रतिबंधित तरीका सीखने के लिए मजबूर करते हैं, HOPSCOTCH आपको मानक Lean का उपयोग करके प्रमाण लिखने की अनुमति देता है। यह एक शेफ को उनके पसंदीदा चाकू के साथ खाना पकाने देने जैसा है, बजाय इसके कि उन्हें प्लास्टिक के चाकू उपयोग करने के लिए मजबूर किया जाए।
• प्रमाण एक वस्तु के रूप में (Proofs as Objects): HOPSCOTCH में, एक प्रमाण केवल टेक्स्ट का ढेर नहीं है। यह एक संरचित वस्तु है, जैसे कि लेगो (Lego) मॉडल। खेल में प्रत्येक "हॉप" एक विशिष्ट लेगो ईंट है। आप उन्हें एक साथ जोड़ सकते हैं, और कंप्यूटर जांचता है कि क्या वे पूरी तरह से फिट बैठते हैं। यदि आप दो ऐसी ईंटों को जोड़ने का प्रयास करते हैं जो मेल नहीं खाती हैं, तो कंप्यूटर कहता है, "नहीं, यह काम नहीं करता।"
• "एब्स्ट्रैक्शन" (अमूर्तन) का तरीका: इन प्रमाणों के सबसे कठिन हिस्सों में से एक यह दिखाना है कि दो अलग-अलग दिखने वाले सिस्टम बिल्कुल एक जैसा व्यवहार करते हैं। HOPSCOTCH "स्टेट एब्स्ट्रैक्शन" (अवस्था अमूर्तन) नामक एक चतुर तकनीक का उपयोग करता है। कल्पना कीजिए कि आपके पास दो रोबोट हैं। एक के पास अव्यवस्थित आंतरिक वायरिंग डायग्राम है, और दूसरे के पास एक साफ-सुथरा डायग्राम है। HOPSCOTCH आपको एक मानचित्र (एब्स्ट्रैक्शन फंक्शन) बनाने की अनुमति देता है जो दिखाता है कि अव्यवस्थित तार साफ-सुथरे तारों के अनुरूप कैसे हैं। यदि मानचित्र सही है, तो कंप्यूटर जानता है कि दोनों रोबोटों का व्यवहार समान है, भले ही वे अंदर से अलग दिखते हों।

उन्होंने वास्तव में क्या किया और पाया

लेखकों ने केवल उपकरण नहीं बनाया; उन्होंने इसे परीक्षण के लिए रखा। उन्होंने चार प्रमुख क्रिप्टोग्राफिक अवधारणाओं की सुरक्षा को औपचारिक रूप से सत्यापित करने के लिए HOPSCOTCH का उपयोग किया:

1. एन्क्रिप्ट-देन-मैक (Encrypt-then-MAC): संदेशों को गुप्त और छेड़छाड़-मुक्त (tamper-proof) बनाने का एक तरीका। उन्होंने सिद्ध किया कि यदि अंतर्निहित एन्क्रिप्शन और "टैगिंग" (MAC) सुरक्षित हैं, तो यह पूरी प्रक्रिया भी सबसे स्मार्ट हैकर्स के खिलाफ सुरक्षित है।
2. एल-गैमल एन्क्रिप्शन (ElGamal Encryption): पब्लिक कीज़ का उपयोग करके गुप्त संदेश भेजने का एक प्रसिद्ध तरीका। उन्होंने दिखाया कि कैसे 'डिसिजनल डिफी-हेलमैन (DDH) धारणा' नामक एक कठिन गणितीय समस्या के आधार पर इसकी सुरक्षा को सिद्ध किया जा सकता है।
3. वन-टाइम सीक्रेसी से IND-CPA तक: उन्होंने सिद्ध किया कि यदि कोई सिस्टम एक एकल संदेश के लिए सुरक्षित है, तो इसे कई संदेशों के लिए सुरक्षित बनाया जा सकता है, जो मजबूत एन्क्रिप्शन बनाने के लिए एक महत्वपूर्ण कदम है।
4. GGM कंस्ट्रक्शन: यह GGM विधि एक साधारण रैंडम नंबर जनरेटर को एक जटिल "स्यूडो-रैंडम फंक्शन" (एक नकली रैंडम नंबर जनरेटर जो वास्तविक दिखता है) में बदल देती है। पिछले कंप्यूटर प्रमाण केवल इसके बहुत उथले संस्करणों (जैसे 3-स्टेप ट्री) को संभाल सकते थे। लेखकों ने नॉन-कांस्टेंट डेप्थ (गैर-स्थिर गहराई) के लिए GGM की सुरक्षा सिद्ध करने के लिए HOPSCOTCH का उपयोग किया, जिसका अर्थ है कि यह किसी भी आकार के पेड़ों (trees) के लिए काम करता है। उनकी जानकारी के अनुसार, यह पहली बार है जब एक सामान्य-उद्देश्य वाले कंप्यूटर प्रूफ असिस्टेंट ने इस विशिष्ट, जटिल निर्माण को सफलतापूर्वक सत्यापित किया है।

उन्होंने यह कैसे किया (गेम मैकेनिक्स)

शोध पत्र बताता है कि HOPSCOTCH प्रमाण को विशिष्ट चरणों, या "कंस्ट्रक्टर्स" (निर्माताओं) में तोड़कर काम करता है:

• ऑब्जर्वेशनल इक्विवेलेंस (अवलोकन संबंधी समानता): यह सिद्ध करना कि दो खेल बाहर से देखने में एक जैसे लगते हैं।
• रिडक्शन (न्यूनीकरण): यह दिखाना कि यदि आप गेम A को तोड़ सकते हैं, तो आप गेम B को भी तोड़ सकते हैं।
• हाइब्रिड सीक्वेंस (संकर अनुक्रम): कई छोटे चरणों को एक साथ जोड़ना।

ढांचे में "टैक्टिक्स" (स्वचालित सहायक) शामिल हैं जो इन चरणों को आपके लिए हल करने की कोशिश करते हैं। उदाहरण के लिए, यदि आपको सिद्ध करने की आवश्यकता है कि दो ओरेकल (गेम सिस्टम) एक ही हैं, तो कंप्यूटर स्वचालित रूप से एक "स्टेट एब्स्ट्रैक्शन" मैप खोजने का प्रयास कर सकता है। यदि वह नहीं कर पाता है, तो वह चरण को मानव द्वारा हल करने के लिए छोड़ देता है, लेकिन संरचना को बनाए रखता है ताकि मनुष्य को पता रहे कि वे कहाँ हैं।

लेखकों ने एक "कंप्यूटेशनल साउंडनेस थ्योरम" (संगणनात्मक सुदृढ़ता प्रमेय) भी सिद्ध किया। यह एक फैंसी तरीका है कहने का: "यदि कंप्यूटर कहता है कि यह प्रमाण वैध है, तो यह वास्तव में वास्तविक दुनिया में भी वैध है।" उन्होंने दिखाया कि प्रत्येक प्रमाण वस्तु जिसे HOPSCOTCH बनाता है, उसके लिए आप गणितीय रूप से गणना कर सकते हैं कि एक हैकर को कितना "लाभ" (advantage) मिलेगा, जो प्रमाण में उपयोग की गई धारणाओं पर आधारित है। यह सुनिश्चित करता है कि कंप्यूटर केवल अपने साथ खेल नहीं खेल रहा है; यह एक वास्तविक, ठोस सुरक्षा गारंटी दे रहा है।

निष्कर्ष

शोध पत्र निष्कर्ष निकालता है कि HOPSCOTCH विशेष सुरक्षा उपकरणों की सुविधा और सामान्य-उद्देश्य वाले गणित सहायकों की शक्ति के बीच के अंतर को सफलतापूर्वक पाटता है। यह क्रिप्टोग्राफरों को ऐसे प्रमाण लिखने की अनुमति देता है जो पढ़ने में आसान, जांचने में आसान और मानवीय त्रुटियों के प्रति कम संवेदनशील हैं। हालांकि लेखक स्वीकार करते हैं कि कंप्यूटर अभी तक यह जांच नहीं पाता है कि "हैकर" पर्याप्त तेजी से चल रहा है या नहीं (एक तकनीकी विवरण जिसे पॉलीनोमियल टाइम कहा जाता है), लेकिन उन्होंने पूरी तरह से स्वचालित, विश्वसनीय सुरक्षा प्रमाणों के लिए आधार तैयार कर दिया है।

उन्होंने भविष्य की ओर भी संकेत दिया है: इन संरचित प्रमाण वस्तुओं के साथ, जल्द ही AI का उपयोग इन प्रमाणों को स्वचालित रूप से लिखने में मदद करने के लिए करना, या सिस्टम को "बुरे आयोजनों" (bad events) और संभाव्यता (probability) से जुड़े अधिक जटिल परिदृश्यों तक विस्तारित करना संभव हो सकता है। लेकिन फिलहाल, मुख्य उपलब्धि स्पष्ट है: उन्होंने एक विश्वसनीय, लचीला और शक्तिशाली तरीका बनाया है जिससे कंप्यूटर हमें यह सिद्ध करने में मदद कर सके कि हमारे डिजिटल रहस्य सुरक्षित हैं।