CAJ | 학술논문

安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.
안전협의모형시안전협의분석여험증적기출,현유적건모방법중존재착일사결점,여:건모복잡、중용성차등.위차제출료일충류형화적π연산:πt연산,병급출료상응류형추리규칙화구치규칙,πt연산적안전성야득도료증명.πt연산가이대안전협의、협의공격자진행형식화건모.기우πt연산적안전협의모형급기건모과정사용NRL협의위례주출료설명.동시급출료공격자모형,병증명료기우πt연산적안전협의공격자모형여D-Y공격자모형재행동능력상시일치적.저보증료기우πt연산적안전협의모형적험증결과적정학성.기우πt연산적건모방법능재협의수거어의、협의삼여자지식방면실현세치적묘술.여동류방법상비,해방법가제공다충분석지지,구유경호적역용성、중용성.분석표명,해방법가이재건모중발현일정적안전협의루동.