计算机科学
計算機科學
계산궤과학
Computer Science
2015年
9期
118-126,143
,共10页
刘海%彭长根%张弘%任祉静
劉海%彭長根%張弘%任祉靜
류해%팽장근%장홍%임지정
ATEL%博弈论%理性安全协议%形式化分析%理性安全性%理性公平性
ATEL%博弈論%理性安全協議%形式化分析%理性安全性%理性公平性
ATEL%박혁론%이성안전협의%형식화분석%이성안전성%이성공평성
Alternating-time temporal epistemic logic(ATEL)%Game theory%Rational secure protocol%Formal analysis%Rational security%Rational fairness
博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证.但在理性环境中,由于参与者对知识的自利性,ATL和ATEL都不能形式化分析与验证理性安全协议.因此在CEGS中引入效用函数和偏好关系知识,得到新的rCEGS,并在合作模态算子《Γ》中加入行为ACT参数,提出新的可形式化分析理性安全协议的交替时序认知逻辑rATEL-A.然后运用rATEL-A构建两方理性安全协议的形式化模型,并基于rCEGS的等价扩展式博弈,对具体的两方理性交换协议进行形式化分析,结果表明构建的形式化模型可以有效地形式化分析理性安全协议的正确性、理性安全性和理性公平性.
博弈邏輯ATL和ATEL可以對傳統安全協議的公平性、安全性等性質進行分析與驗證.但在理性環境中,由于參與者對知識的自利性,ATL和ATEL都不能形式化分析與驗證理性安全協議.因此在CEGS中引入效用函數和偏好關繫知識,得到新的rCEGS,併在閤作模態算子《Γ》中加入行為ACT參數,提齣新的可形式化分析理性安全協議的交替時序認知邏輯rATEL-A.然後運用rATEL-A構建兩方理性安全協議的形式化模型,併基于rCEGS的等價擴展式博弈,對具體的兩方理性交換協議進行形式化分析,結果錶明構建的形式化模型可以有效地形式化分析理性安全協議的正確性、理性安全性和理性公平性.
박혁라집ATL화ATEL가이대전통안전협의적공평성、안전성등성질진행분석여험증.단재이성배경중,유우삼여자대지식적자리성,ATL화ATEL도불능형식화분석여험증이성안전협의.인차재CEGS중인입효용함수화편호관계지식,득도신적rCEGS,병재합작모태산자《Γ》중가입행위ACT삼수,제출신적가형식화분석이성안전협의적교체시서인지라집rATEL-A.연후운용rATEL-A구건량방이성안전협의적형식화모형,병기우rCEGS적등개확전식박혁,대구체적량방이성교환협의진행형식화분석,결과표명구건적형식화모형가이유효지형식화분석이성안전협의적정학성、이성안전성화이성공평성.
