形式化验证可信第三方角色的性质

Verifcation of electronic business system' security with TTP using formal method

随着电子商务的发展,电子商务协议中受信任的第三方担负着越来越重要的角色。针对电子协议的安全性,用形式化的方法(如CCS)对几种带有可信任第三方平台的电子商务协议进行描述,并用模型检测的方法对安全协议的几种性质进行了阐述和验证。

With the development of Internet technology and the extension of its application areas,electronic commerce is becoming flourishing.In electronic commerce protocol,the Trusted Third Party（TTP） takes on a very important role.This paper used Calculus of Communication System（CCS） to give the formal specification of the electronic business system with TTP.And the system＇ security was verified and analyzed using model checking.