Modelling of the PKI protocols in the universally composable framework using model checkers

We analyze the PKI protocols in the universally composable security framework with following purposes: 1) decomposition of the code of the cryptographic service “Digital Signature with PKI” to the high- and low-danger parts, 2) obtaining a deterministic and cryptographically sound abstraction of this service. We experimented with NuSMV model checker to automate partially our analysis.