Долев-Яо моделі: интерактивті криптографиялық протоколдарды формалды түрде модельдеу
Dolev–Yao model
Долев-Яо моделі – интерактивті криптографиялық протоколдарды зерттеуге арналған формалды модель. Желі абстракті машиналармен хабар алмасады, қауіпсіздікті бағалайды.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Долев-Яо моделі, оның авторлары Дэнни Долев және Эндрю Яоның есімдерімен аталады, өзара әрекеттесетін криптографиялық протоколдардың қасиеттерін дәлелдеуге қолданылатын формалды модель.
The Dolev–Yao model, named after its authors Danny Dolev and Andrew Yao, is a formal model used to prove properties of interactive cryptographic protocols.
Желілік
Желі абстрактілі машиналар жиынтығымен бейнеленеді, олар хабар алмаса алады. Бұл хабарлар формалды терминдерден құралған. Бұл терминдер хабарлардың ішкі құрылымының бір бөлігін ашады, бірақ кейбір бөліктері қарсыластан жасырылуы тиіс.
The network is represented by a set of abstract machines that can exchange messages. These messages consist of formal terms. These terms reveal some of the internal structure of the messages, but some parts will hopefully remain opaque to the adversary.
Қарсылас
Бұл модельдегі қарсылас кез келген хабарламаны тыңдай, тоқтата, және жасауға қабілді, және оның мүмкіндіктері қолданылған криптографиялық әдістердің шектеулерімен ғана анықталады. Басқаша айтқанда: "шабуылшы хабарды өздігінен жеткізеді". Мұндай шексіз күшті модельдеу өте қиындық тудырды, сондықтан көптеген қауіп модельдері оны қарапайымдастырады, сияқты, кең таралған есептеу ортасындағы шабуылшы үшін жасалған модельдерде.
The adversary in this model can overhear, intercept, and synthesize any message and is only limited by the constraints of the cryptographic methods used. In other words: "the attacker carries the message." This omnipotence has been very difficult to model, and many threat models simplify it, as has been done for the attacker in ubiquitous computing.
Алгебралық модель
Криптографиялық примитивтер абстрактілі операторлармен модельделеді. Мысалы, пайдаланушы үшін асимметриялық шифрлеу шифрлеу функциясымен және шифрлеуді шешу функциясымен көрсетіледі. Олардың негізгі қасиеттері – олардың композициясы сәйкестік функциясы болып табылады және шифрланған хабарлама туралы ешқандай ақпаратты ашпайды. Нақты әлемнен өзгеше, қарсылас шифрлеудің биттік өрнегін өзгерте алмайды және кілтті болжай алмайды. Дегенмен, шабуылшы жіберілген және осылайша белгілі болған кез келген хабарламаны қайта пайдалана алады. Шабуылшы оларды өзі білген кез келген кілттермен шифрлей немесе шеше алады, содан кейін келесі хабарламаларды жалғандауға болады. Протокол – сұраулардың (желі арқылы хабарлама жіберу) және жауаптардың (желіден хабарлама алу) арасында кезектесіп алмасатын, бірінен соң бірі орындалатын орындалулар жиынтығы ретінде модельделеді.
Cryptographic primitives are modeled by abstract operators. For example, asymmetric encryption for a user is represented by the encryption function and the decryption function Their main properties are that their composition is the identity function and that an encrypted message reveals nothing about Unlike in the real world, the adversary can neither manipulate the encryption's bit representation nor guess the key. The attacker may, however, re use any messages that have been sent and therefore become known. The attacker can encrypt or decrypt these with any keys he knows, to forge subsequent messages. A protocol is modeled as a set of sequential runs, alternating between queries (sending a message over the network) and responses (obtaining a message from the network).
Ескертпе
Долев-Яо моделінің символдық сипаты оны есептеу модельдерімен салыстырғанда басқаруға оңай және алгебралық әдістерге қолжетімді етеді, бірақ оның нақтылығы төмен болуы мүмкін. Дегенмен, криптографиялық протоколдарға арналған екі модель де байланысты. Сондай-ақ, символдық модельдер шабуылшының қабілеттері туралы жасалған болжамдар негізінде протоколдың қауіпсіз емес, бұзылғанын көрсетуге өте ыңғайлы.
The symbolic nature of the Dolev–Yao model makes it more manageable than computational models and accessible to algebraic methods but potentially less realistic. However, both kinds of models for cryptographic protocols have been related. Also, symbolic models are very well suited to show that a protocol is broken, rather than secure, under the given assumptions about the attackers capabilities.