Describing and verifying cryptographic protocal using PI-calculus

Author

Xiao-Pei, Zhang ; Wen-jun, Luo ; Xiang, Li

Author_Institution

Inst. of Comput. Sci., Guizhou Univ., Guiyang

fYear

2008

Firstpage

280

Lastpage

284

Abstract

Using formal method is an effective methodology for modeling and verifying software system. Describing and verifying cryptographic protocol by formal method is an important research. Pi-calculus is a kind of mobile process algebra which can be used to model concurrent and dynamic system. Mobility workbench (MWB) is an automatic tool for pi-calculus and can be used for analyzing and verifying mobile concurrent system described by pi-calculus. In this paper we analyze Aziz-Diffie wireless communication security protocol using formal method based pi-calculus and verifying the attack of this protocol by MWB.

Keywords

cryptographic protocols; pi calculus; program verification; Aziz-Diffie wireless communication security protocol; cryptographic protocol; formal method; mobile process algebra; mobility workbench; pi-calculus; software verification; Algebra; Communication system security; Computer science; Concurrent computing; Cryptographic protocols; Cryptography; Mobile computing; Software systems; Wireless application protocol; Wireless communication; Aziz-Diffie; MWB; mobile process; pi-calculus;

fLanguage

English

Publisher

ieee

Conference_Titel

Anti-counterfeiting, Security and Identification, 2008. ASID 2008. 2nd International Conference on

Conference_Location

Guiyang

Print_ISBN

978-1-4244-2584-6

Electronic_ISBN

978-1-4244-2585-3

Type

conf

DOI

10.1109/IWASID.2008.4688400

Filename

4688400