[Top] [Prev] [Next]

Example 2b

*bank: @ks[av us bmon] +<+ @us[bmon us exts]

This example uses the same Copland phrase as in ex2, but we now want to disallow deep and recent corruptions. When we run Chase with the following ex2b.gln file, no models are produced, therefore, according to Chase there are no adversary actions that can produce evidence that will pass appraisal if deep and recent corruptions are not considered.

[ bound = 500, limit = 5000, input_order ]

% Assume adversary avoids detection at our main measurement
% event. Others can be added.
l(V) = msp(us, M, us, exts, X)
 => corrupt_at(us, exts, V).

% Assumptions about system dependencies.
depends(ks, C, ks, av) => false. 
depends(us, C, us, bmon) => false.
depends(us, C, us, exts) => false.

% Axioms defining "deep" components
% We don't want to see models with deep corruptions
l(V) = cor(ks, M) => false.

% Axiom defining which components might be recently corrupted
prec(V, V1) & l(V1) = cor(P,C) & ms_evt(V)
 => false. 

m4_include(`ex2b.gli')m4_dnl

m4_include(`ex2b_dist.gli')m4_dnl

m4_include(`thy.gli')m4_dnl

Note, this .gln is the same as in ex1b except for the include statements at the bottom.

Analysis

As stated above and in contrast to the other examples, no models are included in this analysis because no models were generated by Chase under the assumptions. This result is important since in some systems, we may be confident deep corruptions are not possible or are not a reasonable expectation for the adversary to corrupt. We might assume the same about recent corruptions and consider them too hard for the adversary. Under these assumptions, we see that the ordering of the attestations in our phrase are quite strong. We also see that by changing our assumptions in the .gln, Chase allows us to interactively explore different scenarios and choose where we think the greatest risk of compromise lies. Just because there are no models in this example, does not mean there is no risk, but that the risk is characterized as recent or deep.

Click here to move on to the next variation of this example.