💻 computer science

Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

यह शोध पत्र प्राइम फील्ड्स (prime fields) पर अंकगणितीय मास्किंग (arithmetic masking) के लिए पहले मशीन-चेक्ड कंपोजिशन थ्योरम्स प्रस्तुत करता है, जो यह सिद्ध करता है कि पाइपलाइन चरणों के बीच फ्रेश रैंडम मास्किंग पिछले चरणों से सुरक्षा स्वतंत्रता सुनिश्चित करती है और माइक्रोसॉफ्ट के एडम्स ब्रिज पीक्यूसी (Adams Bridge PQC) एक्सेलेरेटर में एक गंभीर इंटर-स्टेज मास्किंग दोष का निदान करने के लिए इन औपचारिक परिणामों का उपयोग करता है।

मूल लेखक: Ray Iskander, Khaled Kirah

प्रकाशित 2026-04-29

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Ray Iskander, Khaled Kirah

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

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

कंप्यूटर सुरक्षा की दुनिया में, शोर के दो मुख्य प्रकार होते हैं:

बूलियन शोर (Boolean Noise): स्विचों को चालू/बंद करने (on/off) की तरह। हमारे पास इन स्विचों को सुरक्षित रूप से स्टैक करने के लिए पहले से ही एक आदर्श नियम पुस्तिका मौजूद है।
अरिथमेटिक शोर (Arithmetic Noise): एक घड़ी पर नंबर जोड़ने की तरह (जहाँ 12 + 1 = 1 होता है)। यही वह चीज़ है जिसका आधुनिक "पोस्ट-क्वांटम" क्रिप्टोग्राफी उपयोग करता है। अब तक, हमारे पास इन संख्या-आधारित मास्क को सुरक्षित रूप से स्टैक करने के लिए कोई नियम पुस्तिका नहीं थी।

यह शोध पत्र वह लापता नियम पुस्तिका प्रदान करता है। यहाँ उन्होंने जो पाया है, उसका सरल विवरण दिया गया है।

1. समस्या: "लीकी" (Leaky) मध्य भाग

कल्पना कीजिए कि एक दो-चरणीय फैक्ट्री लाइन है:

स्टेशन A: आपका गुप्त संदेश लेता है, उसमें कुछ शोर जोड़ता है, और उसे आगे भेज देता है।
स्टेशन B: जो स्टेशन A ने भेजा है, उसे लेता है, उसमें और अधिक शोर जोड़ता है, और अंतिम परिणाम भेजता है।

शोधकर्ताओं ने पाया कि इन स्टेशनों को जोड़ने के तरीके में एक खतरनाक खामी थी (एक प्रसिद्ध माइक्रोसॉफ्ट सुरक्षा चिप जिसे "एडम्स ब्रिज" कहा जाता है)।

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

उपमा: कल्पना कीजिए कि स्टेशन A एक ब्लेंडर है। यह आपके गुप्त संदेश को बर्फ के साथ मिलाता है। लेकिन जिस तरह से ब्लेड घूमते हैं, उसके कारण बाहर आने वाले बर्फ के टुकड़े थोड़े असमान होते हैं—कुछ जगहों पर बर्फ अधिक होती है, तो कुछ जगहों पर कम। यदि कोई जासूस (एक हैकर) स्टेशन A और स्टेशन B के ठीक बीच में खड़ा हो जाए और बर्फ के टुकड़ों को गिनने लगे, तो वह आपके गुप्त संदेश के एक हिस्से का अनुमान लगा सकता है। इसे साइड-चैनल अटैक (Side-Channel Attack) कहा जाता है।

2. समाधान: "फ्रेश मास्क" (The Renewal Argument)

इस शोध पत्र का सबसे बड़ा "आहा!" क्षण आश्चर्यजनक रूप से सरल है। उन्होंने सिद्ध किया कि यदि आप स्टेशन A और स्टेशन B के बीच एक नया, बिल्कुल ताज़ा यादृच्छिक मास्क डाल देते हैं, तो समस्या तुरंत समाप्त हो जाती है।

