It is increasingly important to analyze system security quantitatively using concepts such
as trust, reputation, cost, and risk. This requires a thorough understanding of how such
concepts should interact so that we can validate the assessment of threats, the choice of
adopted risk management, etc.. To this end, we propose a declarative language Peal+ in
which the interaction of such concepts can be rigorously described and analyzed. Peal+ has
been implemented in PEALT using the SMT solver Z3 as analysis back-end. PEALT's code
generators target complex back-ends and evolve with optimizations or new back-ends. Thus
we can neither trust the tool chain nor feasibly prove correctness of all involved artefacts.
We eliminate the need to trust that tool chain by independently certifying scenarios found
by back-ends in a manner agnostic of code generation and choice of back-end. This scenario
validation is compositional, courtesy of Kleene's 3-valued logic and potential re nement of
scenarios. We prove the correctness of this validation, discuss how PEALT presents scenarios
to further users' understanding, and demonstrate the utility of this approach by showing how
it can express attack-countermeasure trees so that the interaction of attack success probability,
attack cost, and attack impact can be analyzed.