Many Petri nets-based methods have been developed and applied to analyze cryptographic protocols. Most of them offer the analysis of one attack trace only. Only a few of them provide the analysis of multiple attack traces, but they are rather inefficient. Similarly, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. Recently, we proposed a simple but practical Petri nets-based model checking methodology for the analysis of cryptographic protocols, which offers an efficient analysis of all attack traces. In our previous analysis, we assume that the underlying cryptographic algorithms are black boxes, and attackers cannot learn anything from cipher text if they do not have a correct key. In this paper, we relax this assumption by considering some algebraic properties of the underlying encryption algorithm. Then, we apply our new method to TMN authenticated key exchange protocol as a case study. Surprisingly, we obtain a very efficient analysis when the numbers of attack traces and states are large, and we discover two new attacks which exploit the algebraic properties of the encryption.

A multi-application smart card system consists of an issuer, service vendors and cardholders, where cardholders are recipients of smart cards (from the issuer) to be used in connection with applications offered by service vendors. Authentic post-issuance program modification is necessary for a multi-application smart card system because applications in the system are realized after the issuance of a smart card. In this paper, we propose a system where only authentic modification is possible. In the proposed system, the smart card issuer stores a unique long bitstring called PID in a smart card. The smart card is then given to the cardholder. A unique substring of the PID (subPID) is shared between the cardholder and a corresponding service vendor. Another subPID is shared between the issuer and the cardholder. During program modification, a protocol using the subPIDs, a one-way hash function and a pseudorandom number generator function verifies the identity of the parties and the authenticity of the program.

A computational model for security verification of cryptographic protocols is proposed. Until most recently, security verification of cryptographic protocols was left to the protocol designers' experience and heuristics. Though some formal verification methods have been proposed for this purpose, they are still insufficient for the verification of practical real-time cryptographic protocols. In this paper we propose a new formalism based on a term rewriting system approach that we have developed. In this model, what and when the saboteur can obtain is expressed by a first-order term of a special form, and time-related concepts such as the passage of time and the causality relation are specified by conditional term rewriting systems. By using our model, a cryptographic protocol which was shown to be secure by the BAN-logic is shown to be insecure.

We have devised a polynomial time algorithm to decide the security of cryptographic protocols formally under certain conditions, and implemented the algorithm on a computer as a supporting system for deciding the security. In this paper, a useful approach is presented to decide security problems which do not satisfy some of the above-mentioned conditions by using the system. For its application, we consider a basic security problem of Kerberos protocol, whether or not an enemy can obtain the session key between a client and a server by using any information not protected in communication channels and using any operation not prohibited in the system. It is shown that Kerberos is secure for this problem.

In this paper, we present an electronic voting scheme with a single voting center using an anonymous channel. The proposed scheme is a 3-move protocol between each voter and the center, with one extra move if one wants to make objection to the tally. This objection can be broadcasted widely since it will not disclose the vote itself to the other parties besides the center. The main idea in the proposal is that each voter sends anonymously a public key signed by the center and an encrypted vote decryptable using this key. Since even the center cannot modify a received ballot to a different vote using the same public key, the key can be used as an evidence in making open objection to the tally.

It is difficult to decide whether or not a given cryptographic protocol is secure even though the cryptographic algorithm used for the protocol is assumed to be secure. We have proposed an algorithm to decide the security of cryptographic protocols under several conditions. In this paper, we review our algorithm and report a system to verify the security. The system has be implemented on a computer. By using this system, we have verified the security of several protocols efficiently.