小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
3期
492-497
,共6页
刘文远%马生%司亚利%侯贵宾
劉文遠%馬生%司亞利%侯貴賓
류문원%마생%사아리%후귀빈
电子商务协议%形式化分析%有穷自动机%逻辑分析
電子商務協議%形式化分析%有窮自動機%邏輯分析
전자상무협의%형식화분석%유궁자동궤%라집분석
提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.
提齣一種擴展的有窮自動機模型,併結閤卿-週邏輯給齣一種新的電子商務協議形式化分析方法,用于分析電子商務協議的可追究性、公平性和時限性.該方法結閤瞭模型檢測和邏輯分析兩種形式化分析方法的優點,可以準確形象地描述協議的具體運行過程,併且在髮生重放攻擊時能夠正確分析各方的責任.利用該方法對Kim等人提齣的改進版ZG協議進行瞭實例分析,給齣瞭描述該協議運行過程的狀態轉換圖,結閤狀態轉換圖對該協議分析得齣其滿足可追究性、公平性、時限性,併且不存在被重放攻擊的可能.最後用時間自動機UPPAAL驗證瞭新方法中有窮自動機模型的準確性和時限性分析的有效性.
제출일충확전적유궁자동궤모형,병결합경-주라집급출일충신적전자상무협의형식화분석방법,용우분석전자상무협의적가추구성、공평성화시한성.해방법결합료모형검측화라집분석량충형식화분석방법적우점,가이준학형상지묘술협의적구체운행과정,병차재발생중방공격시능구정학분석각방적책임.이용해방법대Kim등인제출적개진판ZG협의진행료실례분석,급출료묘술해협의운행과정적상태전환도,결합상태전환도대해협의분석득출기만족가추구성、공평성、시한성,병차불존재피중방공격적가능.최후용시간자동궤UPPAAL험증료신방법중유궁자동궤모형적준학성화시한성분석적유효성.
