This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the s...This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the secrecy of online purchases. A number of concepts, notations, functions, predicates, assumptions and rules are introduced. We describe the knowledge of all legal participants, and a malicious spy, to assess the security of the sub-protocol. Avoiding search in a large state space, the method converges very quickly. We implemented our method in the Isabelle/Isar automated reasoning environment, therefore the whole verification process can be executed mechanically and efficiently. Keywords Formal verification - electronic transaction protocol - knowledge-based system This work was supported by EC, EPSRC, the National Natural Science Foundation of China (No.60496320, 60496321), and Hong Kong K C Wang Education Foundation.Xiao-Qi Ma graduated from Nanjing University of Science and Technology, China, in 1997. He received his Master’s degree from the Institute of Software, Chinese Academy of Sciences in 2003. He is currently a PhD student at the University of Reading. His research interests include computer network security, knowledge-based systems, and operating systems.Xiao-Chun Cheng obtained his PhD in 1996. He has worked as a lecturer at the University of Reading since 2000. He is a guest professor at North East Normal University and Beijing Normal University. His research interests include theoretical and applied aspects in decision support systems, knowledge-based systems and intelligent systems.展开更多
A five-channel far-infrared (FIR) hydrogen cyanide (HCN) laser interferometer was developed to measure plasma electron density profile on the HT-7 superconducting tokamak. The principle and structure of the five-chann...A five-channel far-infrared (FIR) hydrogen cyanide (HCN) laser interferometer was developed to measure plasma electron density profile on the HT-7 superconducting tokamak. The principle and structure of the five-channel FIR laser interferometer is described. The laser source used in the interferometer was a continuous wave glow discharge HCN laser with a 3.4 m cavity length and a 100 mW power output at 337μm wavelength. The temporal resolution was 0.1 ms and the detection sensitivity was 1/12 fringe. Preliminary experimental results measured by the interferometer on HT-7 tokamak are reported.展开更多
The outstanding properties of CVD diamond film such as electronic, optical, thermal and mechanical and the high radiation hardness have made it an ideal candidate material for radiation detectors in severe environment...The outstanding properties of CVD diamond film such as electronic, optical, thermal and mechanical and the high radiation hardness have made it an ideal candidate material for radiation detectors in severe environments. Fabrication of ＇detector grade＇ CVD diamond films and development of CVD diamond detectors have been leading edge subjects. Micro-strip gas chamber （MSGC） fabricated on CVD diamond substrate would overcome the charge-up effect and the substrate instability, which has been a hotspot in the research of gas detectors.展开更多
The invocation of World Wide Web (www) first triggered mass adoption of the Internet for public access to digital information exchanges across the globe. To get a big market on the Web, a special security infrastructu...The invocation of World Wide Web (www) first triggered mass adoption of the Internet for public access to digital information exchanges across the globe. To get a big market on the Web, a special security infrastructure would need to be put into place transforming the wild-and-woolly Internet into a network with end-to-end protections. XML (extensible Markup Language) is widely accepted as powerful data representation standard for electronic documents, so a security mechanism for XML documents must be provided in the first place to secure electronic commerce over Internet. In this paper the authors design and implement a secure framework that provides XML signature function, XML Element-wise Encryption function, smart card based crypto API library and Public Key Infrastructure (PKI) security functions to achieve confidentiality, integrity, message authentication, and/or signer authentication services for XML documents and existing non-XML documents that are exchanged by Internet for E-commerce application.展开更多
In the relationship between electronic pricing and the market and consumers in daily life, this paper analyzes the fraud of electronic pricing, and studies the ways to deal with the fraud. We started to cooperate with...In the relationship between electronic pricing and the market and consumers in daily life, this paper analyzes the fraud of electronic pricing, and studies the ways to deal with the fraud. We started to cooperate with effective production sources to avoid the serious consequences of electronic fraud.展开更多
基金This work was supported by EC, EPSRC, the National Natural Science Foundation of China (No.60496320, 60496321)and Hong Kong K C Wang Education Foundation.
文摘This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the secrecy of online purchases. A number of concepts, notations, functions, predicates, assumptions and rules are introduced. We describe the knowledge of all legal participants, and a malicious spy, to assess the security of the sub-protocol. Avoiding search in a large state space, the method converges very quickly. We implemented our method in the Isabelle/Isar automated reasoning environment, therefore the whole verification process can be executed mechanically and efficiently. Keywords Formal verification - electronic transaction protocol - knowledge-based system This work was supported by EC, EPSRC, the National Natural Science Foundation of China (No.60496320, 60496321), and Hong Kong K C Wang Education Foundation.Xiao-Qi Ma graduated from Nanjing University of Science and Technology, China, in 1997. He received his Master’s degree from the Institute of Software, Chinese Academy of Sciences in 2003. He is currently a PhD student at the University of Reading. His research interests include computer network security, knowledge-based systems, and operating systems.Xiao-Chun Cheng obtained his PhD in 1996. He has worked as a lecturer at the University of Reading since 2000. He is a guest professor at North East Normal University and Beijing Normal University. His research interests include theoretical and applied aspects in decision support systems, knowledge-based systems and intelligent systems.
文摘A five-channel far-infrared (FIR) hydrogen cyanide (HCN) laser interferometer was developed to measure plasma electron density profile on the HT-7 superconducting tokamak. The principle and structure of the five-channel FIR laser interferometer is described. The laser source used in the interferometer was a continuous wave glow discharge HCN laser with a 3.4 m cavity length and a 100 mW power output at 337μm wavelength. The temporal resolution was 0.1 ms and the detection sensitivity was 1/12 fringe. Preliminary experimental results measured by the interferometer on HT-7 tokamak are reported.
文摘The outstanding properties of CVD diamond film such as electronic, optical, thermal and mechanical and the high radiation hardness have made it an ideal candidate material for radiation detectors in severe environments. Fabrication of ＇detector grade＇ CVD diamond films and development of CVD diamond detectors have been leading edge subjects. Micro-strip gas chamber （MSGC） fabricated on CVD diamond substrate would overcome the charge-up effect and the substrate instability, which has been a hotspot in the research of gas detectors.
文摘The invocation of World Wide Web (www) first triggered mass adoption of the Internet for public access to digital information exchanges across the globe. To get a big market on the Web, a special security infrastructure would need to be put into place transforming the wild-and-woolly Internet into a network with end-to-end protections. XML (extensible Markup Language) is widely accepted as powerful data representation standard for electronic documents, so a security mechanism for XML documents must be provided in the first place to secure electronic commerce over Internet. In this paper the authors design and implement a secure framework that provides XML signature function, XML Element-wise Encryption function, smart card based crypto API library and Public Key Infrastructure (PKI) security functions to achieve confidentiality, integrity, message authentication, and/or signer authentication services for XML documents and existing non-XML documents that are exchanged by Internet for E-commerce application.
文摘In the relationship between electronic pricing and the market and consumers in daily life, this paper analyzes the fraud of electronic pricing, and studies the ways to deal with the fraud. We started to cooperate with effective production sources to avoid the serious consequences of electronic fraud.