उपमा:

सुधार के बिना: स्टेशन A बर्फ का एक थोड़ा असमान ढेर स्टेशन B को सौंपता है। स्टेशन B उसे ठीक करने की कोशिश करता है, लेकिन असमानता पहले से ही उसमें समा चुकी होती है।
सुधार के साथ: स्टेशन A अपना असमान ढेर एक "रीसेट बटन" को सौंपता है। यह बटन उस ढेर को ताजे पानी की एक बड़ी, पूरी तरह से मिश्रित बाल्टी में डाल देता है (नया मास्क)। अब, जब स्टेशन B उस बाल्टी से एक स्कूप लेता है, तो वह फिर से पूरी तरह से यादृच्छिक (random) हो जाता है।

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

श 3. "1-बिट बैरियर" (The 1-Bit Barrier)

शोधकर्ताओं ने पाया कि इन चिप्स में इस्तेमाल होने वाले विशिष्ट गणित के लिए, शोर अपने आप में कभी भी पूरी तरह से यादृच्छिक नहीं होता है। इसमें 1 बिट तक की जानकारी का "लीक" होता है।

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

4. प्रमाण: मशीन-चेक्ड (Machine-Checked)

लेखकों ने इसे केवल कागज पर नहीं लिखा; उन्होंने अपने तर्क के हर चरण की जांच करने के लिए Lean 4 नामक एक कंप्यूटर प्रोग्राम का उपयोग किया।

उन्होंने 18 विशिष्ट प्रमाण लिखे।
कंप्यूटर ने बिना किसी त्रुटि के और बिना किसी "बाद में करने के लिए" नोट्स (जिन्हें "सॉरी स्टब्स" कहा जाता है) के उन सभी को सत्यापित किया।
इसका अर्थ है कि गणित पूरी तरह से ठोस है। यह केवल एक सिद्धांत नहीं है; यह एक सत्यापित तथ्य है।

5. निदान: माइक्रोसॉफ्ट का चिप क्यों असुरक्षित था?

टीम ने अपने नए नियम को माइक्रोसॉफ्ट के "एडम्स ब्रिज" चिप पर लागू किया।

निष्कर्ष: चिप में दो चरण (बटरफ्लाई और बैरेट) थे लेकिन उनके बीच कोई फ्रेश मास्क नहीं था।
परिणाम: इन दोनों चरणों को जोड़ने वाला तार "लीकी" था। यह समान (uniform) नहीं था। इसने पुष्टि की कि अन्य शोधकर्ताओं ने पावर एनालिसिस (बिजली के उपयोग को मापने) का उपयोग करके इस चिप को सफलतापूर्वक क्यों हैक किया था।
सुधार: शोध पत्र एक सरल सुधार बताता है: चरणों के बीच एक अतिरिक्त रैंडम नंबर जनरेटर और एक घटाव (subtraction) चरण जोड़ें। यह मध्यवर्ती तार को पूरी तरह से सुरक्षित बना देता है।

सारांश

यह शोध पत्र सुरक्षित कंप्यूटर चिप्स के लिए पहेली के एक लापता टुकड़े को हल करता है।

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

संक्षेप में: यदि आप एक बहु-चरणीय प्रक्रिया के माध्यम से एक रहस्य छिपाना चाहते हैं, तो केवल पहले चरण के भेष पर भरोसा न करें। हर चरण के बीच एक नया भेष बदल दें, और रहस्य सुरक्षित रहेगा।

यहाँ शोध पत्र "Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र पोस्ट-क्वांटम क्रिप्टोग्राफी (PQC) हार्डवेयर के औपचारिक सुरक्षा सत्यापन (formal security verification) में एक महत्वपूर्ण अंतराल को संबोधित करता है, विशेष रूप से NIST मानकों (ML-KEM और ML-DSA) में उपयोग किए जाने वाले नंबर थ्योरेटिक ट्रांसफॉर्म (NTT) कार्यान्वयन के लिए।

