The goal of the paper is to develop a software for automated analysis of PKCS#11 tokens with focus on the security of stored cryptographic keys. The paper first outlines the PKCS#11 standard and the Cryptoki API specified by the standard, including the various components of the API. Then the paper describes the mechanics of cryptographic key protection in Cryptoki. It analyses the individual functions relevant to key protection and defines the first set of tests. Then the paper performs an analysis of the previously published attacks against keys stored on the device and also outlines the second set of tests with focus on discovering attack vulnerabilities. Afterwards the paper examines various ways to improve the security of Cryptoki by altering the standard. The discussion of the proposed restrictions takes into consideration their impact on practical usability of the tokens. In order to further evaluate the security of the tokens against possible attacks, the paper also utilizes model checker software. The results of the previously defined tests are used to compose a model that is sent to a model checker for further analysis. Since the developed software is written in Java, the paper also examines the Java PKCS#11 wrapper and discusses the advantages and disadvantages against using C for implementation. The most obvious advantage is that the software can be easily deployed on other operating systems, which is particularly useful for testing tokens that only work on Windows. The disadvantage is that the used wrapper does not implement all the Cryptoki functions, but the paper shows that all these limitations either do not matter or they can be worked around. The paper also presents the developed tool called Caetus. The tool first connects into the token, discovers the basic capabilities of the device and based on these capabilities it performs in-depth testing of Cryptoki functions. First part of the tests focuses on adherence to the PKCS#11 standard, which means the discovered issues do not necessarily mean security risks. The other set of tests attempts to discover vulnerability of the token to the previously published attacks and other trivial attacks. Finally the tool can use the discovered capabilities in order to compose a model specification which is then sent to the model checker. The tool is currently optimized for analysis of software tokens. The last part of the paper consists of tables with results of token testing and discussion of the results.