Cryptofraglets reloaded
Bioinspired Security Modeling of a RFID Protocol and Properties

Marinella Petrocchi, Institute of Informatics and Telematics of CNR, marinella.petrocchi@iit.cnr.it
Paolo Santi, MIT-Fraunhofer Ambient Mobility, Senseable City Lab, psanti@mit.edu
Angelo Spognardi, Institute of Informatics and Telematics of CNR, angelo.spognardi@iit.cnr.it

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. In this paper, we propose an executable specification of fraglets (and fraglets-based cryptographic protocols) in the rewriting logic-based Maude interpreter to model a RFID protocol and its security properties.

Maude implementation

Here are the source files of our Maude implementation. You can also download all the files with this package: cryptofraglets.2.0.tar.gz

Instructions

To run our Maude specifications:
  • copy all the files in the same directory
  • move to the directory
  • execute any of the RIPP-FS files with the load command
Example:
Maude> cd cryptofraglets.2.0
Maude> load rippfs.test.maude
==========================================
frewrite in RIPPFS : ((['kzero-l 'klast],['dl delta],['tl 'tnow],['tnl 'tl
    'tnow],[hashi 'authval max-delta 'auth10],[match 'authval mcast anyone
    'authl],[mcast anyone 'tl 'tnow],[matchs 'dl match 'kzero-l hashi
    'expkeytag-l],[match 'expkeytag-l match 'tl hmac 'exphmac],[matchs
    'hmac-tag match 'ifoktag hv 'exphmac],[matchs 'hmac-tag match 'ifkotag hnv
    'exphmac],['ifkotag 'DOH],['ifoktag 'OK]) @ reader) ; (empty @ malreader) ;
    (['klast-l 'klast],['dl delta],[hashi 'authlast max 'auth10],[matchs 'dl
    matchs 'authl hashi 'authnew],[matchs 'authlast match 'ifauthl hv
    'authnew],[matchs 'authlast match 'ifnotauthl hnv 'authnew],['ifauthl
    matchs 'dl match 'klast-l hashi 'know-l],[matchs 'know-l matchs 'tl hmac
    'tagauth-l],[match 'tagauth-l mcast anyone 'hmac-tag],['ifnotauthl mcast
    anyone h('PRNG)]) @ tag .
rewrites: 67 in 4ms cpu (1ms real) (16750 rewrites/second)
result FragletStoreSet: ((['authl h(h(h(h('auth10))))],['hmac-tag h(h(h(
    'klast)) || 'tnow)],['tl 'tnow]) @ malreader) ; ((['OK],['dl 2],['hmac-tag
    h(h(h('klast)) || 'tnow)],['tnl 'tl 'tnow],[hnv 'exphmac h(h(h('klast)) ||
    'tnow) 'DOH]) @ reader) ; (['authl h(h(h(h('auth10))))],['authlast h(h(h(h(
    h(h('auth10))))))],['dl 2],['know-l h(h('klast))],['tl 'tnow],[hnv 'authnew
    h(h(h(h(h(h('auth10)))))) mcast (tag % reader % malreader) h('PRNG)]) @ tag