1. परिचय
पासवर्ड मैनेजर (PMs) सुरक्षा बढ़ाने के लिए आवश्यक उपकरण हैं, क्योंकि ये मजबूत, अद्वितीय पासवर्डों के उपयोग को संभव बनाते हैं बिना याद रखने के संज्ञानात्मक बोझ के। इनके लाभों के बावजूद, उपयोगकर्ता का विश्वास अपनाने में एक महत्वपूर्ण बाधा बना हुआ है। यह शोधपत्र विश्वास को प्रभावित करने वाली एक महत्वपूर्ण विशेषता को संबोधित करता है: यादृच्छिक पासवर्ड जनन एल्गोरिदम। हम कार्यात्मक शुद्धता और सुरक्षा गुण दोनों को सिद्ध करने के लिए EasyCrypt ढांचे का उपयोग करते हुए एक औपचारिक रूप से सत्यापित संदर्भ कार्यान्वयन प्रस्तावित करते हैं, जिसका लक्ष्य PMs में पासवर्ड जनन के लिए एक विश्वसनीय मानक स्थापित करना है।
2. वर्तमान पासवर्ड जनन एल्गोरिदम
इस अध्ययन ने 15 पासवर्ड मैनेजरों का सर्वेक्षण किया, जिसमें विस्तृत विश्लेषण तीन व्यापक रूप से उपयोग किए जाने वाले, ओपन-सोर्स उदाहरणों पर केंद्रित था: Google Chrome का पासवर्ड मैनेजर, Bitwarden, और KeePass। लक्ष्य सामान्य एल्गोरिदम को समझना और औपचारिक सत्यापन के लिए क्षेत्रों की पहचान करना था।
2.1 पासवर्ड संरचना नीतियाँ
पासवर्ड मैनेजर उपयोगकर्ताओं को नीतियाँ परिभाषित करने की अनुमति देते हैं जो उत्पन्न पासवर्डों को बाधित करती हैं। ये नीतियाँ लंबाई, वर्ण समुच्चय (जैसे, लोअरकेस, अपरकेस, संख्याएँ, विशेष वर्ण), और प्रति समुच्चय न्यूनतम/अधिकतम घटनाएँ निर्दिष्ट करती हैं। PDF में तालिका 1 Chrome, Bitwarden, और KeePass में उपलब्ध विशिष्ट विकल्पों का विवरण देती है, जो अनुमत वर्ण समुच्चय और नीति सूक्ष्मता (जैसे, KeePass कस्टम वर्ण समुच्चय और अपवर्जन परिभाषित करने की अनुमति देता है) में भिन्नताओं को उजागर करती है।
2.2 यादृच्छिक पासवर्ड जनन
Chrome द्वारा उदाहरणित मूल एल्गोरिदम में एक बहु-चरणीय प्रक्रिया शामिल है: 1) न्यूनतम घटनाओं वाले समुच्चयों से यादृच्छिक रूप से वर्ण उत्पन्न करें। 2) शेष लंबाई को उन सभी समुच्चयों के संघ से वर्ण खींचकर भरें जिनकी अधिकतम गिनती तक नहीं पहुँची है। 3) अंतिम स्ट्रिंग पर एक यादृच्छिक क्रमचय लागू करें। इस प्रक्रिया को यादृच्छिकता और नीति अनुपालन के बीच संतुलन बनाना चाहिए।
3. औपचारिक सत्यापन दृष्टिकोण
यह शोधपत्र पासवर्ड जनन एल्गोरिदम को औपचारिक रूप देने और सत्यापित करने के लिए EasyCrypt प्रूफ असिस्टेंट का उपयोग करता है। सत्यापन दो प्रमुख गुणों पर केंद्रित है:
- कार्यात्मक शुद्धता: एल्गोरिदम हमेशा एक ऐसा पासवर्ड उत्पन्न करता है जो उपयोगकर्ता-परिभाषित संरचना नीति को संतुष्ट करता है।
- सुरक्षा (यादृच्छिकता): आउटपुट पासवर्ड, एक क्रिप्टोग्राफिक रूप से सुरक्षित यादृच्छिक संख्या जनरेटर (CSPRNG) मानते हुए, नीति-परिभाषित वर्णमाला से खींची गई समान लंबाई की पूर्णतः यादृच्छिक स्ट्रिंग से कम्प्यूटेशनल रूप से अविभेद्य है। इसे गेम-आधारित क्रिप्टोग्राफिक प्रूफ दृष्टिकोण का उपयोग करके मॉडल किया गया है।
यह औपचारिक विधि पारंपरिक परीक्षण से आगे बढ़कर, एल्गोरिदम के व्यवहार के बारे में गणितीय गारंटी प्रदान करती है।
4. तकनीकी विवरण और गणितीय सूत्रीकरण
सुरक्षा गुण को एक क्रिप्टोग्राफिक गेम के रूप में औपचारिक रूप दिया गया है। मान लीजिए $\mathcal{A}$ एक संभाव्य बहुपद-समय (PPT) प्रतिद्वंद्वी है। मान लीजिए $\text{Gen}(policy)$ पासवर्ड जनन एल्गोरिदम है और $\text{Random}(policy)$ एक आदर्श जनरेटर है जो $policy$ को संतुष्ट करने वाली सभी स्ट्रिंग्स से एक समान रूप से यादृच्छिक स्ट्रिंग आउटपुट करता है। $\mathcal{A}$ की उनके बीच अंतर करने में लाभ को इस प्रकार परिभाषित किया गया है:
$\text{Adv}_{\text{Gen}}^{\text{dist}}(\mathcal{A}) = |\Pr[\mathcal{A}(\text{Gen}(policy)) = 1] - \Pr[\mathcal{A}(\text{Random}(policy)) = 1]|$
एल्गोरिदम को सुरक्षित माना जाता है यदि यह लाभ सभी PPT प्रतिद्वंद्वियों $\mathcal{A}$ के लिए नगण्य है, अर्थात $\text{Adv}_{\text{Gen}}^{\text{dist}}(\mathcal{A}) \leq \epsilon(\lambda)$, जहाँ $\epsilon$ सुरक्षा पैरामीटर $\lambda$ में एक नगण्य फलन है। EasyCrypt में प्रूफ इस लाभ को बाउंड करने के लिए गेमों के एक अनुक्रम (Game$_0$, Game$_1$, ...) का निर्माण करता है, जो अक्सर इस धारणा पर निर्भर करता है कि अंतर्निहित PRG सुरक्षित है।
5. प्रायोगिक परिणाम और चार्ट विवरण
जबकि PDF मुख्य रूप से औपचारिक विशिष्टीकरण और प्रूफ रणनीति पर केंद्रित है, व्यावहारिक परिणाम एक सत्यापित संदर्भ कार्यान्वयन है। "प्रयोग" EasyCrypt वातावरण में औपचारिक प्रूफ का सफल समापन है। यह शुद्धता के लिए एक खाका के रूप में कार्य करता है।
संकल्पनात्मक चार्ट विवरण: एक फ्लोचार्ट सत्यापित एल्गोरिदम को प्रभावी ढंग से दृश्यमान बना सकता है:
- प्रारंभ: उपयोगकर्ता नीति इनपुट करता है (लंबाई L, वर्ण समुच्चय S1...Sn न्यूनतम/अधिकतम गिनती के साथ)।
- चरण 1 - न्यूनतम पूर्ति: प्रत्येक समुच्चय Si के लिए जहाँ min_i > 0 है, Si से min_i यादृच्छिक वर्ण उत्पन्न करें। काउंटर: $\sum min_i$ वर्ण उत्पन्न हुए।
- चरण 2 - लंबाई L तक भरें: मान लीजिए $\text{Remaining} = L - \sum min_i$। जब तक Remaining > 0: उन सभी समुच्चयों Si से एक पूल बनाएँ जहाँ current_count(Si) < max_i। इस पूल से एक यादृच्छिक वर्ण चुनें। Remaining घटाएँ।
- चरण 3 - फेरबदल: L वर्णों की सूची पर एक क्रिप्टोग्राफिक रूप से सुरक्षित यादृच्छिक क्रमचय (फिशर-येट्स शफल) लागू करें।
- चरण 4 - आउटपुट: अंतिम फेरबदल स्ट्रिंग आउटपुट करें। इस चरण पर हरे रंग का चेकमार्क "औपचारिक रूप से सत्यापित (EasyCrypt): शुद्धता और यादृच्छिकता" लेबल किया गया है।
6. विश्लेषण ढाँचा: उदाहरण केस
परिदृश्य: यह सत्यापित करना कि जब "समान वर्णों को बाहर करें" विकल्प (जैसे, 'l', 'I', 'O', '0' को बाहर करना) सक्षम हो, तो एल्गोरिदम एक सूक्ष्म पूर्वाग्रह से बचता है।
संभावित दोष (सत्यापन के बिना): एक अनाड़ी कार्यान्वयन पहले पूर्ण समुच्चय से एक पासवर्ड उत्पन्न कर सकता है और फिर बाहर किए गए वर्णों को हटा सकता है, जिसके परिणामस्वरूप एक छोटा पासवर्ड हो सकता है या शेष वर्ण समुच्चयों के वितरण को बदल सकता है, जिससे नीति का उल्लंघन हो सकता है या पूर्वाग्रह पैदा हो सकता है।
औपचारिक सत्यापन दृष्टिकोण: EasyCrypt में, हम वर्ण समुच्चय को $\text{Alphabet}_{\text{final}} = \text{Alphabet}_{\text{full}} \setminus \text{ExcludedSet}$ के रूप में निर्दिष्ट करेंगे। तब प्रूफ यह प्रदर्शित करेगा कि जनन प्रक्रिया (उपरोक्त चरण 1 और 2) संबंधित वर्ण समुच्चयों के लिए $\text{Alphabet}_{\text{final}}$ से समान रूप से नमूना लेती है, और न्यूनतम/अधिकतम बाधाओं का मूल्यांकन इस कम किए गए समुच्चय के विरुद्ध सही ढंग से किया जाता है। यह निर्माण द्वारा दोष को समाप्त कर देता है।
गैर-कोड आर्टिफैक्ट: वर्ण चयन चरण के लिए EasyCrypt में औपचारिक विशिष्टीकरण तार्किक रूप से सैंपलिंग पूल को परिभाषित करेगा, यह सुनिश्चित करते हुए कि बाहर किए गए वर्ण कभी भी स्रोत का हिस्सा नहीं होते।
7. मूल अंतर्दृष्टि और विश्लेषक का परिप्रेक्ष्य
मूल अंतर्दृष्टि: इस शोधपत्र का मौलिक योगदान पासवर्ड मैनेजरों के लिए विश्वास मॉडल को "कोड समीक्षा और परीक्षण के माध्यम से संभवतः सुरक्षित" से "औपचारिक सत्यापन के माध्यम से गणितीय रूप से सिद्ध सुरक्षित" में बदलना है। यह पासवर्ड जनरेटर को विश्वास की एक कुंजी के रूप में सही ढंग से पहचानता है—एकल विफलता बिंदु जो, यदि दोषपूर्ण है, तो मैनेजर की संपूर्ण सुरक्षा आधार को कमजोर कर देता है। यह कार्य अनुप्रयुक्त क्रिप्टोग्राफी में एक महत्वपूर्ण लेकिन कम सराहे गए रुझान का हिस्सा है, जो TLS प्रोटोकॉल (प्रोजेक्ट एवरेस्ट) या क्रिप्टोग्राफिक लाइब्रेरीज (HACL*) के औपचारिक सत्यापन जैसे प्रयासों को दर्पण करता है।
तार्किक प्रवाह: तर्क ठोस है: 1) अपारदर्शी सुरक्षा के कारण उपयोगकर्ता विश्वास कम है। 2) पासवर्ड जनन एक महत्वपूर्ण, जटिल घटक है जो सूक्ष्म बग (जैसे, पूर्वाग्रह, नीति उल्लंघन) के प्रति संवेदनशील है। 3) औपचारिक विधियाँ उच्चतम आश्वासन प्रदान करती हैं। 4) EasyCrypt इस सत्यापन के लिए एक व्यावहारिक ढाँचा प्रदान करता है। 5) एक सत्यापित संदर्भ कार्यान्वयन उद्योग के लिए एक स्वर्ण मानक के रूप में कार्य कर सकता है।
शक्तियाँ और दोष: शक्तियाँ: एक ठोस, उच्च-प्रभाव वाली समस्या पर ध्यान केंद्रित करना उत्कृष्ट है। गेम-आधारित प्रूफ के लिए एक परिपक्व उपकरण EasyCrypt का उपयोग करना व्यावहारिक है। वास्तविक दुनिया के PM एल्गोरिदम का विश्लेषण शोध को व्यवहार में आधारित करता है। दोष: यह शोधपत्र एक "की ओर" शोधपत्र है—यह आधार तैयार करता है लेकिन किसी प्रमुख PM की सभी नीतियों के लिए एक पूर्ण, युद्ध-परीक्षित सत्यापित कार्यान्वयन प्रस्तुत नहीं करता। वास्तविक चुनौती वाणिज्यिक पासवर्ड नीतियों (जैसे KeePass के व्यापक विकल्प) की जटिलता है, जो सत्यापन राज्य स्थान को विस्फोटित कर सकती है। यह कमरे में हाथी को भी नजरअंदाज करता है: आसपास के PM सिस्टम (UI, मेमोरी, स्टोरेज, ऑटो-फिल) की सुरक्षा समान रूप से महत्वपूर्ण है, जैसा कि NCC Group जैसे संगठनों के अध्ययनों में उल्लेख किया गया है।
कार्रवाई योग्य अंतर्दृष्टि: 1) PM विक्रेताओं के लिए: इस सत्यापित संदर्भ कार्यान्वयन को अपनाएँ या इसके विरुद्ध क्रॉस-चेक करें। पूर्ण UI नीति इंजन के अविश्वसनीय रहने पर भी, मूल जनन तर्क को सत्यापित करके प्रारंभ करें। 2) सुरक्षा ऑडिटरों के लिए: मूल क्रिप्टोग्राफिक मॉड्यूल के लिए औपचारिक सत्यापन की मांग करें, इसे समीक्षित क्रिप्टोग्राफिक आदिमों का उपयोग करने के समान एक नए सर्वोत्तम अभ्यास के रूप में मानें। 3) शोधकर्ताओं के लिए: इस कार्य का विस्तार करके जनरेटर के CSPRNG और सिस्टम एन्ट्रॉपी स्रोतों के साथ एकीकरण को सत्यापित करें—एक श्रृंखला उतनी ही मजबूत होती है जितनी उसकी सबसे कमजोर कड़ी। इस क्षेत्र को सत्यापित एंड-टू-एंड घटकों के लिए लक्ष्य रखना चाहिए, जैसे seL4 जैसे सत्यापित ऑपरेटिंग सिस्टम के पीछे की दृष्टि।
8. अनुप्रयोग संभावनाएँ और भविष्य की दिशाएँ
तत्काल अनुप्रयोग पासवर्ड जनन के लिए एक ड्रॉप-इन, सत्यापित लाइब्रेरी का निर्माण है जिसे Bitwarden और KeePass जैसे ओपन-सोर्स पासवर्ड मैनेजरों में एकीकृत किया जा सकता है, जिससे उनकी विश्वसनीयता में काफी वृद्धि होगी। आगे देखते हुए:
- मानकीकरण: यह कार्य क्रिप्टोग्राफिक रूप से सुरक्षित पासवर्ड जनन के लिए एक औपचारिक मानक (जैसे, एक IETF RFC) के विकास को सूचित कर सकता है, NIST SP 800-63B के समान लेकिन सत्यापनीय कार्यान्वयन के साथ।
- ब्राउज़र और OS एकीकरण: Chrome, Firefox, और iOS/macOS Keychain जैसे प्रमुख प्लेटफॉर्म सत्यापित जनरेटर अपना सकते हैं, जिससे अरबों उपयोगकर्ताओं के लिए सुरक्षा आधार रेखा बढ़ जाएगी।
- अन्य डोमेन में विस्तार: यह पद्धति अन्य यादृच्छिक स्ट्रिंग जनन आवश्यकताओं, जैसे API कुंजी, टोकन, या रिकवरी कोड उत्पन्न करने के लिए सीधे लागू होती है।
- स्वचालित नीति अनुपालन: भविष्य के उपकरण उपयोगकर्ता-अनुकूलित नीतियों के लिए स्वचालित रूप से औपचारिक प्रूफ उत्पन्न कर सकते हैं, जिससे अद्वितीय नीति आवश्यकताओं वाले उद्यम PMs के लिए उच्च-आश्वासन जनन सुलभ हो जाएगा।
- संकर दृष्टिकोण: औपचारिक सत्यापन को PM स्टैक के अविश्वसनीय भागों के लिए फज़िंग (जैसे, AFL++ जैसे उपकरणों का उपयोग करके) के साथ जोड़ना एक मजबूत, बहु-स्तरीय रक्षा प्रदान कर सकता है।
अंतिम दिशा संपूर्ण महत्वपूर्ण सुरक्षा उपतंत्रों का क्रमिक औपचारिक सत्यापन है, जो उद्योग को प्रतिक्रियाशील पैचिंग से सक्रिय रूप से सिद्ध सुरक्षा की ओर ले जाता है।
9. संदर्भ
- Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Towards Formal Verification of Password Generation Algorithms used in Password Managers. arXiv preprint arXiv:2106.03626.
- Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., & Strub, P. Y. (2014). EasyCrypt: A framework for formal cryptographic proofs. Journal of Cryptology.
- Shoup, V. (2004). Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive.
- NCC Group. (2023). Password Manager Security Review. Retrieved from https://www.nccgroup.com
- Klein, G., et al. (2009). seL4: Formal verification of an OS kernel. Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles.
- National Institute of Standards and Technology (NIST). (2017). Digital Identity Guidelines: Authentication and Lifecycle Management (SP 800-63B).