This paper initiates a study of accountable certificate management methods, necessary to support long-term authenticity of digital doc- uments. Our main contribution is a model for accountable certifi- cate management, where clients receive attestations confi rming in- clusion/removal of their certificates from the database of valid cer- tifi cates. We explain why accountability depends on the inability of the third parties to create contradictory attestations. After that we define an undeniable attester as a primitive that provides effi- cient attestation creation, publishing and verifi cation, so that it is intractable to create contradictory attestations. We introduce au- thenticated search trees and build an effi cient undeniable attester upon them. The proposed system is the fi rst accountable long-term certificate management system. Moreover, authenticated search trees can be used in many security-critical applications instead of the (sorted) hash trees to reduce trust in the authorities, without decrease in efficienc y. Therefore, the undeniable attester promises looks like a very useful cryptographic primitive with a wide range of applications.

In this article we present a technique for static analysis, correct with respect to complexity-theoretic definitions of security, of cryptographic protocols for checking whether these protocols satisfy confidentiality properties. The ap proach is similar to Abadi and Rogaway — we define patterns for cryptographic protocols (they did it for formal expressions), such that the protocol is secure iff the patterns are. We then statically analyse the patterns, they should be easier to analyse than the protocols themselves. We consider symmetric encryption as the cryptographic primitive in protocols. Handling this primitive has so far received comparatively less attention in approaches striving to unite the formal and computational models of cryptography. I. INTRODUCTION A cryptographic protocol is expected to satisfy certain security properties. In this paper we are interested in confi - dentiality properties which state that all protocol runs mu st look somehow similar — the view of the adversary may not depend on the secret information that one legitimate protoc ol party wishes to transmit to some other one. Protocols have to be verified about satisfying the required security properties. The verification procedure should pro duce some kind of proof that the property is satisfied. It is possib le to craft these proofs by hand. However, there exist a lot of pr o- tocols, so automatic verification methods are necessary. Su ch methods do indeed exist; there are tools which take protocol descriptions as inputs and return whether these protocols a re secure or not (and in the case of insecurity, may even show an attack). The methods do not necessarily always give a definit e answer (the problem of deciding whether the protocol is secure may be very hard, depending on the definition of security), they may also have an option to answer "don't know". Even methods that sometimes answer "don't know" are useful if they can be expected to give definite answers for reasonable protocols reasonably often. Quite often the methods have only two possible answers — "secure" and "don't know". This is called "erring on the safe side" — labeling an insecure protocol secure may have much more serious consequences than labeling a secure protocol potentially insecure. Almost all the existing tools and methods for automatic checking of security properties have one common shortcoming — they are based on the Dolev-Yao model, i.e. they assume "perfect" cryptography. In this model, the exchanged messages are modeled as elements of a certain term algebra; the capa- bilities of the adversary and the security definitions are al so given in terms of that algebra.