Specifying Security for Computer Supported Collabo

SpecifyingSecurityforComputerSupportedCollaborativeWorkingSimonN.FoleyJeremyL.JacobyAbstractCSCWsystemsprovidecomputersupporttofacilitatecooperationbe-tweenusers.ThispaperproposesanapproachtotheformalspecicationofsecurityrequirementsforCSCWapplications,whereaCSCWappli-cationisviewedasacollectionofactivitiesthatusersmayparticipatein.Thespecicationapproachisstraightforward,andcanbeusedtocaptureawidevarietyofsecurityrequirements,includingintegrityandcondentiality.Itisillustratedwithacasestudyofasecureelectronicexaminationssystem.1IntroductionThepurposeofComputerSupportedCollaborativeWorking(CSCW)istopro-videcomputersupportthatfacilitatescollaborationandcooperationbetweenusers.Thissupportmaybeassimpleastheprovisionofelectronicmailfacili-ties,givingusersthefreedomtocooperateinanunstructuredmanner.Itmaybeassophisticatedassomeoftheapplicationsinconcurrentengineeringwhichexerciseahighdegreeofcontrolovertheactionsoftheparticipantsinanengi-neeringdesignactivity.AnexampleisreportedbyBowenandBahler[1];thesystemtheydescribemediatesconictsbetweenuser’scontributionstowardsanoveralldesign.CSCWsupportmaybeacrossasinglecomputerenvironment,ormoretypically,acrossnetworksofheterogeneoussystems.ResearchinCSCWandgroupwareevolvedfromworkonDecisionSupportSystems[9].AgreatdealofworkhasbeendoneonthetechnologicalaspectsofCSCW:theproblemsofhowoneactuallyprovidescomputersupportforcooperation.Introductionstothesubjectmaybefoundintheliterature[17,18].InthispaperweareinterestedinwhatismeantbysecurityinCSCWappli-cations.Todothis,werequireaclearandformaldenitionofwhatismeantbyDepartmentofComputerScience,UniversityCollege,Cork,IrelandyDepartmentofComputerScience,TheUniversityofYork,Heslington,YorkYO15DD,England1aCSCWapplicationandthesupportthatwewouldexpecttheCSCWsystemtoprovide.Wearenotconcernedwith,atleastatthisstage,thetechnologicalaspectsofhowsecurityshouldbeenforced.ButweareconcernedwithhowonemightspecifythesecurityrequirementsforaCSCWapplicationandtheresultingpropertiesthataCSCWsystem,providingsupportfortheapplication,shoulduphold.Whileintegritysecurityrequirementscanbecharacterizedassafetyorfunctionalityproperties,informationowbasedsecurityrequirementsaredescribedintermsof(hardertoreasonabout)condentialityproperties[13].Ourproposedspecicationapproachcanbeusedtocapturebothtypesofrequirement.AsimplecasestudymotivatesourproposalofwhatcharacterizesaCSCWsystem,andthesecuritypropertiesthatitshouldmaintain.Thecasestudyisasecureelectronicexaminationsystem,wheretheusers(professors,lecturersandstudents)cooperateinthesetting,takingandgradingofexaminations.Thecasestudycontainsmanysecurityrequirements.Forexample,integrityrequirementssuchas,onlylecturersappointedassettersofanexampapermaywriteanexampaper,andcondentialityrequirementssuchas,astudentmaynotlearnordeduceanythingaboutthecontentsofanexampaperuntilithasbeenreleased.Thesecurityrequirementsforthiscasestudyareexpressible,inanaturalway,usingourspecicationapproach.Tooursurprise,allofthecondentialityrequirementswereexpressible,usingthesameinformation-owproperty.Thisisoneofourmainconclusions.ACSCWapplicationmaybeviewedasacollectionofactivitiesthatusersmayparticipatein.Section2describeshowusersmayjoin,leaveandparticipatein,anactivityduringitslifetime.OurperspectiveofCSCWapplications,whileabstract,doesappeartoconformtothecriteriagivenbyReinhardetal.[21]toidentifyCSCWsystems.Basedonthisperspective,Section3investigateshowwemightformallyspecifyfunctionalitypropertiesforCSCWactivities.ThisgivesrisetoanumberofsafetypropertiesthataCSCWsystem,supportingtheactivity,shoulduphold.OurapproachisillustratedinSection4bytheformalspecicationoftheactivitiesofaSecureElectronicExaminations(SEE)system.MuchoftheSEEcasestudyisanexampleofintegrityandaccess-controlstylesecurityspecications.Thesesafety-propertybasedrequirementsspecifycontrolsoverwhether,andhow,usersmayparticipateinactivities.Section5investigateshowwemightspecifycondentialitypropertiesforaCSCWsystem.Theessenceofourdenitionofcondentialityisthatinformationmaynotowfromtheparticipantsinanactivitytothenon-participants,duringthelifetimeoftheactivity.Giventhisdenition,weshowhowthecondentialityrequirementsfortheSEEsystemcanbeexpressed.Wealsoprovideanunwindingtheoremwhichdenescondentialityintermsofstatesandstatetransitions.InSection6weleaveourmaincasestudyforabrieflookatsomeothers.AglossaryofthemathematicalnotationusedisgiveninAppendixB.22ComputerSupportedCollaborativeWorkingWeviewacollaborationassomeagreedactivitythatanumberofdierentusersmayparticipatein.ACSCWsystemisasystemthatprovidessupportfortheseactivities,ensuringthatuserparticipationinactivitiesisinaccordancetotherequirementsoftheindividualactivities.Inthissectionweproposeanapproachtoorganizingthedescriptionoftherequirementsofanactivity.Example1Inauniversity,anumberofpeoplemaybeinvolvedinthesettingofanexaminationpaper.Initially,thechairforthesubjectconcernedisrespon-sibleforappointingstatosetthepaper.Onceappointed,amemberofstamaysetallorpartofapaper;thistypicallyinvolvesdevisingaseri