💻 computer science

Formal Verification of Probing Security via Conditional Independence

यह शोधपत्र नॉन-इंटरफेरेंस गुणों और कंडीशनल इंडिपेंडेंस के बीच संबंध स्थापित करने के लिए प्रोबेबिलिस्टिक सेपरेशन लॉजिक (Lilac) का लाभ उठाते हुए, मास्क्ड क्रिप्टोग्राफिक एल्गोरिदम की प्रोबिंग सुरक्षा के लिए एक नवीन औपचारिक सत्यापन दृष्टिकोण प्रस्तावित करता है।

मूल लेखक: Satoshi Kura, Katsuyuki Takashima

प्रकाशित 2026-05-25

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

CC BY 4.0

मूल लेखक: Satoshi Kura, Katsuyuki Takashima

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

कल्पना कीजिए कि आप एक व्यस्त, शोर वाले रसोईघर में एक गुप्त रेसिपी को सुरक्षित रखने की कोशिश कर रहे हैं। क्रिप्टोग्राफी की दुनिया में, यह "गुप्त रेसिपी" एक प्राइवेट की (private key) है, और "शोर" एक साइड-चैनल अटैक (side-channel attack) है। हमलावर गणित को तोड़ने की कोशिश नहीं कर रहे हैं; वे "लीक्स" (जैसे बिजली का उपयोग या टाइमिंग) पर नज़र रखने की कोशिश कर रहे हैं ताकि आपके गुप्त डेटा का अनुमान लगाया जा सके जबकि कंप्यूटर नंबरों की गणना कर रहा होता है।

इसे रोकने के लिए, क्रिप्टोग्राफर्स मास्किंग (Masking) नामक एक तकनीक का उपयोग करते हैं। मास्किंग को ऐसे समझें जैसे आप अपनी गुप्त रेसिपी को कागज के $t+1$ टुकड़ों (शेयर्स) में फाड़ रहे हैं। आप इन टुकड़ों में से एक-एक हिस्सा $t+1$ अलग-अलग शेफ को देते हैं। जब तक कोई जासूस केवल $t$ टुकड़ों (या उससे कम) को देख पाता है, तब तक उसे केवल रैंडम कचरा ही दिखाई देता है। वे रेसिपी को फिर से नहीं बना सकते क्योंकि उनके पास कम से कम एक महत्वपूर्ण टुकड़ा गायब है।

हालांकि, यह प्रमाणित करना कि एक जटिल रेसिपी (एल्गोरिदम) वास्तव में सुरक्षित है, अत्यंत कठिन है। यदि आप इसे हाथ से जांचने की कोशिश करते हैं, तो आप एक मामूली लीक को भी मिस कर सकते हैं, और पूरा सुरक्षा तंत्र विफल हो सकता है। यहीं पर यह पेपर काम आता है।

समस्या: "लीक" की जांच करना

लेखक एक औपचारिक प्रमाण (formal proof) (एक गणितीय गारंटी) बनाना चाहते हैं कि एक मास्क्ड एल्गोरिदम सुरक्षित है। पारंपरिक रूप से, यह "सिम्युलेटर" (Simulator) की अवधारणा का उपयोग करके किया जाता है।

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

लेकिन इन सिम्युलेटर्स को हाथ से बनाना त्रुटिपूर्ण हो सकता है। लेखक एक बेहतर तरीका चाहते थे।

समाधान: एक नया लॉजिक टूल (Lilac)

लेखक "सिम्युलेटर्स" और "कंडीशनल इंडिपेंडेंस (Conditional Independence)" नामक एक अवधारणा के बीच संबंध पेश करते हैं।

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

यह पेपर सिद्ध करता है कि यदि एक सिम्युलेटर मौजूद है, तो सार्वजनिक जानकारी के आधार पर, गुप्त जानकारी लीक से "कंडीशनली इंडिपेंडेंट" है।

इसे गणितीय रूप से जांचने के लिए, वे Lilac नामक एक टूल का उपयोग करते हैं।

Lilac क्या है? Lilac को प्रायिकता (probability) के एक बहुत ही सख्त, सुपर-पावर्ड नियम पुस्तिका के रूप में समझें। यह एक लॉजिक गेम की तरह है जहाँ आपको यह साबित करना होता है कि कार्डों के दो ढेर एक-दूसरे से स्वतंत्र रूप से शफल किए गए हैं।
"सेपरेटिंग कंजंक्शन" (Separating Conjunction): इस नियम पुस्तिका में, एक विशेष प्रतीक (एक जादुई छड़ी की तरह) है जो कहता है, "ये दो कार्डों के ढेर पूरी तरह से अलग हैं और एक-दूसरे को प्रभावित नहीं करते हैं।"
नवाचार: लेखकों ने इस नियम पुस्तिका में "कंडीशनिंग" (अर्थात "के आधार पर..." वाला हिस्सा) को संभालने के लिए नए नियम जोड़े हैं। यह उन्हें यह प्रमाणित करने की अनुमति देता है कि भले ही जासूस कुछ डेटा देखता है, वह गुप्त जानकारी को प्रकट नहीं करता क्योंकि उसके पास पहले से ही सार्वजनिक डेटा मौजूद है।

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

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

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

