计算机仿真
計算機倣真
계산궤방진
COMPUTER SIMULATION
2007年
2期
99-102
,共4页
进程演算%安全协议%形式化方法
進程縯算%安全協議%形式化方法
진정연산%안전협의%형식화방법
进程演算通常用来研究交互式反应系统,其中的互模拟方法是用来形式化验证系统属性的重要途径.首先扩展了进程演算中的Spi演算,并将其应用于形式化描述网络安全协议--Kerberos协议的安全属性.为了验证该协议所声称的安全属性,引入了Spi演算中环境敏感互模拟的方法,即两个系统与环境发生交互过程中是否互模拟.通过采用该互模拟关系对Kerberos协议两个安全属性--可认证性和保密性--的证明,发现其可认证性是可靠的,而保密性存在一个可能的漏洞.最后,指出了基于互模拟的安全协议形式化验证方法今后值得进一步研究的方向.
進程縯算通常用來研究交互式反應繫統,其中的互模擬方法是用來形式化驗證繫統屬性的重要途徑.首先擴展瞭進程縯算中的Spi縯算,併將其應用于形式化描述網絡安全協議--Kerberos協議的安全屬性.為瞭驗證該協議所聲稱的安全屬性,引入瞭Spi縯算中環境敏感互模擬的方法,即兩箇繫統與環境髮生交互過程中是否互模擬.通過採用該互模擬關繫對Kerberos協議兩箇安全屬性--可認證性和保密性--的證明,髮現其可認證性是可靠的,而保密性存在一箇可能的漏洞.最後,指齣瞭基于互模擬的安全協議形式化驗證方法今後值得進一步研究的方嚮.
진정연산통상용래연구교호식반응계통,기중적호모의방법시용래형식화험증계통속성적중요도경.수선확전료진정연산중적Spi연산,병장기응용우형식화묘술망락안전협의--Kerberos협의적안전속성.위료험증해협의소성칭적안전속성,인입료Spi연산중배경민감호모의적방법,즉량개계통여배경발생교호과정중시부호모의.통과채용해호모의관계대Kerberos협의량개안전속성--가인증성화보밀성--적증명,발현기가인증성시가고적,이보밀성존재일개가능적루동.최후,지출료기우호모의적안전협의형식화험증방법금후치득진일보연구적방향.