संदर्भ: NTT के हार्डवेयर कार्यान्वयन साइड-चैनल हमलों (जैसे Differential Power Analysis - DPA) का प्रतिरोध करने के लिए प्राइम फील्ड ( $\mathbb{Z}_q$ ) पर अरिथमेटिक मास्किंग (arithmetic masking) पर निर्भर करते हैं।
अंतराल: जबकि बुलियन मास्किंग ( $GF(2^n)$ पर) की एक परिपक्व संरचना सिद्धांत (NI, SNI, PINI) और मशीन-चेक्ड प्रमाण मौजूद हैं, अरिथमेटिक मास्किंग (प्राइम फील्ड पर) के लिए समान कंपोजिशन थ्योरम का अभाव है।
विशिष्ट समस्या: अरिथमेटिक मास्किंग में, मॉड्यूलर रिडक्शन (जैसे Barrett reduction) जैसे ऑपरेशन मास्क के साथ गैर-तुच्छ (non-trivial) तरीकों से इंटरैक्ट करते हैं। XOR जैसे बुलियन ऑपरेशन के विपरीत, जहाँ मास्किंग पूर्णतः एकरूपता (uniformity) बनाए रखती है, अरिथमेटिक मास्किंग के परिणामस्वरूप गैर-एकरूप आउटपुट वितरण (multiplicity > 1) हो सकता है।
भेद्यता (Vulnerability): पिछले अनुभवजन्य विश्लेषणों और संरचनात्मक अध्ययनों ने माइक्रोसॉफ्ट के "Adams Bridge" PQC एक्सेलेरेटर में कमजोरियों की पहचान की थी, जहाँ पाइपलाइन चरणों के बीच के इंटरमीडिएट वायर (intermediate wires) गैर-एकरूप थे, जिससे DPA हमले संभव हो गए। हालाँकि, यह औपचारिक रूप से समझाने के लिए कि यह क्यों होता है और कंपोजिशन थ्योरम के माध्यम से इसे कैसे ठीक किया जाए, एक औपचारिक सैद्धांतिक स्पष्टीकरण की कमी थी।

2. कार्यप्रणाली (Methodology)

लेखक अरिथमेटिक मास्किंग के लिए कंपोजिशन थ्योरम को व्युत्पन्न करने और सिद्ध करने के लिए Lean 4 प्रूफ असिस्टेंट का उपयोग करके औपचारिक सत्यापन (formal verification) का प्रयोग करते हैं।

औपचारिक मॉडल: वे PF-PINI(k) नामक एक मात्रात्मक सुरक्षा मीट्रिक (quantitative security metric) को परिभाषित करते हैं, जो प्राइम-फील्ड प्रोब आइसोलेटिंग नॉन-इंटरफेरेंस (Prime-Field Probe Isolating Non-Interference) है।
- बाइनरी सुरक्षा अवधारणाओं (सुरक्षित/असुरक्षित) के विपरीत, PF-PINI मास्क स्पेस के सापेक्ष आउटपुट मानों की मल्टीप्लिसिटी (multiplicity) को मापता है।
- $k=1$ पूर्णतः एकरूप वितरण को दर्शाता है।
- $k=2$ अधिकतम मल्टीप्लिसिटी 2 को दर्शाता है, जो प्रति वायर 1 बिट तक की जानकारी लीक कर सकता है।
"रिन्यूअल आर्गुमेंट" (The "Renewal Argument"): मुख्य सैद्धांतिक अंतर्दृष्टि यह है कि दो पाइपलाइन चरणों के बीच एक ताज़ा रैंडम मास्क (fresh random mask) लागू करने से पहले चरण का सुरक्षा पैरामीटर ( $k_1$ ) इंटरमीडिएट वायर से पूरी तरह से "मिटा" (erase) दिया जाता है, चाहे पहले चरण का आउटपुट कितना भी गैर-एकसमान क्यों न हो।
हार्डवेयर ब्रिजिंग: लेखक अमूर्त बीजगणितीय मॉडलों ( $\mathbb{Z}_q$ ) और RTL डिजाइनों में उपयोग किए जाने वाले हार्डवेयर-फेडफुल नेचुरल नंबर अंकगणित (Nat) के बीच के अंतर को औपचारिक रूप से पाटते हैं, विशेष रूप से Barrett reduction के लिए।
सत्यापन का दायरा: संपूर्ण कार्य 18 मशीन-चेक्ड थ्योरम से बना है जिनमें कोई भी sorry स्टब (बिना सिद्ध धारणाएं) नहीं है, जो उच्च-आश्वासन गारंटी सुनिश्चित करता है।

