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