Skip to Main content Skip to Navigation
Master Thesis

Description de propriétés de sécurité pour un processus de validation/vérification

Abstract : The work presented in this report deals with the validation of access control dened through security policies. We are interested in the validation by means of test generation based on a security model, written in B. We use the Meca tool, which takes as input a functional model and a description of the security policy, both expressed as B models. Meca generates a security kernel, that is in charge of intercepting the access of the subjects to the objects, and restricts the behaviors to those that satisfy the security requirements. We present a complete case study, led on an electronic purse case study, using a discretionary access control policy.
Document type :
Master Thesis
Complete list of metadata
Contributor : Cnam - Service Commun De La Documentation - Bibliothèque Centrale Connect in order to contact the contributor
Submitted on : Monday, October 4, 2010 - 3:42:08 PM
Last modification on : Monday, February 21, 2022 - 3:38:12 PM
Long-term archiving on: : Wednesday, January 5, 2011 - 2:46:03 AM


  • HAL Id : dumas-00523234, version 1



Thierry Moutet. Description de propriétés de sécurité pour un processus de validation/vérification. Cryptographie et sécurité [cs.CR]. 2010. ⟨dumas-00523234⟩



Record views


Files downloads