Research Article
Executable Specification of Cryptofraglets in Maude for Security Verification
482 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
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.
Copyright © 2009–2024 ICST
