CAJ | 학술논문

密码协议的描述和分析有两类截然不同的方法：一类以形式化方法为主要手段，另一类以计算复杂性理论为基础．Abadi 和Rogaway首次试图将这两类不同的方法关联起来，证明一个协议在形式化模型下具有某种安全属性，那么在计算模型下也保持相应的安全属性．在这一工作的带动下，形式化方法的计算可靠性研究越来越受到关注，成为密码协议分析研究的一个重要内容．围绕这一热点问题，人们做了大量的工作．该文首先对两类分析方法做概要介绍；其次对形式化分析的计算可靠性研究成果进行分类和总结，并对各种方法的主要思想进行了介绍；最后对该领域未来的研究方向进行了展望．
밀마협의적묘술화분석유량류절연불동적방법：일류이형식화방법위주요수단，령일류이계산복잡성이론위기출．Abadi 화Rogaway수차시도장저량류불동적방법관련기래，증명일개협의재형식화모형하구유모충안전속성，나요재계산모형하야보지상응적안전속성．재저일공작적대동하，형식화방법적계산가고성연구월래월수도관주，성위밀마협의분석연구적일개중요내용．위요저일열점문제，인문주료대량적공작．해문수선대량류분석방법주개요개소；기차대형식화분석적계산가고성연구성과진행분류화총결，병대각충방법적주요사상진행료개소；최후대해영역미래적연구방향진행료전망．
There are two different approaches in analysis of cryptographic protocols.One isbased on formal methods,and the other is based on computational complexity as modern cryptog-raphy does.Abadi and Rogaway tried to reconcile these two approaches in their seminal work.They set up a relation for some formal results that if a security property is proved in formal model,then the corresponding property is also valid in computational model.Motivated by this work,many works appeared in this area.In this survey,we will summarize various approaches oncomputational soundness of formal methods in analysis cryptographic protocols,present theirmain ideas,and point out the future research directions in this area.