This talk will describe one of the analysis tools that we have been developing for the Trust4all project. It is an extension of the work on Q-automata that has previously been at an AGC talk. Members of SEN2 have helped implement some of this work in mCRL.

We present a powerful and flexible method for automatically checking the secrecy of values inside components. In our framework an attacker may monitor the external communication of a component, interact with it and monitor the components resource usage. We use an automata model of components in which each transition is tagged with resource usage information. We extend these automata to pass values and say that a value is kept secret if the observable behaviour of the automata is the same for all possible instantiations of that value. If a component leaks some, but not all of the information about its secret we use a notion of secrecy degree to quantify the worst-case leakage. We show how this secrecy degree can be automatically calculated, for values from a finite domain, using the mCRL process algebraic verification toolset.