Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
In this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be argued to be a very limited model, it should be s...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2013-01-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/3720 |
| _version_ | 1818422467465576448 |
|---|---|
| author | Mauricio Ayala-Rincón Yuri Santos Rego |
| author_facet | Mauricio Ayala-Rincón Yuri Santos Rego |
| author_sort | Mauricio Ayala-Rincón |
| collection | DOAJ |
| description | In this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be argued to be a very limited model, it should be stressed here that they are the basis of more sophisticated protocols of great applicability, such as those which allow treatment of multiparty, tuples, nonces, name-stamps, signatures, etc. In the current algebraic approach, steps of the protocol are modeled in a monoid freely generated by the cryptographic operators. Words in this monoid are specified as finite sequences and the whole protocol as a finite sequence of protocol steps, that are functions from pairs of users to sequences of cryptographic operators. In a previous work, assuming that for balanced protocols admissible words produced by a potential intruder should be balanced, a formalization of the characterization of security of this kind of protocols was given in PVS. In this work, the previously assumed property is also formalized, obtaining in this way a complete formalization which mathematically guarantees the security of these protocols. Despite such property being relatively easy to specify, obtaining a complete formalization requires a great amount of effort, because several algebraic properties, that are related to the preservation of the balancing property of the admissible language of the intruder, should be formalized in the granularity of the underlying data structure (of finite sequences used in the specification). Among these properties, the most complex are related to the notion of linkage property, which allows for a systematic analysis of words of the admissible language of a potential saboteur, showing how he/she is unable to isolate private keys of other users under the assumption of balanced protocols. The difficulties that arose in conducting this formalization are also presented in this work. |
| first_indexed | 2024-12-14T13:26:43Z |
| format | Article |
| id | doaj.art-767e571c84044efa805d9f4f91c1d389 |
| institution | Directory Open Access Journal |
| issn | 1972-5787 |
| language | English |
| last_indexed | 2024-12-14T13:26:43Z |
| publishDate | 2013-01-01 |
| publisher | University of Bologna |
| record_format | Article |
| series | Journal of Formalized Reasoning |
| spelling | doaj.art-767e571c84044efa805d9f4f91c1d3892022-12-21T22:59:49ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872013-01-0161316110.6092/issn.1972-5787/3720Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol ModelMauricio Ayala-RincónYuri Santos RegoIn this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be argued to be a very limited model, it should be stressed here that they are the basis of more sophisticated protocols of great applicability, such as those which allow treatment of multiparty, tuples, nonces, name-stamps, signatures, etc. In the current algebraic approach, steps of the protocol are modeled in a monoid freely generated by the cryptographic operators. Words in this monoid are specified as finite sequences and the whole protocol as a finite sequence of protocol steps, that are functions from pairs of users to sequences of cryptographic operators. In a previous work, assuming that for balanced protocols admissible words produced by a potential intruder should be balanced, a formalization of the characterization of security of this kind of protocols was given in PVS. In this work, the previously assumed property is also formalized, obtaining in this way a complete formalization which mathematically guarantees the security of these protocols. Despite such property being relatively easy to specify, obtaining a complete formalization requires a great amount of effort, because several algebraic properties, that are related to the preservation of the balancing property of the admissible language of the intruder, should be formalized in the granularity of the underlying data structure (of finite sequences used in the specification). Among these properties, the most complex are related to the notion of linkage property, which allows for a systematic analysis of words of the admissible language of a potential saboteur, showing how he/she is unable to isolate private keys of other users under the assumption of balanced protocols. The difficulties that arose in conducting this formalization are also presented in this work.http://jfr.unibo.it/article/view/3720PVSformalization of security propertiesautomated theorem provingalgebraic specification |
| spellingShingle | Mauricio Ayala-Rincón Yuri Santos Rego Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model Journal of Formalized Reasoning PVS formalization of security properties automated theorem proving algebraic specification |
| title | Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model |
| title_full | Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model |
| title_fullStr | Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model |
| title_full_unstemmed | Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model |
| title_short | Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model |
| title_sort | formalization in pvs of balancing properties necessary for proving security of the dolev yao cascade protocol model |
| topic | PVS formalization of security properties automated theorem proving algebraic specification |
| url | http://jfr.unibo.it/article/view/3720 |
| work_keys_str_mv | AT mauricioayalarincon formalizationinpvsofbalancingpropertiesnecessaryforprovingsecurityofthedolevyaocascadeprotocolmodel AT yurisantosrego formalizationinpvsofbalancingpropertiesnecessaryforprovingsecurityofthedolevyaocascadeprotocolmodel |