Geodesic
Modelling of the PKI protocols in the universally composable framework using model checkers
Prikladnaâ diskretnaâ matematika, no. 1 (2009), pp. 79-92

Voir la notice de l'article provenant de la source Math-Net.Ru

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. 
@article{PDM_2009_1_a4,
     author = {S. E. Prokopyev},
     title = {Modelling of the {PKI} protocols in the universally composable framework using model checkers},
     journal = {Prikladna\^a diskretna\^a matematika},
     pages = {79--92},
     publisher = {mathdoc},
     number = {1},
     year = {2009},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDM_2009_1_a4/}
}
TY  - JOUR
AU  - S. E. Prokopyev
TI  - Modelling of the PKI protocols in the universally composable framework using model checkers
JO  - Prikladnaâ diskretnaâ matematika
PY  - 2009
SP  - 79
EP  - 92
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDM_2009_1_a4/
LA  - ru
ID  - PDM_2009_1_a4
ER  - 
%0 Journal Article
%A S. E. Prokopyev
%T Modelling of the PKI protocols in the universally composable framework using model checkers
%J Prikladnaâ diskretnaâ matematika
%D 2009
%P 79-92
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDM_2009_1_a4/
%G ru
%F PDM_2009_1_a4
S. E. Prokopyev. Modelling of the PKI protocols in the universally composable framework using model checkers. Prikladnaâ diskretnaâ matematika, no. 1 (2009), pp. 79-92. http://geodesic.mathdoc.fr/item/PDM_2009_1_a4/