词条 | Dolev–Yao model |
释义 |
The Dolev–Yao model[1] is a formal model used to prove properties of interactive cryptographic protocols.[2][3] The networkThe 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 adversaryThe 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, for example, the attacker in ubiquitous computing. The algebraic modelCryptographic 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). RemarkThe 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.[4] 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. See also
References1. ^{{Citation | last1 = Dolev | first1 = D. | last2 = Yao | first2 = A. C. | title = On the security of public key protocols | journal = IEEE Transactions on Information Theory | volume = IT-29 | issue = 2 | url = http://www.cs.huji.ac.il/~dolev/pubs/dolev-yao-ieee-01056650.pdf | pages = 198–208 | year = 1983 | doi = 10.1109/tit.1983.1056650}} {{DEFAULTSORT:Dolev-Yao model}}2. ^{{Citation | last1 = Backes | first1 = Michael | last2 = Pfitzmann | first2 = Birgit | last3 = Waidner | first3 = Michael | title = Soundness Limits of Dolev-Yao Models | url = https://hal.archives-ouvertes.fr/docs/00/08/06/78/PDF/paper6.pdf | series = Workshop on Formal and Computational Cryptography (FCC'06), affiliated with ICALP'06 | year = 2006 }} 3. ^{{Citation | last1 = Chen | first1 = Quingfeng | last2 = Zhang | first2 = Chengqi | last3 = Zhang | first3 = Shichao | title = Secure Transaction Protocol Analysis: Models and Applications | url = https://books.google.com/?id=IMIuV_tUYfMC&printsec=frontcover&dq=secure+transaction+protocol+analysis+models+applications#v=onepage&q&f=false | series = Lecture Notes in Computer Science / Programming and Software Engineering | year = 2008 | isbn = 9783540850731 }} 4. ^{{Citation | contribution = A Computational Interpretation of Dolev-Yao Adversaries | citeseerx = 10.1.1.94.2941 | last1 = Herzog | first1 = Jonathan | year = 2005}} 1 : Computer security |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。