Executable Specification of Cryptofraglets in Maude for Security Verification

Fabio Martinelli; Marinella Petrocchi

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

Download

458 downloads

Cite: BibTeX Plain Text

@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 Martinelli¹, Marinella Petrocchi¹

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.

Keywords: Fraglets cryptofraglets threat model security protocols Maude

Published: 2012-05-28

: http://dx.doi.org/10.1007/978-3-642-12808-0_2