小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
11期
2594-2598
,共5页
王宝文%卢贝%司亚利%刘文远
王寶文%盧貝%司亞利%劉文遠
왕보문%로패%사아리%류문원
形式化分析方法%电子商务协议%颜色Petri网%CPN Tools%KZG协议
形式化分析方法%電子商務協議%顏色Petri網%CPN Tools%KZG協議
형식화분석방법%전자상무협의%안색Petri망%CPN Tools%KZG협의
formal analysis%E-commerce protocols%colored Petri nets%CPN tools%KZG protocol
针对现有颜色Petri网方法未能分析时限性的缺点,提出一种基于颜色Petri网的电子商务协议分析方法,用于分析可追究性、公平性和时限性三个重要安全属性.针对时限性建立了表示主体是否成功接收消息的状态颜色集和主体自定义的时间颜色集,并充分考虑时限性对公平性的影响,更加有效地分析公平性.文中以KZG协议为例,建立了KZG的分层颜色Petri网模型,利用CPN Tools工具对该模型仿真运行,并通过状态空间和查询函数分析了协议的性质,证明了本方法的有效性.
針對現有顏色Petri網方法未能分析時限性的缺點,提齣一種基于顏色Petri網的電子商務協議分析方法,用于分析可追究性、公平性和時限性三箇重要安全屬性.針對時限性建立瞭錶示主體是否成功接收消息的狀態顏色集和主體自定義的時間顏色集,併充分攷慮時限性對公平性的影響,更加有效地分析公平性.文中以KZG協議為例,建立瞭KZG的分層顏色Petri網模型,利用CPN Tools工具對該模型倣真運行,併通過狀態空間和查詢函數分析瞭協議的性質,證明瞭本方法的有效性.
침대현유안색Petri망방법미능분석시한성적결점,제출일충기우안색Petri망적전자상무협의분석방법,용우분석가추구성、공평성화시한성삼개중요안전속성.침대시한성건립료표시주체시부성공접수소식적상태안색집화주체자정의적시간안색집,병충분고필시한성대공평성적영향,경가유효지분석공평성.문중이KZG협의위례,건립료KZG적분층안색Petri망모형,이용CPN Tools공구대해모형방진운행,병통과상태공간화사순함수분석료협의적성질,증명료본방법적유효성.
