Opacity generalised to transition systems

OpacityGeneralisedtoTransitionSystems

JeremyW.Bryans1,MaciejKoutny1,LaurentMazar´e2,andPeterY.A.Ryan1

1SchoolofComputingScience,UniversityofNewcastle,NewcastleuponTyne,NE17RU,UnitedKingdom2LaboratoireVERIMAG;2,av.deVignates,Gi`eres,France

Abstract.Recently,opacityhasprovedtobeapromisingtechniquefordescribingsecurityproperties.MuchoftheworkhasbeencouchedintermsofPetrinets.Here,weextendthenotionofopacitytothemodeloflabelledtransitionsystemsandgeneraliseopacityinordertobet-terrepresentconceptsfromtheworkoninformationflow.Inparticular,weestablishlinksbetweenopacityandtheinformationflowconceptsofanonymityandnon-interferencesuchasnon-inference.Wealsoinvesti-gatewaysofverifyingopacitywhenworkingwithPetrinets.Ourworkisillustratedbyanexamplemodellingrequirementsuponasimplevotingsystem.Keywords:opacity,non-deducibility,anonymity,non-interference,Petrinets,observablebehaviour,labelledtransitionsystems.

Introduction

Thenotionofsecrecyhasbeenformulatedinvariouswaysinthecomputer

securityliterature.However,twoviewsofsecurityhavebeendevelopedover

theyearsbytwoseparatecommunities.Thefirstonestartsfromthenotion

ofinformationflow,describingtheknowledgeanintrudercouldgaininterms

ofpropertiessuchasnon-deducibilityornon-interference.Thesecondviewwas

initiatedbyDolevandYao’sworkandfocussedinitiallyonsecurityprotocols[7].

Theideahereistodescribeproperlythecapabilityoftheintruder.Somevariants

ofsecrecyappeared,suchasstrongsecrecy,givingmoreexpressivitythanthe

classicalsecrecypropertybutstilllackingtheexpressivityofinformationflow

concepts.

Recently,opacityhasprovedtobeapromisingtechniquefordescribingse-

curityproperties.MuchoftheworkhasbeencouchedintermsofPetrinets.

Inthispaper,weextendthenotionofopacitytothemoregeneralframework

oflabelledtransitionsystems.Whenusingopacitywehavefine-grainedcontrol

overtheobservationcapabilitiesoftheplayers,andweshowonewaythatthese

capabilitiesmaybeencoded.Theessentialideaisthatapredicateisopaqueifan

observerofthesystemwillneverbeabletoestablishthetruthofthatpredicate.

Inthefirstsection,afterrecallingsomebasicdefinitions,wepresentagen-

eralisationofopacity,andshowhowthisspecialisesintothethreepreviously

definedvariants.InSection2,weshowhowopacityisrelatedtopreviouswork

insecurity.InSection3,weconsiderthequestionofopacitychecking.After

restrictingourselvestoPetrinets,wegivesomedecidabilityandundecidability

properties.Asopacityisundecidableassoonasweconsidersystemswithinfinite

numberofstates,wepresentanapproximationtechniquewhichmayprovidea2J.W.Bryans,M.Koutny,L.Mazar´eandP.Y.A.Ryan

wayofmodelcheckingeveninsuchcases.Finally,inSection4,weconsidera

votingscheme,andshowhowtheapproximationtechniquemightbeused.All

theproofsareavailablein[6].

1BasicDefinitions

ThesetoffinitesequencesoverasetAwillbedenotedbyA∗,andtheempty

sequenceby󰀔.Thelengthofafinitesequenceλwillbedenotedbylen(λ),and

itsprojectionontoasetB⊆Abyλ|B.

Definition1Alabelledtransitionsystem(LTS)isatupleΠ=(S,L,∆,S0),

whereSisthe(potentiallyinfinite)setofstates,Listhe(potentiallyinfinite)

setoflabels,∆⊆S×L×Sisthetransitionrelation,andS0isthenonempty

(finite)setofinitialstates.WeconsideronlydeterministicLTSs,andsoforany

transitions(s,l,s󰀅),(s,l,s󰀅󰀅)∈∆,itisthecasethats󰀅=s󰀅󰀅1.

ArunofΠisapair(s0,λ),wheres0∈S0andλ=l1...lnisafinitesequenceof

labelssuchthattherearestatess1,...,snsatisfying(si−1,li,si),fori=1,...,n.

Wewilldenotethestatesnbys0⊕λ,andcallitreachablefroms.

Thesetofallrunsisdenotedbyrun(Π),andthelanguagegeneratedbyΠis

definedasL(Π)={λ|∃s0∈S0:(s0,λ)∈run(Π)}.

LetΠ=(S,L,∆,S0)beanLTSfixedfortherestofthissection,andΘbe

asetofelementscalledobservables.Wewillnowaimatmodellingthedifferent

capabilitiesforobservingthesystemmodelledbyΠ.First,weintroduceageneral

observationfunctionandthen,specialiseittoreflectlimitedinformationabout

runsavailabletoanobserver.

Definition2Anyfunctionobs:run(Π)→Θ∗isanobservationfunction.It

iscalledlabel-basedand:static/dynamic/orwellian/m-orwellian(m≥1)if

respectivelythefollowinghold(belowλ=l1...ln):

–static:thereisamappingobs󰀅:L→Θ∪{󰀔}suchthatforeveryrun(s,λ)

ofΠ,obs(s,λ)=obs󰀅(l1)...obs󰀅(ln).

–dynamic:thereisamappingobs󰀅:L×L∗→Θ∪{󰀔}suchthatforeveryrun

(s,λ)ofΠ,obs(s,λ)=obs󰀅(l1,󰀔)obs󰀅(l2,l1)...obs󰀅(ln,l1...ln−1).

–orwellian:thereisamappingobs󰀅:L×L∗→Θ∪{󰀔}suchthatforevery

run(s,λ)ofΠ,obs(s,λ)=obs󰀅(l1,λ)...obs󰀅(ln,λ).

–m-orwellian:thereisamappingobs󰀅:L×L∗→Θ∪{󰀔}suchthatfor

everyrun(s,λ)ofΠ,obs(s,λ)=obs󰀅(l1,κ1)...obs󰀅(ln,κn),wherefori=

1,...,n,κi=lmax{1,i−m+1}lmax{1,i−m+1}+1...lmin{n,i+m−1}.

Ineachoftheabovefourcases,wewilloftenuseobs(λ)todenoteobs(s,λ)

whichispossibleasobs(s,λ)doesnotdependons.

Notethatallowingobs󰀅toreturn󰀔allowsonetomodelinvisibleactions.The

differentkindsofobservablefunctionsreflectdifferentcomputationalpowerof

theobservers.Staticfunctionscorrespondtoanobserverwhichalwaysinterprets

1AnondeterministicLTScanbetransformedintoadeterministiconethrougharelabelingthatassignsauniquelabeltoeachtransition.