Research Article
Formal Analysis of FPH Contract Signing Protocol Using Colored Petri Nets
@INPROCEEDINGS{10.1007/978-3-642-05284-2_7, author={Magdalena Payeras-Capell\'{a} and Maci\'{a} Mut-Puigserver and Andreu Isern-Dey\'{a} and Josep Ferrer-Gomila and Lloren\`{e} Huguet-Rotger}, title={Formal Analysis of FPH Contract Signing Protocol Using Colored Petri Nets}, proceedings={Security and Privacy in Communication Networks. 5th International ICST Conference, SecureComm 2009, Athens, Greece, September 14-18, 2009, Revised Selected Papers}, proceedings_a={SECURECOMM}, year={2012}, month={5}, keywords={contract signing protocol Coloured Petri Nets formal verification}, doi={10.1007/978-3-642-05284-2_7} }- Magdalena Payeras-Capellà
Macià Mut-Puigserver
Andreu Isern-Deyà
Josep Ferrer-Gomila
Llorenç Huguet-Rotger
Year: 2012
Formal Analysis of FPH Contract Signing Protocol Using Colored Petri Nets
SECURECOMM
Springer
DOI: 10.1007/978-3-642-05284-2_7
Abstract
An electronic contract signing protocol is a fair exchange protocol where the parties exchange their signature on a contract. Some contract signing protocols have been presented, and usually they come with an informal analysis. In this paper we use Colored Petri Nets to formally verify the fairness and the resistance to five previously described attacks of FPH contract signing protocol. We have modeled the protocol and the roles of the signers, a trusted third party, malicious signers as well as the role of an intruder. We have proven that the protocol is resistant to typical attacks. However, we have detected three cases where the protocol generates contradictory evidences. Finally, we have explained which should be the behavior of an arbiter to allow the resolution of these conflicting situations.
