Dolev-Yao attacker model और symbolic crypto

1983 में Danny Dolev और Andrew Yao द्वारा प्रस्तावित Dolev-Yao मॉडल, प्रतीकात्मक प्रोटोकॉल विश्लेषण के लिए मानक विरोधी मॉडल है। हमलावर पूरे नेटवर्क को नियंत्रित करता है।

Dolev-Yao हमलावर ये कार्य कर सकता है: किसी भी संदेश को अवरोधित करना, संदेशों को संग्रहित करना, पुराने संदेशों को पुनःप्रेषित करना, ज्ञात घटकों से नए संदेश जाली बनाना, लेकिन अंतर्निहित क्रिप्टोग्राफ़िक आदिमों को तोड़ नहीं सकता।

प्रतीकात्मक मॉडलों में, कूटलेखन एक पूर्ण ब्लैक बॉक्स होता है: हमलावर कुंजी के बिना संदेश को कूटमुक्त नहीं कर सकता, बड़ी संख्याओं का गुणनखंडन नहीं कर सकता और जाली हस्ताक्षर नहीं बना सकता। इससे विश्लेषण सरल हो जाता है, लेकिन कार्यान्वयन-स्तरीय हमले छूट सकते हैं।

संदेशों को पदों के रूप में निरूपित किया जाता है: enc(k, m), sig(sk, m), hash(m), pair(a, b)। हमलावर कुछ पदों को जानता है और निर्धारित नियमों (निगमन नियमों) का उपयोग करके नए पद निकालता है।

हमलावर का ज्ञान निगमन के अंतर्गत बंद होता है: यदि वह enc(k,m) और k जानता है, तो वह m निकाल सकता है। यदि वह pair(a,b) जानता है, तो वह a और b निकाल सकता है। प्रारंभिक ज्ञान का समापन = वह सब कुछ जो हमलावर सीख सकता है।

प्रोटोकॉल सुरक्षा इस प्रकार व्यक्त की जाती है: "किसी भी पहुँच योग्य स्थिति में हमलावर के ज्ञान में गुप्त s कभी शामिल नहीं होता।" गोपनीयता = पहुँच-योग्यता। प्रमाणीकरण = कुछ निश्चित हानिकारक अनुरेख प्रतिरूपों का न होना।

दो-पक्षीय प्रोटोकॉल: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}। पद बीजगणित में: Alice enc(pubkey_B, pair(Na, A)) भेजती है। हम सत्यापित करते हैं कि निष्पादन के बाद केवल B को Na ज्ञात है।

एप्लाइड पाई कलन (Abadi और Fournet, 2001) प्रोटोकॉलों के निरूपण के लिए एक प्रक्रिया बीजगणित है। प्रक्रियाएँ चैनलों के माध्यम से संचार करती हैं; हमलावर सार्वजनिक चैनलों को नियंत्रित करता है। ProVerif और Tamarin इसी औपचारिकता का उपयोग करते हैं।

Dolev-Yao मॉडल में सुरक्षित प्रोटोकॉल तब भी संगणकीय रूप से असुरक्षित हो सकता है, जब उसका क्रिप्टोग्राफिक कार्यान्वयन कमजोर हो। संगणकीय सुदृढ़ता प्रमेय (Cortier आदि) विशिष्ट आदिम वर्गों के लिए इस अंतर को पाटता है।

Dolev-Yao इनका निरूपण नहीं कर सकता: बीजीय गुणधर्म (जैसे, XOR की क्रमविनिमेयता), पार्श्व-चैनल हमले, कार्यान्वयन की त्रुटियाँ या प्रायिकतामूलक विफलताएँ। समीकरणीय सिद्धांत मॉडल जैसे विस्तार कुछ बीजीय गुणधर्मों को सँभालते हैं।

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