可信信道協(xié)議的設計與形式化驗證.pdf

1、北京交通大學碩士學位論文可信信道協(xié)議的設計與形式化驗證姓名：左向暉申請學位級別：碩士專業(yè)：信息安全指導教師：何永忠201106ABSTRACTABSTRACTCurrentlythesecurityofmostnetworksreliesonsecurechanneltechnologies，suchasSSHandIPSec，toprotectconfidentialinformationontheInternetHowever，il

2、lstheattackingtechnologyofmaliciousUSerSbecomesmoresophisticated，themodernPCsystemsaremorevulnerabletomaliciouscodeattacks，illegallyinformationstealingandothersecuritythreats，whichmaketheattackthroughdamagingtheterminals

3、TrustedcomputingCanenhancethesecuritylevelofthesecurechanneltechnologiesbyimprovingthesecurityofterminalsTrustedcomputingusestheTrustedPlatformModule(TPM)astherootsoftrustforstorageandmeasurement，aimingtoapplyhardwareenf

4、orcementmechanismstoprovidealladequatefoundationforbuildingatligh—assurancetrustedplatformWeprovideaschemeoftrustedchannelprotoc01TheschemecombinesremoteattestationofTrustedComputingwiththeprocedureofestablishingasecurec

5、onnection，nleproposedmethodnotonlydealswiththeproblemofcommunicatingwithunknownendpointsecurityinsecurechannelprotocol，butalsoensBrestheconfidentialityofinformationontheIntemetWefirststudythefundamentalsofTrustedComputin

6、gespeciallytheIntegrityMeasurementmechanismwhichisthecoreandbasisofTrustedComputingWiththecomparisonsofsecurityprotocol，wechoosetheSSHprotocolasthesecurechannelprotoc01WealsoanalyzeOpenSSHhandshakeconnection，anddesignthe

7、procedureofestablishingatrustedsecureconnectionandexchangingasessionkeyInordertoverifythesecurityfeatureoftheproposedscheme，wealsostudyformalmethodsofverifyingsecurityprotocols，Throughtheeounterexamplefromthesymbolicmode

8、lcheckingtool，NuSMVwhichverifiesthetwoabstractionofourscheme，weimprovethekeyexchangingprotoc01IntheendweproposeaTrustedSSHprotocolframeworkwhichholdsthetransparencyofremoteattestationinkeyexchangingalgorithmandtheconfide