मुख्य निष्कर्ष

पेपर का दावा है कि "सिम्युलेटर्स" के जटिल विचार को "कंडीशनल इंडिपेंडेंस" की भाषा में अनुवाद करके, वे इस नए लॉजिकल फ्रेमवर्क का उपयोग करके इन क्रिप्टोग्राफिक टूल्स की सुरक्षा को स्वचालित और कठोर रूप से सत्यापित कर सकते हैं।

उन्होंने MINIADDREP_NOISE, REFRESH, और SECMULT के लिए औपचारिक प्रमाण लिखकर इसे सफलतापूर्वक प्रदर्शित किया, जिससे यह दिखाया गया कि ये विशिष्ट एल्गोरिदम साइड-चैनल हमलों के खिलाफ गुप्तों की रक्षा के लिए आवश्यक सख्त सुरक्षा आवश्यकताओं को पूरा करते हैं। उन्होंने यह दावा नहीं किया कि वे भविष्य की सभी सुरक्षा समस्याओं को ठीक कर देंगे या इसे मेडिकल डिवाइस पर लागू करेंगे; उनका कार्य पूरी तरह से इस नए लॉजिकल फ्रेमवर्क का उपयोग करके इन विशिष्ट क्रिप्टोग्राफिक गणितीय ऑपरेशन्स की सुरक्षा को सिद्ध करने के बारे में है।

तकनीकी सारांश: कंडीशनल इंडिपेंडेंस के माध्यम से प्रोबिंग सुरक्षा का औपचारिक सत्यापन

समस्या विवरण

साइड-चैनल हमले क्रिप्टोग्राफिक स्कीम्स के लिए एक महत्वपूर्ण खतरा पैदा करते हैं, जिससे मास्किंग (masking) को एक व्यापक उपाय के रूप में अपनाया जाता है। मास्किंग गुप्त मानों (secret values) को शेयरों (shares) में विभाजित करती है ताकि यह सुनिश्चित किया जा सके कि मध्यवर्ती मानों के किसी भी उपसमूह से होने वाला रिसाव (leakage) अंतर्निहित गुप्त मान को प्रकट न कर सके। हालांकि, मास्क्ड एल्गोरिदम की सुरक्षा को प्रमाणित करना, विशेष रूप से ISW प्रोबिंग मॉडल (जहाँ एक एडवरसरी $t$ मध्यवर्ती मानों तक प्रोब कर सकता है) के तहत, मैन्युअल रूप से करना त्रुटिपूर्ण होता है। मैन्युअल सुरक्षा प्रमाणों में कई खामियां पाई गई हैं, जिसके लिए औपचारिक सत्यापन (formal verification) की आवश्यकता है।

जबकि प्रोबेबिलिस्टिक सेपरेशन लॉजिक (probabilistic separation logic) का उपयोग इनपुट स्वतंत्रता (जैसे, वन-टाइम पैड्स में) जैसे गुणों को सत्यापित करने के लिए सफलतापूर्वक किया गया है, इसका उपयोग अभी तक मास्क्ड एल्गोरिदम की प्रोबिंग सुरक्षा (विशेष रूप से $t$ -noninterference) को सत्यापित करने के लिए नहीं किया गया है। मौजूदा औपचारिक सत्यापन उपकरण अक्सर प्रतिस्थापन-आधारित (substitution-based) विधियों या टाइप इन्फरेंस (type inference) पर निर्भर करते हैं, जिनमें जटिल कंडीशनल इंडिपेंडेंस रीजनिंग के लिए आवश्यक मॉड्यूलरिटी या अभिव्यक्तता (expressiveness) की कमी हो सकती है।

कार्यप्रणाली

यह कार्य सिम्युलेटर-आधारित सुरक्षा परिभाषाओं और कंडीशनल इंडिपेंडेंस (conditional independence) के बीच एक कठोर संबंध स्थापित करके औपचारिक सत्यापन के लिए एक नवीन दृष्टिकोण प्रस्तावित करता है। कार्यप्रणाली Lilac पर आधारित है, जो कंडीशनल इंडिपेंडेंस के बारे में तर्क करने के लिए डिज़ाइन किया गया एक प्रोबेबिलिस्टिक सेपरेशन लॉजिक है।

