当前网络应用环境需要通信双方信任彼此实施的安全策略。为了达到这个目标需要解决两个密切联系的问题:一是通信双方采用何种安全策略及如何配置选定的安全策略,二是通信双方如何证明彼此正确实施了安全策略。域型强制实行(domain and typeenforcement, DTE)强制访问控制模型的主体关联域属性,客体关联型属性,根据域和型来仲裁主体对客体或其他主体的访问请求,能够实现网络访问控制所需要细粒度和高的可用性,构成了本文安全策略的基础。可信计算组(trusted computing group, TCG)系列标准之一的可信计算平台模块(trusted platform module,TPM)可以提供系统的不可篡改的度量,构成了本文平台证明的基础用来证明安全策略在主机上的正确实施。本文在深入分析网络访问控制应用场景的基础上,提出了基于DTE和平台证明的网络强制访问控制形式模型。该模型主要使用两个技术:DTE技术(包括构建在DTE之上的基于角色的访问控制子模型)和基于TPM的平台证明技术。利用前者实现网络主机间的访问控制,利用后者实现网络主机的可信引导和主机间的策略实施验证。本形式模型设置了安全相关的不变量,描述了系统的迁移规则,证明了相应的安全定理。本文最后论述和分析了模型在实际应用场景下的实施方案。