The current paradigm for trusted computer syst, ems holds that trust is a property of a system. It is a. property that ca. n be formally modeled, specified, and verified. It can be “designed int, o” a. system using a rigorous design methodology. For high levels of a. ssurante, the design methodology uses forma. 1 models sod methods in order to “prove” tha. t trust is present. This paradigm underlies The Department of Defense Trusted Computer System E~ valuation Criteria (TCSEC)[3], commonly ca. lled the “Orange Book,” and its companion “rainbow series” rep0rt. s. In this paper, we will refer to these documents as the “Crit. eria.” The Criteria specifies a. met. hoclology for modeling, designing, and implement~ iug a. syst, em tl1a. t builds trust into a system, and a process for proving to an evaluator that the methodology has been followed. For a description of the Criteria, and the eva. lua, tiou process, see Chokhani [l].