Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols
A computationally observational equivalence model for the Diffe-Hellman key agreement primitive was pro-posed and the soundness of the model was proved.Compared with prior works,this model can extend the power of the mechanized prover CryptoVerif directly.When applying the model to proving the publi...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2011-01-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/74420087/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841537768357888000 |
|---|---|
| author | FENG Chao ZHANG Quan TANG Chao-jing |
| author_facet | FENG Chao ZHANG Quan TANG Chao-jing |
| author_sort | FENG Chao |
| collection | DOAJ |
| description | A computationally observational equivalence model for the Diffe-Hellman key agreement primitive was pro-posed and the soundness of the model was proved.Compared with prior works,this model can extend the power of the mechanized prover CryptoVerif directly.When applying the model to proving the public-key Kerberos,the deficiency of the adversary’s capability was uncovered and an enhanced model for the adversary was presented.The model was vali-dated by verifying the public-key Kerberos in Diffie-Hellman mode with CryptoVerif automatically.Being different from current approaches,the verification procedure is both automatic and computationally sound. |
| format | Article |
| id | doaj-art-23eb2dd9b33b4d1e89614d2604a10b73 |
| institution | Kabale University |
| issn | 1000-436X |
| language | zho |
| publishDate | 2011-01-01 |
| publisher | Editorial Department of Journal on Communications |
| record_format | Article |
| series | Tongxin xuebao |
| spelling | doaj-art-23eb2dd9b33b4d1e89614d2604a10b732025-01-14T08:15:35ZzhoEditorial Department of Journal on CommunicationsTongxin xuebao1000-436X2011-01-013211812674420087Computationally sound mechanized proofs for Diffie-Hellman key exchange protocolsFENG ChaoZHANG QuanTANG Chao-jingA computationally observational equivalence model for the Diffe-Hellman key agreement primitive was pro-posed and the soundness of the model was proved.Compared with prior works,this model can extend the power of the mechanized prover CryptoVerif directly.When applying the model to proving the public-key Kerberos,the deficiency of the adversary’s capability was uncovered and an enhanced model for the adversary was presented.The model was vali-dated by verifying the public-key Kerberos in Diffie-Hellman mode with CryptoVerif automatically.Being different from current approaches,the verification procedure is both automatic and computationally sound.http://www.joconline.com.cn/zh/article/74420087/security protocolsDiffie-Hellman primitivesKerberos protocolmechanized proofs |
| spellingShingle | FENG Chao ZHANG Quan TANG Chao-jing Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols Tongxin xuebao security protocols Diffie-Hellman primitives Kerberos protocol mechanized proofs |
| title | Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols |
| title_full | Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols |
| title_fullStr | Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols |
| title_full_unstemmed | Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols |
| title_short | Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols |
| title_sort | computationally sound mechanized proofs for diffie hellman key exchange protocols |
| topic | security protocols Diffie-Hellman primitives Kerberos protocol mechanized proofs |
| url | http://www.joconline.com.cn/zh/article/74420087/ |
| work_keys_str_mv | AT fengchao computationallysoundmechanizedproofsfordiffiehellmankeyexchangeprotocols AT zhangquan computationallysoundmechanizedproofsfordiffiehellmankeyexchangeprotocols AT tangchaojing computationallysoundmechanizedproofsfordiffiehellmankeyexchangeprotocols |