We propose in this paper a logic-based approach for reasoning about PKI trust models. Our formalism uses the predicate calculus language to describe a PKI trust model with greater precision than the widely used graph. Indeed, it allows us to formalize the certificates of the model and the statements about entities beliefs with regard to public key authenticity and CAs trustworthiness. In this formalism, we take into account the number of CAs that have participated in an entity belief, the trust level in a statement and the certificate policies constraints. By using this approach, we can verify the suitability of a model to applications with particular requirements.