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/

[1] NSA Cross-Organizational CAPI Team, Security Service API: Cryptographic API Recommendation, Second Edition. Government Information Technology Issues, 1996

[2] RFC 2246, The TLS Protocol Version 1.0, January 1999

[3] Canetti R., “Universally Composable Security: A New paradigm for Cryptographic Protocols”, 42nd IEEE Symposium on Foundations of Computer Science (Las Vegas, NV, 2001), IEEE Computer Soc., Los Alamitos, CA, 2001, 136–145 | MR

[4] Lincoln P., Mitchell J., Mitchell M., Scedrov A., Probabilistic Polynomial-Time Equivalence and Security Analysis, , 1999 http://citeseer.ist.psu.edu

[5] Mateus P., Mitchell J., Scedrov A., Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus, , 2002 http://citeseer.ist.psu.edu | MR

[6] Canetti R., Universally Composable Signature, Certification, and Authentication, , 2004 http://citeseer.ist.psu.edu

[7] Canetti R., Krawczyk H., Universally Composable Notions of Key Exchange and Secure Channels, , 2002 http://citeseer.ist.psu.edu

[8] Canetti R., Rabin T., Universal Composition with Join State, , 2002 http://eprint.iacr.org | MR

[9] Backes M., Pfitzmann B., Waidner M., A Universally Composable Cryptographic Library, , 2003 http://citeseer.ist.psu.edu

[10] Pfitzmann B., Schunter M., Waidner M., Secure Reactive Systems, IBM Research Report RZ 3206(93252), IBM Research Division, Zurich, Feb., 2000

[11] Backes M., Jacobi C., “Cryptographically Sound and Machine-Assisted Verification of Security Protocols”, Proc. 20th Annual STACS, Lecture Notes in Computer Science, 2607, Springer, 2003, 675–686 | MR | Zbl

[12] Prototype Verification System (PVS), http://pvs.csl.sri.com

[13] Cimatti A., Clarke E., Giunchiglia F., Roveri M., NuSMV: a new symbolic model checker, Software Tools for Technology Transfer, 1998

[14] Cheetancheri S., Our experiments with NuSMV, , 2004 http://shasta.cs.ucdavis.edu/eas

[15] Prokopev S. E., “Adaptatsiya modeli bezopasnosti Kanetti dlya ispolzovaniya v kachestve arkhitektury podsistemy kriptograficheskikh servisov”, Problemy informatsionnoi bezopasnosti. Kompyuternye sistemy, 2005, no. 5