Weanalyze 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.
Download file
Counter downloads: 80
- Title Modelling of the PKI protocols in the universally composableframework using model checkers
- Headline Modelling of the PKI protocols in the universally composableframework using model checkers
- Publesher
Tomsk State University - Issue Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics 1(3)
- Date:
- DOI
Keywords
PKI , цифровая подпись , NuSMV , верификаторы моделей , UC-модели Authors
References
Lincoln P., Mitchell J., Mitchell M., Scedrov A. Probabilistic Polynomial-Time Equivalence and Security Analysis. <http://citeseer.ist.psu.edu>. 1999.
Canetti R. Universally Composable Security: A New paradigm for Cryptographic Protocols // 42nd FOCS, 2001.
NSA Cross-Organizational CAPI Team. Security Service API: Cryptographic API Recommendation. Second Edition. // Government Information Technology Issues, 1996. RFC 2246. The TLS Protocol Version 1.0. January 1999.
Mateus P., Mitchell J., Scedrov A. Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus. <http://citeseer.ist.psu.edu>. 2002.
Canetti R. Universally Composable Signature, Certification, and Authentication. <http://><citeseer.ist.psu.edu>. 2004.
Canetti R., Krawczyk H. Universally Composable Notions of Key Exchange and Secure Channels. <http://citeseer.ist.psu.edu>. 2002.
Canetti R., Rabin T. Universal Composition with Join State. <http://eprint.iacr.org>.2002.
Backes M., Pfitzmann В., Waidner M. A Universally Composable Cryptographic Library. <http://citeseer.ist.psu.edu>. 2003.
Pfitzmann В., Schunter M., Waidner M. Secure Reactive Systems. // IBM Research Report RZ 3206(93252), IBM Research Division, Zurich, Feb. 2000.
Baches M., Jacobi С. Cryptographically Sound and Machine-Assisted Verification of Security Protocols // In Proc. 20th Annual STACS, volume 2607 of Lecture Notes in Computer Science, pages 675-686. Springer, 2003.
<http://pvs.csl.sri.com>-Prototype Verification System (PVS).
Cimatti A., Clarke E., Giunchiglia F., Roveri M. NuSMV: a new symbolic model checker. // Software Tools for Technology Transfer, 1998.
Cheetancheri S. Our experiments with NuSMV. http: //shasta. cs .ucdavis .edu/eas. 2004.
Прокопьев С. Е. Адаптация модели безопасности Канетти для использования в качестве архитектуры подсистемы криптографических сервисов // Проблемы информационной безопасности. Компьютерные системы. 2005. №5.
Modelling of the PKI protocols in the universally composableframework using model checkers | Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics. 2009. № 1(3).
Download full-text version
Download fileCounter downloads: 275