计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2010年
8期
113-116
,共4页
安全电子交易%符号模型验证器%符号模型%模型检测
安全電子交易%符號模型驗證器%符號模型%模型檢測
안전전자교역%부호모형험증기%부호모형%모형검측
Secure Electronic Transaction(SET)%Symbolic Model Verifier(SMV)%symbolic model%model checking
在以Lu&Smolka对SET协议支付过程的简化模型为研究对象的情况下,进行形式化建模和有限状态机模型.同时应用CTL时相应的安全性质进行形式描述,并在网络环境被入侵者控制的假设下,利用SMV分析了协议的认证性、保密性和完整性,发现攻击并对该攻击所产生的影响进行了讨论.最后修改其协议模型对改进后的协议进行分析和检验,说明了SET协议独具特色的双重签名在整个协议运行中至关重要.
在以Lu&Smolka對SET協議支付過程的簡化模型為研究對象的情況下,進行形式化建模和有限狀態機模型.同時應用CTL時相應的安全性質進行形式描述,併在網絡環境被入侵者控製的假設下,利用SMV分析瞭協議的認證性、保密性和完整性,髮現攻擊併對該攻擊所產生的影響進行瞭討論.最後脩改其協議模型對改進後的協議進行分析和檢驗,說明瞭SET協議獨具特色的雙重籤名在整箇協議運行中至關重要.
재이Lu&Smolka대SET협의지부과정적간화모형위연구대상적정황하,진행형식화건모화유한상태궤모형.동시응용CTL시상응적안전성질진행형식묘술,병재망락배경피입침자공제적가설하,이용SMV분석료협의적인증성、보밀성화완정성,발현공격병대해공격소산생적영향진행료토론.최후수개기협의모형대개진후적협의진행분석화검험,설명료SET협의독구특색적쌍중첨명재정개협의운행중지관중요.
The simplified model of payment process of the SET protocol is used to build up its formal model and finite state machine model,as well as CTL formulations of the security properties are presented.Under the assumption of the network environment being controlled by intruder,the symbolic model checking ware(SMV)is appLed for analyzing the authentication,confidentiality and integrity,attacks are found.Then,the influence of attacks is discussed.Finally,the protocol model is optimized.The result of analysis and checking indicates the importance of dual signature on SET protocol.