3. प्रमुख योगदान (Key Contributions)

यह शोध पत्र छह प्राथमिक योगदान देता है:

रिन्यूअल थ्योरम (Theorem 4.1): यह सिद्ध करता है कि यदि दो चरणों ( $G_1 \to G_2$ ) के बीच एक ताज़ा रैंडम मास्क लागू किया जाता है, तो इंटरमीडिएट वायर पूर्णतः एकसमान हो जाता है। किसी विशिष्ट इंटरमीडिएट मान को उत्पन्न करने वाले मास्क युग्मों का कार्डिनैलिटी (cardinality) ठीक $q$ है, जो $G_1$ के सुरक्षा पैरामीटर से स्वतंत्र है।
पॉजिटिव कंपोजिशन थ्योरम (Theorem 4.4): यह प्रदर्शित करता है कि एक ताज़ा मास्किंग वाला दो-चरणीय पाइपलाइन PF-PINI( $k_2$ ) को संतुष्ट करता है। कंपोज्ड आउटपुट की सुरक्षा केवल दूसरे चरण के पैरामीटर ( $k_2$ ) पर निर्भर करती है; पहले चरण की कमजोरी ( $k_1$ ) पूरी तरह से मिट जाती है।
नेगेटिव कंपोजिशन थ्योरम (Theorems 5.1–5.3): यह सिद्ध करता है कि ताज़ा मास्किंग के बिना, इंटरमीडिएट वायर पहले चरण की मल्टीप्लिसिटी ( $k_1$ ) को बनाए रखता है। यदि $k_1 > 1$ है, तो वायर गैर-एकसमान है, जो DPA हमलों के लिए एक आवश्यक स्थिति बनाता है।
अल्जेब्रिक-हार्डवेयर ब्रिज (Theorem 6.1): यह औपचारिक रूप से सिद्ध करता है कि अल्जेब्रिक Barrett reduction मैप, मानक स्कोप स्थितियों ( $q \le 2^s$ ) के तहत हार्डवेयर-फेडफुल Nat अंकगणित मैप के समकक्ष है। यह मान्य करता है कि सैद्धांतिक सीमाएँ सीधे सिलिकॉन कार्यान्वयन पर लागू होती हैं।
Adams Bridge निदान: यह थ्योरम को औपचारिक रूप से एडम्स ब्रिज एक्सेलेरेटर का निदान करने के लिए इंस्टैंशिएट करता है। प्रमाण पुष्टि करता है कि ताज़ा इंटर-स्टेज मास्किंग की कमी के कारण Barrett आउटपुट वायर गैर-एकसमान (PF-PINI(2)) रह जाते हैं, जो पूर्ववर्ती अनुभवजन्य DPA हमलों की सफलता की व्याख्या करता है।
यूनिवर्सल 1-बिट बैरियर: यह कम्प्यूटेशनल साक्ष्य प्रदान करता है कि PF-PINI(2) बाउंड मॉड्यूलर रिडक्शन (Barrett और Montgomery दोनों) के लिए सार्वभौमिक है, जो इन ऑपरेशन्स के लिए एक मौलिक "1-बिट बैरियर" का सुझाव देता है।

4. मुख्य परिणाम (Key Results)

