To search, Click below search items. |
| All Published Papers Search Service |
|
|
|
Title |
Process Calculus and Horn Clauses-Based Deduction in the Verification of Security Protocols |
|
Author |
Nguyen Truong Thang, Khuat Thanh Son |
| Citation |
Vol. 20 No. 5 pp. 11-17 |
|
Abstract |
In security protocols, there is a well-known theorem about the undecidability of security properties such as secrecy and authentication. That is, it is not possible to develop an automatic procedure that in finite time and space always decides correctly whether or not a security property holds for any given protocol model. With respect to the importance of security protocols in the Internet nowadays, to deal with this limitation, several approaches imposing assumptions in the model are presented in order to make protocol design more reliable. These approaches are classified into relaxing some restrictions on the theorem requirements. This paper presents in details a notable technique, namely the combination of process calculus and Horn clauses-based reasoning in an automatic decision procedure. In particular, the characteristics of process calculus for modeling and Horn clauses for automatic verification are presented. Some strengths and weaknesses of this combination compared with other approaches are also given. This combination technique is implemented in ProVerif an automatic symbolic verifier of security protocols. |
|
Keywords |
Undecidability, security protocols, process calculus, Horn clauses, formal verification. |
|
URL |
