华南理工大学学报（自然科学版）
華南理工大學學報（自然科學版）
화남리공대학학보（자연과학판）
JOURNAL OF SOUTH CHINA UNIVERSITY OF TECHNOLOGY(NATURAL SCIENCE EDITION)
2013年
1期
77-82,94
,共7页
自动信任协商%安全性%形式化分析%Applied π演算%观察等价%ProVerif
自動信任協商%安全性%形式化分析%Applied π縯算%觀察等價%ProVerif
자동신임협상%안전성%형식화분석%Applied π연산%관찰등개%ProVerif
为了对自动信任协商(ATN)的安全性进行形式化分析与验证,文中借鉴安全协议的形式化分析方法,提出一种用进程代数Appliedπ演算对ATN建模并验证其安全性的方法.该方法将ATN形式化为两个协商者进程的并发执行,其中一个协商者的进程就是对其拥有的证书及授权策略的静态建模；ATN的安全性被定义为Appliedπ演算的观察等价性,从而使该方法不仅能检查授权策略执行的安全性,而且能对协商者的隐私安全进行验证.借助安全协议的自动分析工具ProVefif,文中实现了对ATN安全性的自动分析.实验结果表明,用Applied π演算形式化及验证ATN的安全性是可行的,安全性验证可自动完成,并且效率较高.
為瞭對自動信任協商(ATN)的安全性進行形式化分析與驗證,文中藉鑒安全協議的形式化分析方法,提齣一種用進程代數Appliedπ縯算對ATN建模併驗證其安全性的方法.該方法將ATN形式化為兩箇協商者進程的併髮執行,其中一箇協商者的進程就是對其擁有的證書及授權策略的靜態建模；ATN的安全性被定義為Appliedπ縯算的觀察等價性,從而使該方法不僅能檢查授權策略執行的安全性,而且能對協商者的隱私安全進行驗證.藉助安全協議的自動分析工具ProVefif,文中實現瞭對ATN安全性的自動分析.實驗結果錶明,用Applied π縯算形式化及驗證ATN的安全性是可行的,安全性驗證可自動完成,併且效率較高.
위료대자동신임협상(ATN)적안전성진행형식화분석여험증,문중차감안전협의적형식화분석방법,제출일충용진정대수Appliedπ연산대ATN건모병험증기안전성적방법.해방법장ATN형식화위량개협상자진정적병발집행,기중일개협상자적진정취시대기옹유적증서급수권책략적정태건모；ATN적안전성피정의위Appliedπ연산적관찰등개성,종이사해방법불부능검사수권책략집행적안전성,이차능대협상자적은사안전진행험증.차조안전협의적자동분석공구ProVefif,문중실현료대ATN안전성적자동분석.실험결과표명,용Applied π연산형식화급험증ATN적안전성시가행적,안전성험증가자동완성,병차효솔교고.
