Bioinspired Models of Network, Information, and Computing Systems. 4th International Conference, BIONETICS 2009, Avignon, France, December 9-11, 2009, Revised Selected Papers

Research Article

Executable Specification of Cryptofraglets in Maude for Security Verification

Download284 downloads
  • @INPROCEEDINGS{10.1007/978-3-642-12808-0_2,
        author={Fabio Martinelli and Marinella Petrocchi},
        title={Executable Specification of Cryptofraglets in Maude for Security Verification},
        proceedings={Bioinspired Models of Network, Information, and Computing Systems. 4th International Conference, BIONETICS 2009, Avignon, France, December 9-11, 2009, Revised Selected Papers},
        proceedings_a={BIONETICS},
        year={2012},
        month={5},
        keywords={Fraglets cryptofraglets threat model security protocols Maude},
        doi={10.1007/978-3-642-12808-0_2}
    }
    
  • Fabio Martinelli
    Marinella Petrocchi
    Year: 2012
    Executable Specification of Cryptofraglets in Maude for Security Verification
    BIONETICS
    Springer
    DOI: 10.1007/978-3-642-12808-0_2
Fabio Martinelli1, Marinella Petrocchi1
  • 1: IIT-CNR, Pisa

Abstract

Fraglets are computation fragments flowing through a computer network. They implement a chemical reaction model where computations are carried out by having fraglets react with each other. The strong connection between their way of transforming and reacting and some formal rewriting system makes a fraglet program amenable to verification. Starting from a threat model which we intend to use for modeling secure communication protocols with fraglets, we propose an executable specification of fraglets (and fraglets-based cryptographic protocols) in the rewriting logic-based Maude interpreter.