CAJ | 학술논문

攻击者建模是安全协议验证工作的一个重要部分，直接影响到验证的效率与质量，但目前却还没有一个可遵循的形式化框架，影响了建模工作的准确性与客观性。针对这一问题，通过对在安全协议验证中具有广泛影响的 DY 模型进行形式化，建立了一个 DY 模型的构建框架，刻画了攻击者的构成要素、行为规则以及行为模式，从而保证了攻击者具有合理的行为与能力，并能在攻击过程中获取新的知识，不断增强攻击能力。最后，将该工作运用到 Otway-Rees 协议的验证中，找出了该协议中所存在的漏洞，从而证明了该构建框架的有效性。
공격자건모시안전협의험증공작적일개중요부분，직접영향도험증적효솔여질량，단목전각환몰유일개가준순적형식화광가，영향료건모공작적준학성여객관성。침대저일문제，통과대재안전협의험증중구유엄범영향적 DY 모형진행형식화，건립료일개 DY 모형적구건광가，각화료공격자적구성요소、행위규칙이급행위모식，종이보증료공격자구유합리적행위여능력，병능재공격과정중획취신적지식，불단증강공격능력。최후，장해공작운용도 Otway-Rees 협의적험증중，조출료해협의중소존재적루동，종이증명료해구건광가적유효성。
The modelling of intruders is an important part of security protocol verification,which di-rectly affects the efficiency and correctness of verification.There is no available formal framework of introders modelling,which is a disadvantage for modelling work.A framework for formalizing/con-structing DY model that has extensive influence on security protocol verification was proposed.The framework can depict the components,behaviours and behaviour model of the intruders,which en-sures that the intruder has reasonable behaviours and ability and can acquire new knowledges in the attacking process to enhance contantly the attacking ability.The effectiveness of the framework was confirmed in the verification of Otway-Rees protocol in which a fault in the protocol was found.