Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)

तकनीकी सारांश: परिमित संस्करण गुण से परे: सिम्बोलिक डिफी-हेलमैन समूह मॉडलों का विस्तार

समस्या विवरण
डिफी-हेलमैन (DH) समूह आधुनिक क्रिप्टोग्राफिक प्रोटोकॉल के आधार हैं, फिर भी अत्याधुनिक सिम्बोलिक प्रोटोकॉल वेरीफायर (जैसे Tamarin, ProVerif, और Maude-NPA) पूर्ण समर्थन करने में अक्षम हैं। हालांकि ये उपकरण घातांक (exponentiation) और घातांकों के गुणन (multiplication of exponents) को मॉडल कर सकते हैं, वे आम तौर पर समूह तत्वों के गुणन (group elements multiplication) को मॉडल नहीं कर पाते हैं, जो घातांकों के योग के अनुरूप होता है। यह सीमा इसलिए उत्पन्न होती है क्योंकि पूर्ण DH समूहों को वर्णित करने वाला समीकरण सिद्धांत (equational theory)—जिसमें वितरकता (distributivity), साहचर्य (associativity), और क्रमविनिमेयता (commutativity) शामिल है—यूनिफिकेशन समस्या को अनिर्णायक (undecidable) और अनंत बनाता है। फलस्वरूप, मौजूदा उपकरण उन प्रोटोकॉल के बारे में तर्क करने में असमर्थ हैं जो मिश्रित समूह तत्वों (जैसे ElGamal एन्क्रिप्शन या MQV की-एक्सचेंज) का निर्माण करते हैं जहाँ विरोधी या ईमानदार पक्ष घातांकों की पूर्ण क्षेत्र संरचना (field structure) का उपयोग करते हैं।

कार्यप्रणाली
लेखक पूर्ण DH समूह संरचना का उपयोग करने वाले प्रोटोकॉल की सुरक्षा गुणों को सत्यापित करने के लिए एक अर्ध-निर्णय प्रक्रिया (semi-decision procedure) प्रस्तावित करते हैं। यह दृष्टिकोण सिम्बोलिक रीजनिंग को बीजगणितीय विधियों के साथ एकीकृत करता है, जिसे Tamarin प्रूवर के एक विस्तार के रूप में लागू किया गया है।

1. सैद्धांतिक आधार: यह कार्य Dougherty और Guttman द्वारा प्रस्तावित रीराइट सिस्टम पर आधारित है, जो AC (associativity and commutativity) के सापेक्ष एक अभिसारी रीराइट सिस्टम ($\to_{DH}$) का उपयोग करके क्षेत्रों (fields) का अनुमान लगाता है। यह सिस्टम पदों (terms) के सामान्य रूपों (normal forms) को परिभाषित करने की अनुमति देता है।
2. गैर-निरसन धारणा (Non-Cancellation Assumption): यह दृष्टिकोण दो प्राथमिक शर्तों पर निर्भर करता है:
   • C1: सभी समूह तत्व एक ही निश्चित समूह से संबंधित हैं जिसका एक सामान्य जनरेटर (generator) है।
   • C2 (गैर-निरसन): सुरक्षा गुणों में ऐसे पद शामिल होते हैं जहाँ उप-पद (subterms) एक दूसरे को निरस्त (cancel) नहीं करते हैं (अर्थात, वे पहचान तत्व 1 या 0 में कम नहीं हो सकते)। यदि यह स्थिति विफल होती है, तो टूल अभी भी वैध हमलों को खोज सकता है, लेकिन सुरक्षा का प्रमाण प्राप्त करने के लिए यह मैन्युअल सत्यापन आवश्यक है कि विशिष्ट पद निरस्त नहीं होते हैं।
