Cryptofraglets reloaded
Bioinspired Security Modeling of a RFID Protocol and Properties
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.- Fraglets specification: fraglets.maude
- Fraglets rules specification: fraglets.rules.maude
- Cryptofraglets rules specification: cryptofraglets.rules.maude
- RIPP-FS protocol specification: rippfs.test.maude
- RIPP-FS protocol key secrecy: rippfs.istagkeysecret.maude
- RIPP-FS protocol tag privacy: rippfs.tagprivacy.maude
- RIPP-FS protocol forward secrecy: rippfs.forwardsecrecy.maude
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
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