Done
The control mechanisms (XRBAC and XFloor) were modeled by using Colored Petri Nets with time. Formal verification and analysis to prove the correctness of the mechanisms were done using state space functions provided by the CP-nets. But the analysis is not completed yet. The current results show the mechanism model is working as expected. Also the modeled mechanism used communication service provided by the CP-nets to connect the model to external process. Without the communication service, we can simulate our XML access type decision service by randomly generating the classified access types (invalid, implicit, exclusive, shared, and released) in the mechanism model. But I thought it will be more nice if we can test the correctness of the classification decisions service codes used in practical programming of universal collaboration framework. The simulation result also shows the classification decision service is working as expected.
Summary
1. The control mechanisms (XRBAC and XFloor) were modeled by using Colored Petri Nets with time.
2. The classification decision service was verified by the CP-nets simulation methods. This service means XML requests are parsed and one of the classified access types from parsed request are returned for use of control decision in the mechanism model.
3. Informal introduction of the control mechanism model was done.
4. Formal definition of the control mechanism model was done.
5. Using state spaces (also called occurrence graphs) analysis functions provided by the CP-nets, simulation results of the mechanism model are being analyzed.
- some results : analysis results generated from state space analysis functions show the modeling of our control mechanisms is working as expected.
6. The draft report will be finished within roughly next 2 weeks.
Next Research
- Experiment issues - coming soon
mobile vs. non-mobile device,
coarse-grained vs. fine-grained access control,
fine-grained (level (depth) 1) vs. fine-grained access control (level (depth)2))