LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory
The π-calculus is a basic theory of mobile communication based on the notion of interaction, which, is aimed at analyzing and modeling the behaviors of communication processes in communicating and mobile systems, and is widely applied to the security analysis of cryptographic protocol’s design and i...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2024-01-01
|
| Series: | IET Information Security |
| Online Access: | http://dx.doi.org/10.1049/2024/2634744 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832546261546303488 |
|---|---|
| author | Fusheng Wu Jinhui Liu Yanbin Li Mingtao Ni |
| author_facet | Fusheng Wu Jinhui Liu Yanbin Li Mingtao Ni |
| author_sort | Fusheng Wu |
| collection | DOAJ |
| description | The π-calculus is a basic theory of mobile communication based on the notion of interaction, which, is aimed at analyzing and modeling the behaviors of communication processes in communicating and mobile systems, and is widely applied to the security analysis of cryptographic protocol’s design and implementation. But the π-calculus does not provide seamless logical security analysis, so the logical flaws in the design and the implementation of a cryptographic protocol cannot be discovered in time. This paper introduces logical rules and logical proofs, binary tree, and the KMP algorithm and proposes a new extension of the π-calculus theory, a logical security analysis method, and an algorithm. The aim is to analyze whether there are logical flaws in the design and the implementation of a cryptographic protocol, to ensure the security of the cryptographic protocol when it is encoded into software and implemented. This paper presents the logical security proof and analysis of the TLS1.3 protocol’s interactional implementation process. Empirical results show that the additional extension theory, the logical security analysis method, and the algorithm can effectively analyze whether there are logical flaws in the design and the implementation of a cryptographic protocol. |
| format | Article |
| id | doaj-art-541d3f1c0d264b89a51c07c75b025b54 |
| institution | Kabale University |
| issn | 1751-8717 |
| language | English |
| publishDate | 2024-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | IET Information Security |
| spelling | doaj-art-541d3f1c0d264b89a51c07c75b025b542025-02-03T07:23:25ZengWileyIET Information Security1751-87172024-01-01202410.1049/2024/2634744LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension TheoryFusheng Wu0Jinhui Liu1Yanbin Li2Mingtao Ni3Guizhou Key Laboratory of Economic System SimulationSchool of CybersecuritySchool of SoftwareSchool of Electronic Information and Artificial IntelligenceThe π-calculus is a basic theory of mobile communication based on the notion of interaction, which, is aimed at analyzing and modeling the behaviors of communication processes in communicating and mobile systems, and is widely applied to the security analysis of cryptographic protocol’s design and implementation. But the π-calculus does not provide seamless logical security analysis, so the logical flaws in the design and the implementation of a cryptographic protocol cannot be discovered in time. This paper introduces logical rules and logical proofs, binary tree, and the KMP algorithm and proposes a new extension of the π-calculus theory, a logical security analysis method, and an algorithm. The aim is to analyze whether there are logical flaws in the design and the implementation of a cryptographic protocol, to ensure the security of the cryptographic protocol when it is encoded into software and implemented. This paper presents the logical security proof and analysis of the TLS1.3 protocol’s interactional implementation process. Empirical results show that the additional extension theory, the logical security analysis method, and the algorithm can effectively analyze whether there are logical flaws in the design and the implementation of a cryptographic protocol.http://dx.doi.org/10.1049/2024/2634744 |
| spellingShingle | Fusheng Wu Jinhui Liu Yanbin Li Mingtao Ni LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory IET Information Security |
| title | LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory |
| title_full | LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory |
| title_fullStr | LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory |
| title_full_unstemmed | LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory |
| title_short | LπCET: A Logic Security Analysis for Cryptographic Protocols Based on π-Calculus Extension Theory |
| title_sort | lπcet a logic security analysis for cryptographic protocols based on π calculus extension theory |
| url | http://dx.doi.org/10.1049/2024/2634744 |
| work_keys_str_mv | AT fushengwu lpcetalogicsecurityanalysisforcryptographicprotocolsbasedonpcalculusextensiontheory AT jinhuiliu lpcetalogicsecurityanalysisforcryptographicprotocolsbasedonpcalculusextensiontheory AT yanbinli lpcetalogicsecurityanalysisforcryptographicprotocolsbasedonpcalculusextensiontheory AT mingtaoni lpcetalogicsecurityanalysisforcryptographicprotocolsbasedonpcalculusextensiontheory |