발간년도 : [2019]
| 논문정보 |
|
| 논문명(한글) |
[Vol.14, No.6] Formal Specification of Cryptographic Security Protocols |
|
| 논문투고자 |
Gyesik Lee |
|
| 논문내용 |
We introduce a way of formal specification of cryptographic security protocols. We demonstrate how to use formal methods in verifying cryptographic security protocols. Each step of the verification is explained with a concrete example, the Needham-Schroeder public-key protocol. The style of describing the syntax is similar to that of the tool Scyther. It is simple and intuitive to use for the specification of security protocols. Our description corresponds also to the basic concepts of the tool ProVerif. Specifications of cryptographic security protocols are represented at the most abstract level: Messages are terms constructed from symbols and the attacker is modeled as a formal process. A formal language L = (V, C, R, F) for public-key protocols consists of a set V of variables for received messages, a set C of local constant symbols, a set R of role name symbols, and a set F of function symbols. Then a protocol describes the behavior of each of the roles such as initiator, responder, key server, etc. In the specification, the behavior of each role is formalized as a transition system describing how to create messages, how to react to the received messages, and how to manipulate messages. Among many security properties, we illustrate how to formally handle secrecy and authentication. |
|
| 첨부논문 |
|
|
|
|
|
자료실 > 논문지 
