Security and Privacy in Communication Networks. 5th International ICST Conference, SecureComm 2009, Athens, Greece, September 14-18, 2009, Revised Selected Papers

Research Article

Formal Analysis of FPH Contract Signing Protocol Using Colored Petri Nets

Download58 downloads
  • @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
Magdalena Payeras-Capellà1,*, Macià Mut-Puigserver1,*, Andreu Isern-Deyà1,*, Josep Ferrer-Gomila1,*, Llorenç Huguet-Rotger1,*
  • 1: Universitat de les Illes Balears
*Contact email: mpayeras@uib.es, macia.mut@uib.es, andreupere.isern@uib.es, jlferrer@uib.es, l.huguet@uib.es

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.