3. हाइब्रिड कंस्ट्रेंट सॉल्विंग: मुख्य नवाचार एक संशोधित कंस्ट्रेंट-सॉल्विंग एल्गोरिदम है जो सीधे DH पदों के लिए यूनिफिकेशन से बचता है। इसके बजाय, यह दो-चरणीय प्रक्रिया अपनाता है:
   • सिम्बोलिक यूनिफिकेशन (सरलीकृत सिद्धांत): एल्गोरिदम पहले एक सरलीकृत समीकरण सिद्धांत ($\varepsilon_{simp}$) के भीतर पदों को यूनिफ़ाई करता है जो समूह गुणन ऑपरेटर को बाहर रखता है। यह रूट टर्म्स को मिलाने के लिए Tamarin के मौजूदा यूनिफिकेशन एल्गोरिदमों का उपयोग करने की अनुमति देता है।
   • बीजगणितीय पुनर्निर्माण (Algebraic Reconstruction): एक बार रूट टर्म्स मैच हो जाने के बाद, एल्गोरिदम सिम्बोलिक पदों को बीजगणितीय वस्तुओं (क्षेत्र पर बहुपद/polynomials) के रूप में व्याख्या करता है। यह घातांकों को या तो "लीक" (विरोधी को ज्ञात) या "गुप्त" (secret) के रूप में वर्गीकृत करता है। Gaussian elimination (या गैर-रैखिक मामलों के लिए संभावित रूप से Buchberger's algorithm) का उपयोग करके, सिस्टम यह हल करता है कि क्या गुप्त घातांकों को लीक हुए घातांकों के साथ जोड़कर लक्ष्य पद का पुनर्निर्माण किया जा सकता है।
4. इंडिकेटर फंक्शन: यह निर्धारित करने के लिए कि क्या कोई पद अनुमानित (deducible) है, लेखक एक "इंडिकेटर" फंक्शन को परिभाषित करते हैं। यह एक पद के निर्माण के लिए आवश्यक न्यूनतम गुप्त घटकों की पहचान करता है। यदि कोई भी इंडिकेटर विरोधी के ज्ञान से पुनर्निर्मित नहीं किया जा सकता है, तो पद को अनिर्मित (undeducible) माना जाता है।
5. विरोधी मॉडलिंग: विस्तार एक सक्रिय Dolev-Yao विरोधी का समर्थन करता है जो सभी DH ऑपरेटरों को लागू करने में सक्षम है। कंस्ट्रेंट सॉल्वर विरोधी निष्कर्ष (adversarial deduction) को संभालने के लिए पदों के बहुपद व्याख्या से प्राप्त रैखिक समीकरणों को संतुष्ट करने की जाँच करके काम करता है।

प्रमुख योगदान

• पूर्ण DH सिद्धांत के लिए प्रथम स्वचालित टूल: यह कार्य एक स्वचालित सत्यापन टूल का पहला कार्यान्वयन प्रस्तुत करता है जो पूर्ण डिफी-हेलमैन समूह संरचना, जिसमें समूह तत्व गुणन शामिल है, का उपयोग करने वाले प्रोटोकॉल का तर्क करने में सक्षम है।
• सुसंगतता और पूर्णता (Soundness and Completeness): लेखक सिद्ध करते हैं कि विस्तारित कंस्ट्रेंट सॉल्विंग संबंध गैर-निरसन धारणा के तहत सुसंगत और पूर्ण है। यदि Tamarin एक हमला पाता है, तो वह एक वैध निष्पादन है; यदि यह सुरक्षा सिद्ध करता है, तो सिम्बोलिक मॉडल के भीतर कोई उल्लंघनकारी निष्पादन मौजूद नहीं है।
• Tamarin के साथ एकीकरण: यह दृष्टिकोण Tamarin के कंस्ट्रेंट सॉल्विंग एल्गोरिदम को संशोधित करके लागू किया गया है, जिसमें नए नियम ($C@, C_{Prem}, C=, C_{var}$) जोड़े गए हैं जो मानक यूनिफिकेशन नियमों को DH-सॉर्टेड पदों के लिए बीजगणितीय समाधान चरणों से बदलते हैं।
• मिश्रित सिद्धांतों को संभालना: यह विधि अन्य उपयोगकर्ता-परिभाषित समीकरण सिद्धांतों (जैसे सममित एन्क्रिप्शन, पेयर्स) के साथ पूर्ण DH सिद्धांत को संयोजित करने का समर्थन करती है, जो संयुक्त पदों को "क्लीन" करके किया जाता है—अर्थात, यूनिफिकेशन के लिए DH उप-पदों को ताज़ा वेरिएबल्स से बदलकर और फिर बीजगणितीय समाधान के लिए DH बाधाओं को पुनः पेश करके।

परिणाम और केस स्टडीज
लेखकों ने कई प्रोटोकॉल पर इस कार्यान्वयन का मूल्यांकन किया:

• ElGamal एन्क्रिप्शन: टूल ने ElGamal एन्क्रिप्शन स्कीम की निष्पादन क्षमता और गोपनीयता को सफलतापूर्वक सिद्ध किया। विशेष रूप से, यह पहली बार है जब पूर्ण DH समर्थन के साथ सिम्बोलिक मॉडल में ElGamal को स्वचालित रूप से सत्यापित किया गया है। टूल ने यह भी सही ढंग से पहचाना कि जब आरंभकर्ता (initiator) प्रमाणित नहीं होता है, तो गोपनीयता का अभाव होता है।
• MQV की-एक्सचेंज: टूल का उपयोग MQV प्रोटोकॉल के विश्लेषण के लिए किया गया था। इसने सफलतापूर्वक Kaliski द्वारा ज्ञात "अननोन की-शेयर" (unknown key-share) हमले को पुनः खोजा, जो मिश्रित समूह तत्वों वाले जटिल हमलों को खोजने की टूल की क्षमता को प्रदर्शित करता है।
• बेंचमार्क मूल्यांकन: विस्तार का परीक्षण 20 मौजूदा Tamarin मॉडलों (WireGuard और विभिन्न की-एक्सचेंज प्रोटोकॉल सहित) पर किया गया था जो पहले एक प्रतिबंधित DH सिद्धांत का उपयोग करते थे। परिणामों ने दिखाया कि विस्तार इन प्रोटोकॉल के लिए प्रतिबंधित सिद्धांत के समान सुरक्षा निर्णय प्रदान करता है, हालांकि विस्तारित खोज स्थान की जटिलता के कारण रनटाइम में वृद्धि हुई है।

महत्व
यह शोध पत्र दावा करता है कि यह कार्य सिम्बोलिक प्रोटोकॉल सत्यापन में एक महत्वपूर्ण प्रगति है। पूर्ण DH सिद्धांतों में यूनिफिकेशन की अनिर्णियता को दूर करके, लेखक डिफी-हेलमैन समूहों के व्यापक वर्ग के प्रोटोकॉल के स्वचालित सत्यापन को सक्षम बनाते हैं। ElGamal को स्वचालित रूप से सत्यापित करने और मिनटों के भीतर MQV हमलों को पुनः खोजने की क्षमता दृष्टिकोण की व्यवहार्यता, स्केलेबिलिटी और दक्षता को प्रदर्शित करती है, जो सैद्धांतिक बीजगणितीय गुणों और व्यावहारिक स्वचालित सुरक्षा विश्लेषण के बीच के अंतर को पाटती है।