1. सैद्धांतिक आधार: सिम्युलेटर्स और कंडीशनल इंडिपेंडेंस

लेखक नॉन-इंटरफेरेंस (noninterference) की मानक सिम्युलेटर-आधारित परिभाषा को कंडीशनल इंडिपेंडेंस के संदर्भ में पुनर्गठित करते हैं।

सिम्युलेटर-आधारित दृश्य: एक मास्क्ड एल्गोरिदम सुरक्षित है यदि, प्रोब्स के किसी भी सेट $O$ (जो एडवरसरी द्वारा देखे गए हैं) के लिए, एक सिम्युलेटर मौजूद है जो शेष गुप्त शेयरों तक पहुँच के बिना, केवल इनपुट शेयरों के एक उपसमूह $I$ का उपयोग करके $O$ के वितरण (distribution) को उत्पन्न कर सकता है।
कंडीशनल इंडिपेंडेंस दृश्य: यह सुरक्षा आवश्यकता इस कथन के समकक्ष है कि देखे गए मान $O$ , सार्वजनिक इनपुट शेयरों $I$ के दिए जाने पर, गुप्त इनपुट शेयरों ( $\Delta \setminus I$ ) से कंडीशनली इंडिपेंडेंट हैं। औपचारिक रूप से, इसे $O \perp (\Delta \setminus I) \mid I$ के रूप में व्यक्त किया जाता है।

यह शोध पत्र प्रदर्शित करता है कि यह समानता Lilac के सिमेंटिक फ्रेमवर्क के भीतर बनी रहती है, जो स्वतंत्र संयोजनों (independent combinations) के माध्यम से प्रोबेबिलिस्टिक इंडिपेंडेंस को मॉडल करता है और डिसइंटिग्रेशन (disintegration) के माध्यम से कंडीशनिंग करता है।

2. Lilac का विस्तार

Lilac को प्रोबिंग सुरक्षा के लिए लागू करने हेतु, लेखक इसे विशिष्ट प्रूफ़ नियमों के साथ विस्तारित करते हैं जो मूल Lilac फॉर्मूलेशन में मौजूद नहीं थे:

सेमी-ग्राफॉइड एक्सिओम्स (Semi-Graphoid Axioms): यह शोध पत्र सिद्ध करता है कि कंडीशनल इंडिपेंडेंस के लिए सेमी-ग्राफॉइड एक्सिओम्स (Symmetry, Decomposition, Weak Union, और Contraction) Lilac के सिमेंटिक्स के भीतर मान्य हैं। ये एक्सिओम्स प्रमाणों के दौरान कंडीशनल इंडिपेंडेंस कथनों को हेरफेर करने के लिए महत्वपूर्ण हैं।
कंपोजेबिलिटी नियम (Composability Rules): नॉन-इंटरफेरेंस गुणों के कंपोजिशन को संभालने के लिए नए नियम पेश किए गए हैं, विशेष रूप से अनुक्रमिक कंपोजिशन (sequential composition) और फॉर-लूप्स (for-loops) के लिए। ये नियम छोटे गैजेट्स से बने जटिल एल्गोरिदम के मॉड्यूलर सत्यापन की अनुमति देते हैं।
ओनरशिप और वीकनिंग (Ownership and Weakening): अतिरिक्त नियम अनशेयर्ड इनपुट्स (unshared inputs) या वेरिएबल्स के उपसमुच्चयों के साथ काम करते समय रैंडम वेरिएबल्स के स्वामित्व और नॉन-इंटरफेरेंस गुणों के वीकनिंग के बारे में तर्क करने की सुविधा प्रदान करते हैं।

3. सत्यापन फ्रेमवर्क

सत्यापन प्रक्रिया में शामिल हैं:

मास्क्ड एल्गोरिदम (जो प्रोबेबिलिस्टिक प्रोग्रामिंग भाषा APPL में लिखे गए हैं) को Lilac के भीतर होअर ट्रिपल्स (Hoare triples) में अनुवादित करना।
$(I, O)$ -नॉन-इंटरफेरेंस के सत्यापन को एक विशिष्ट कंडीशनल इंडिपेंडेंस होअर ट्रिपल को सिद्ध करने में बदलने के लिए स्थापित समानता (Theorem V.1) का उपयोग करना:
$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$
आवश्यक एंटेलमेंट्स (entailments) को प्राप्त करने के लिए विस्तारित प्रूफ़ नियमों (नए सेमी-ग्राफॉइड और कंपोजेबिलिटी नियमों सहित) को लागू करना।

मुख्य योगदान

