本書針對目前安全協(xié)議中存在的不具有實用性或過于復(fù)雜等問題，以UC安全屬性作為主要對象，研究ZK協(xié)議及對它的形式化甚至自動化進(jìn)行分析驗證，主要工作有：研究UC模型的可描述性及UC模型中協(xié)議模塊化設(shè)計與分析方法，利用UC模型分析密碼協(xié)議的安全性，主要是利用協(xié)議仿真嚴(yán)格證明協(xié)議是否能安全實現(xiàn)特定安全任務(wù)；研究通用可組合零知識證明協(xié)議，可規(guī)約到通用可組合不經(jīng)意傳輸(UCOT)協(xié)議的實現(xiàn)；研究基于零知識證明的通用可組合形式化分析模型的擴(kuò)展和形式化分析。