कंपोजिशन का औपचारिक प्रमाण: यह शोध पत्र स्थापित करता है कि ताज़ा इंटर-स्टेज मास्किंग अरिथमेटिक गैजेट्स को सुरक्षित रूप से कंपोज़ करने के लिए आवश्यक और पर्याप्त शर्त है।
मात्रात्मक सुरक्षा:
- ताज़ा मास्किंग के साथ: इंटरमीडिएट वायर एकसमान ( $k=1$ ) है। अंतिम आउटपुट दूसरे चरण के पैरामीटर ( $k_2$ ) द्वारा सीमित है।
- ताज़ा मास्किंग के बिना: इंटरमीडिएट वायर गैर-एकसमान (अप तक $k_1$ ) है। यह गैर-एकरूपता ही साइड-चैनल लीकेज का मूल कारण है जो अनुभवजन्य हमलों में देखा गया है।
Adams Bridge समाधान: निदान पुष्टि करता है कि Adams Bridge पाइपलाइन में Butterfly और Barrett चरणों के बीच एक एकल ताज़ा रैंडम मास्क रजिस्टर और एक घटाव (subtraction) ऑपरेशन जोड़ने से, अंतिम आउटपुट सुरक्षा पैरामीटर को बदले बिना, इंटरमीडिएट वायर पर DPA भेद्यता को समाप्त किया जा सकता है।
आर्टिफैक्ट उपलब्धता: पूरा Lean 4 सोर्स कोड, जिसमें 18 थ्योरम और एक रिप्रोडक्शन स्क्रिप्ट शामिल है, सार्वजनिक रूप से उपलब्ध है, जो प्रमाणों के स्वतंत्र सत्यापन की अनुमति देता है।

5. महत्व (Significance)

प्रथम मशीन-चेक्ड अरिथमेटिक कंपोजिशन: यह पहला कार्य है जो प्राइम फील्ड पर अरिथमेटिक मास्किंग के लिए मशीन-चेक्ड कंपोजिशन थ्योरम प्रदान करता है, जो PQC हार्डवेयर सुरक्षा में एक बड़े सैद्धांतिक शून्य को भरता है।
सिद्धांत और व्यवहार को जोड़ना: अमूर्त बीजगणितीय प्रमाणों को हार्डवेयर-फेडफुल अंकगणित से औपचारिक रूप से जोड़कर, यह शोध पत्र वास्तविक दुनिया के सिलिकॉन डिजाइनों को सत्यापित करने के लिए एक कठोर आधार प्रदान करता है, जो अनुभवजन्य परीक्षण से आगे बढ़ता है।
डिज़ाइन गाइडलाइन: यह PQC हार्डवेयर के लिए एक स्पष्ट, प्रमाणित डिज़ाइन नियम स्थापित करता है: हमेशा पाइपलाइन चरणों के बीच ताज़ा मास्किंग डालें। यह सरल आर्किटेक्चरल परिवर्तन यह गारंटी देता है कि कंपोज्ड पाइपलाइन की सुरक्षा केवल अंतिम चरण के सबसे कमजोर लिंक द्वारा निर्धारित होती है, न कि मध्यवर्ती चरणों द्वारा।
साक्ष्यों का अभिसरण: औपचारिक प्रमाण तीन स्वतंत्र पूर्व विश्लेषणों (अनुभवजन्य पावर विश्लेषण, कोड समीक्षा, और स्ट्रक्चरल डिपेंडेंसी विश्लेषण) के साथ पूरी तरह मेल खाता है, जो पुष्टि करता है कि Adams Bridge एक्सेलेरेटर में पहचाना गया आर्किटेक्चरल दोष वास्तव में इसकी भेद्यता का मूल कारण है।

संक्षेप में, यह शोध पत्र पोस्ट-क्वांटम क्रिप्टोग्राफी के नए युग के लिए सुरक्षित, कंपोजेबल और साइड-चैनल-प्रतिरोधी हार्डवेयर एक्सेलेरेटर डिजाइन करने के लिए आवश्यक गणितीय और औपचारिक सत्यापन बैकबोन प्रदान करता है।