औपचारिक संबंध: यह शोध पत्र प्रोबिंग सुरक्षा के सिम्युलेटर-आधारित परिभाषाओं और Lilac में व्यक्त की जा सकने वाली कंडीशनल इंडिपेंडेंस प्रॉपर्टीज के बीच एक औपचारिक समानता स्थापित करता है। यह क्रिप्टोग्राफिक सुरक्षा धारणाओं और प्रोबेबिलिस्टिक सेपरेशन लॉजिक के बीच के अंतर को पाटता है।
Lilac का विस्तार: लेखक मास्क्ड एल्गोरिदम को सत्यापित करने के लिए आवश्यक अतिरिक्त प्रूफ़ नियमों का एक सेट प्रदान करते हैं, जिसमें कंडीशनल इंडिपेंडेंस के लिए सेमी-ग्राफॉइड एक्सिओम्स और अनुक्रमिक कंपोजिशन तथा लूप्स के लिए कंपोजेबिलिटी नियम शामिल हैं।
केस स्टडीज: Lilac का उपयोग करके तीन महत्वपूर्ण एल्गोरिदम की प्रोबिंग सुरक्षा को औपचारिक रूप से सत्यापित करके इस दृष्टिकोण की प्रभावशीलता को प्रदर्शित किया गया है:
- MINIADDREPNOISE: मास्क्ड वैल्यूज में यूनिफॉर्म नॉइज़ जोड़ने के लिए एक सबरूटीन।
- REFRESH: शेयर्स को रिफ्रेश करने के लिए एक मौलिक एल्गोरिदम, जो लीकेज संचय (leakage accumulation) को रोकता है।
- SECMULT: एक मानक मास्क्ड मल्टीप्लिकेशन एल्गोरिदम।
- ADDREPNOISEER: Raccoon सिग्नेचर स्कीम (जो NIST पोस्ट-क्वांटम क्रिप्टोग्राफी मानकीकरण के लिए एक उम्मीदवार है) में उपयोग किया जाने वाला एक वेरिएंट, जो यह सिद्ध करता है कि यह $t$ -Strong Noninterference with Unshared Input ( $t$ -SNIU) गुण को संतुष्ट करता है।

परिणाम

शोध पत्र लक्षित एल्गोरिदम के लिए सफलतापूर्वक होअर ट्रिपल्स को व्युत्पन्न करता है, जिससे उनकी नॉन-इंटरफेरेंस प्रॉपर्टीज की पुष्टि होती है।

MINIADDREPNOISE के लिए, प्रमाण दिखाता है कि आउटपुट शेयर्स, देखे गए इनपुट्स के दिए जाने पर, अनऑब्जर्व्ड इनपुट शेयर्स से कंडीशनली इंडिपेंडेंट हैं।
REFRESH के लिए, प्रमाण यह सत्यापित करता है कि एल्गोरिदम $t$ -Strong Noninterference ( $t$ -SNI) को संतुष्ट करता है, जो कि स्टैंडर्ड नॉन-इंटरफेरेंस से अधिक मजबूत गुण है, और उच्च-क्रम मास्किंग में कंपोजेबिलिटी के लिए आवश्यक है।
SECMULT और ADDREPNOISEER के लिए, प्रमाण इन एल्गोरिदम में निहित नेस्टेड लूप्स और जटिल डेटा डिपेंडेंसी को संभालने के लिए नए कंपोजेबिलिटी नियमों का लाभ उठाते हैं।

ADDREPNOISEER का सत्यापन विशेष रूप से महत्वपूर्ण है क्योंकि यह Raccoon सिग्नेचर स्कीम के सुरक्षा प्रमाण के एक प्रमुख घटक को मान्य करता है, जो $t$ -SNIU गुण पर निर्भर करता है।

महत्व और दावे

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

पेपर इस बात पर जोर देता है कि हालांकि सिम्युलेटर्स को कंडीशनल इंडिपेंडेंस से जोड़ने का मूल विचार वैचारिक रूप से सरल है, लेकिन Lilac में इसका औपचारिकीकरण तकनीकी रूप से गैर-तुच्छ (non-trivial) है क्योंकि यह मानक प्रोडक्ट प्रोबेबिलिटी स्पेस के बजाय स्वतंत्र संयोजनों पर निर्भर करता है। मुख्य प्रमेय का सफल व्युत्पत्ति और वास्तविक दुनिया के क्रिप्टोग्राफिक घटकों (Raccoon) पर इसका अनुप्रयोग यह प्रदर्शित करता है कि यह फ्रेमवर्क जटिल, उच्च-क्रम मास्किंग स्कीम्स को सत्यापित करने के लिए व्यवहार्य है।

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