This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
15th IEEE Computer Security Foundations Workshop (CSFW'02)
Game Analysis of Abuse-free Contract Signing
Cape Breton, Nova Scotia, Canada
June 24-June 26
ISBN: 0-7695-1689-0
ASCII Text
x 
 
Steve Kremer, Jean-François Raskin, "Game Analysis of Abuse-free Contract Signing," Computer Security Foundations Workshop, IEEE, pp. 206, 15th IEEE Computer Security Foundations Workshop (CSFW'02), 2002.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.2002.1021817,
author = {Steve Kremer and Jean-François Raskin},
title = {Game Analysis of Abuse-free Contract Signing},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {2002},
issn = {1063-6900},
pages = {206},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2002.1021817},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - Game Analysis of Abuse-free Contract Signing
SN - 1063-6900
SP
EP
A1 - Steve Kremer,
A1 - Jean-François Raskin,
PY - 2002
KW - null
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
Steve Kremer, Université Libre de Bruxelles
Jean-François Raskin, Université Libre de Bruxelles
In this paper we report on the verification of two contract signing protocols. Our verification method is based on the idea of modeling those protocols as games, and reasoning about their properties as strategies for players. We use the formal model of alternating transition systems to represent the protocols and alternating-time temporal logic to specify properties.The paper focuses on the verification of abuse-freeness, relates this property to the balance property, previously studied using two other formalisms, shows some ambugities in the definition of abuse-freeness and proposes a new, stronger definition. Formal methods are not only useful here to verify automatically the protocols but also to better understand their requirements (balance and abuse-freeness are quite complicated and subtle properties).
Citation:
Steve Kremer, Jean-François Raskin, "Game Analysis of Abuse-free Contract Signing," csfw, pp.206, 15th IEEE Computer Security Foundations Workshop (CSFW'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.