Studies the structure of wireless PKI, and designs the system of certificate, wtls protocol, wap secure gateway and the interface of wim.

This paper analyzes the security of Tan's scheme for remote password authentication based on cross-product. We point out that to impersonate one user's log-in reguest, the intruders need only to know the user's two log-in requests, or need only to know one log-in request after booking a smart card and getting some useful information from it, so the scheme is not secure. Some modifications to Tan's scheme for avoiding the above two kinds of possible attacks are given.

A specification method using PVS is presented. Higher order logic is chosen as the specification language. Strong spy and ideal encryption are assumed, and trace model is used to define protocols' behaviors. Moreover, useful structures such as message, event, protocol rule, etc. are semantically encoded.

The advantages and disadvantages of model checking technology and logic reasoning technology is analyzed, Based on it, the author gives a specification of the new mixed technology of the two technologies which can provide a more complete formal analysis of security protocols.

Security requirements for a challenge-response mutual authentication protocol are formulted as seven simple necessary conditions. Each of these conditions is related to an attack so that a protocol not fulfilling all the conditions will be vulnerable to one of the attacks. Two protocols are idetified such that they contain minimal number of necessary security parmeters.

In this paper, we have presented a general method to improve the security of TMN Protocol based on trap-door one-way functions. We also proved its security by using strand space theory and gave some examples of our improvement.

The primary elements of Gurevich's Abstract State Machines(ASM)are introduced. A verification enviroment is proposed for analying of security protocols in ASM,and a general penetrator model is presented so that much of security properties could be dealed with. As a case, Helsinki protocol are specified in the model,a direct mathematical proof of its weakness is given.

The Internet Accessible Mathematical Computation (IAMC) framework makes supplying/accessing mathematical computation easy on the Internet/Web. In this paper, the vulnerabilities of the current IAMC framework is discussed. A scheme for incorporating SSL/TLS protocol into the current Mathematical Computation Protocol is presented. The resulting secure Mathematical Computation Protocol can then provide crypto-graphic authentications, data privacy and integrity.

A simple type system with security levels in π-calculus is proposed, and its type soundness is proved. This simple type. π-calculus with this type system can be used as a general formalism for secure systems or secure protocols analysis and specification.

Plücker coordinates are important in pure mathematics. In this paper, we propose a new method for constructing secret share schemes based on plücker coordinates. We show that several usual linear secret sharing schemes are our scheme's particular examples.

Strand Spaces serve as a model of security protocol analysis. In this paper, the main characteristics of Strand Spaces are briefly introduced, and its advantages and disadvantages are presented. An algorithm of building an ideal model of a protocol is proposed, which is used to bound both the abilities of the penetrator and the number of concurrent protocol runs. Combining Model Checking and Strand Spaces, a method is proposed to use both the automatic reasoning mechanism of the Model Checking and the bounds on security protocol analysis to achieve effective analysis of security protocols, avoiding state explosion problems.

To solve the problems that BAN logic analysis tends to neglect the potential defect of "send again attack" for cryptographic protocols,is made some improvement to the new message judgement of logic postulate of BAN logic analysis, aiming at reducing the misleading probability of BAN logic

Due to the rapid growth of the Internet applications, varied cryptographic protocols, including thses complex protocols with many roles and many cryptographic primitives, have been widely used to achieved various secure requirements in the distributed system. In the large distributed network environment, due to the maximum number of participants involved and the complexcity of run conditions of the protocol, the security characterzation and analysis for protocols is very difficult and complicated. In this paper, we introduce a new algebra system called Cryptographic Protocol Algebra(CPA) that characterizes the algebraic properties of messages involved in the protocol with multiple cryptographic operations. Based on CPA, we propose a new formal model for general cryptographic protocols. And we specify run conditions and security properties of cryptographic protocols in the unbounded network environment by building a formal language. Based on our model, we characterize a coordinated attack mode to protocols, and discuss reduction techniques for the protocol security analysis. Finally we briefly describe a new automatic analysis process for cryptographic protocols.

A mode of operation is an algorithm that features the use of a block cipher to provide an information security service. In the process of calling modes for AES, NIST received 15 candidates. Author introduces the 15 Modes of Operation for AES and their design ideas and characteristics.

This paper firstly presents a briefly survey on the security technologies in wireless communications. Then we focus on some important protocols which will be used in WPKI, especially the WEP algorithm in IEEE 802.11 and the Wireless Transport Layer Security (WTLS) in Wireless Application Protocol (WAP). We study realizations of these two protocols, compare their security features, and discuss their potential advances in applications.

This paper firstly presents a briefly survey on the security technologies in wireless communications Then we focus on some important protocols which will be used in WPKI algorithm in IEEE 802 Protocol(WAP).We.11 and the Wireless Transport Layer Security ( W'I'LS) inespecially the WEP Wireless Application study realizations of these two protocols, compare their security features, and discuss their potential advances in applications.