A game-based verification of non-repudiation and fair exchange protocols

被引：12

作者：

Kremer, Steve ^{[1
]}

Raskin, Jean-François ^{[1
]}

机构：

[1] Departement d'Informatique, Faculté des Sciences, Universite Libre de Bruxelles, Bruxelles

来源：

Journal of Computer Security | 2003年 / 11卷 / 03期

关键词：

Alternating temporal logic - Alternating transition systems - Game based model - Game-based verification - Non-repudiation protocols;

D O I：

10.3233/JCS-2003-11307

中图分类号：

学科分类号：

摘要：

In this paper, we report on a recent work for the verification of non-repudiation protocols. We propose a verification method based on the idea that non-repudiation protocols are best modeled as games. To formalize this idea, we use alternating transition systems, a game based model, to model protocols and alternating temporal logic, a game based logic, to express requirements that the protocols must ensure. This method is automated by using the model-checker Mocha, a model-checker that supports the alternating transition systems and the alternating temporal logic. Several optimistic protocols are analyzed using Mocha.

引用

页码：399 / 429

页数：30

共 30 条

[1]

Alur R., Henzinger T., Kupferman O., Alternating-time temporal logic, Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pp. 100-109, (1997)

[2]

Alur R., Henzinger T., Mang F., Qadeer S., Rajamani S., Tasiran S., MOCHA: Modularity in model checking, Lecture Notes in Computer Science, 1427, pp. 521-525, (1998)

[3]

Asokan N., Schunter M., Waidner M., Optimistic protocols for fair exchange, 4th ACM Conference on Computer and Communications Security, (1997)

[4]

Asokan N., Shoup V., Waidner M., Asynchronous protocols for optimistic fair exchange, Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, IEEE Computer Society, Technical Committee on Security and Privacy, pp. 86-99, (1998)

[5]

Asokan N., Shoup V., Waidner M., Optimistic fair exchange of digital signatures, Advances in Cryptology - EUROCRYPT'98, Volume 1403 of Lecture Notes in Computer Science, 1998, pp. 591-606

[6]

Ben-Or M., Goldreich O., Micali S., Rivest R.L., A fair protocol for signing contracts, IEEE Transactions on Information Theory, 36, 1, pp. 40-46, (1990)

[7]

Boneh D., Naor M., Timed commitments, Advances in Cryptology: Proceedings of Crypto 2000, Volume 1880 of Lecture Notes in Computer Science, pp. 236-254, (2000)

[8]

Boyd C., Kearney P., Exploring fair exchange protocols using specification animation, The Third International Workshop on Information Security - ISW2000, Lecture Notes in Computer Science, Australia, Springer-Verlag, 2000

[9]

Burrows M., Abadi M., Needham R., A logic of authentication, from proceedings of the royal society, William Stallings, Practical Cryptography for Data Internetworks, 426, 1871, (1989)

[10]

Chiou G., Chen W., Secure broadcasting using the secure lock, IEEE Transactions on Software Engineering, 15, 8, pp. 929-934, (1989)

← 1 2 3 →