Simple Public Key Infrastructure Protocol Analysis and Design

Secure electronic communication is based on secrecy, authentication and authorization. One means of assuring a communication has these properties is to use Public Key Cryptography (PKC). The framework consisting of standards, protocols and instructions that make PKC usable in communication applications is called a Public Key Infrastructure (PKI). This thesis aims at proving the applicability of the Simple Public Key Infrastructure (SPKI) as a means of PKC. The strand space approach of Guttman and Thayer is used to provide an appropriate model for analysis. A Diffie-Hellman strand space model is combined with mixed strand space proof methods for proving the correctness of multiple protocols operating in the same context. The result is the public key mixed strand space model. This model is ideal for the analysis of SPKI applications operating as sub-protocols of an implementing application. This thesis then models the popular Internet Transport Layer Security (TLS) protocol as a public key mixed strand space model. The model includes the integration of SPKI certificates. To accommodate the functionality of SPKI, a new protocol is designed for certificate validation, the Certificate Chain Validation Protocol (CCV). The CCV protocol operates as a sub-protocol to TLS and provides online certificate validation. The security of the TLS protocol integrated with SPKI certificates and subprotocols is then analyzed to prove its security properties.