关键词: 安全协议 进程代数 形式化验证 认证性 Objective Canal

Abstract:

Security protocols are used to provide secure communications over open network, which are essentially concurrent programs in distributed systems, and  can be described as a parallel composition system of multiple role-processes by process algebra By using abstract methods, the security protocols＇ proccess model can be transformed into a logic program. By computing the fixedpoint of the logic program, we can verify the parallel interleaved operations  of the security protocols＇ infinite sessions. This paper uses the Objective Carol language, and automatically translates the description of process alg  gebra for Security protocols into relative logic programs.

Key words: security protocol, process algebra, formal verification, authentication;Objective Canal