Computer Science ›› 2016, Vol. 43 ›› Issue (Z11): 329-337.doi: 10.11896/j.issn.1002-137X.2016.11A.077
Previous Articles Next Articles
MA Yuan-yuan, CHEN Zhe, WANG Chen, FEI Jia-xuan and HUANG Xiu-li
| [1] 范红.协议的安全性分析形式化分析理论与方法[D].郑州:中国人民解放军信息工程大学,2003 [2] Abadi M,Needham R.Prudent engineering practice for cryptographic protocols[J].IEEE transactions on Software Enginee-ring,1996,22(1):6-15 [3] Gritzalis S,Spinellis D.Cryptographic protocols over open distributed systems:A taxonomy of flaws and related protocol analysis tools[M]∥Safe Comp 97.Springer London,1997:123-137 [4] Syverson P.A taxonomy of replay attacks [cryptographic protocols][C]∥Proceedings of Computer Security Foundations Workshop VII,1994.IEEE,1994:187-191 [5] 雷新锋,宋书民,刘伟兵,等.计算可靠的密码协议形式化分析综述[J].计算机学报,2014(5):993-1016 [6] Needham R M,Schroeder M D.Using encryption for authentication in large networks of computers[J].Communications of the ACM,1978,21(12):993-999 [7] Dolev D,Yao A C.On the security of public key protocols[J].IEEE Transactions on Information Theory,1983,29(2):198-208 [8] Burrows M,Abadi M,Needham R M.A logic of authentication[C]∥Proceedings of the Twelfth ACM Symposium on Operating System Principles.1989:1-13 [9] Grdel E.Why are modal logics so robustly decidable?[C]∥Bulletin EATCS.1999:90-103 [10] Gong L,Needham R,Yahalom R.Reasoning about belief incryptographic protocols[C]∥1990 IEEE Computer Society Symposium on Research in Security and Privacy,1990.1990:234-248 [11] Abadi M,Tuttle M R.A semantics for a logic of authentication[C]∥Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing.ACM,1991:201-216 [12] Syverson P F,Van Oorschot P C.A unified cryptographic protocol logic[R].Naval Research Lab Washington DC,1996 [13] Kailar R.Reasoning about accountability in protocols for electronic commerce[C]∥Proceedings of Security and Privacy.IEEE,1995:236-250 [14] Coffey T,Saidha P.Logic for verifying public-key cryptographic protocols[J].IEE Proceedings－Computers and Digital Techniques,IET,1997,144(1):28-32 [15] Kailar R,Gligor V D.On belief evolution in authentication protocols[C]∥Proceedings of Computer Security Foundations Workshop IV,1991.IEEE,1991:103-116 [16] Rubin A D,Honeyman P.Nonmonotonic cryptographic protocols[C]∥ Proceedings of Computer Security Foundations Workshop VII,1994.IEEE,1994:100-116 [17] Lowe G.Breaking and fixing the Needham-Schroeder public-key protocol using FDR[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,1996:147-166 [18] Roscoe A W.Proving security protocols with model checkers by data independence techniques[C]∥11th IEEE Computer Security Foundations Workshop,1998.IEEE,1998:84-95 [19] Mitchell J C,Mitchell M,Stern U.Automated analysis of cryptographic protocols using Murφ[C]∥1997 IEEE Symposium on Security and Privacy,1997.IEEE,1997:141-151 [20] Denker G,Meseguer J,Talcott C.Protocol specification and analysis in Maude[C]∥Proc.of Workshop on Formal Methods and Security Protocols.1998:25 [21] Armando A,Compagna L,Ganty P.SAT-based model-checking of security protocols using planning graph analysis[M]∥FME 2003:Formal Methods.Springer Berlin Heidelberg,2003:875-893 [22] Chevalier Y,Vigneron L.A tool for lazy verification of security protocols[C]∥ 16th Annual International Conference on Automated Software Engineering(ASE 2001),2011.IEEE,2001:373-376 [23] Basin D,Mdersheim S,Vigano L.An on-the-fly model-checker for security protocol analysis[M].Springer Berlin Heidelberg,2003 [24] Blanchet B,Abadi M,Fournet C.Automated verification of selected equivalences for security protocols[C]∥20th Annual IEEE Symposium on Logic in Computer Science,2005.IEEE,2005:331-340 [25] Paulson L C.The inductive approach to verifying cryptographic protocols[J].Journal of Computer Security,1998,6(1/2):85-128 [26] Guttman J D,Herzog J C,Fábrega F T.Strand spaces:proving security protocols correct[J].Journal of Computer Security,1999,7(2/3):191-230 [27] Song D X,Berezin S,Perrig A.Athena:a novel approach to efficient automatic security protocol analysis[J].Journal of Computer Security,2001,9(1/2):47-74 [28] Armando A,Basin D,Boichut Y,et al.The AVISPA tool for the automated validation of internet security protocols and applications[C]∥Computer Aided Verification.Springer Berlin Heidelberg.2005:281-285 [29] Meadows C.The NRL protocol analyzer:An overview[J].The Journal of Logic Programming,1996,26(2):113-131 [30] Gibson-Robinson T,Armstrong P,Boulgakov A,et al.FDR3—A modern refinement checker for CSP[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2014:187-201 [31] Lowe G.Casper:A compiler for the analysis of security protocols[C]∥Proceedings of Computer Security Foundations Workshop,1997.IEEE,1997:18-30 [32] Stoller S D.A bound on attacks on payment protocols[C]∥16th Annual IEEE Symposium on Logic in Computer Science,2001.IEEE,2001:61-70 [33] Schneider S.Using CSP for protocol analysis:the Needham-Schroeder public-key protocol[M].University of London,Royal Holloway,Department of Computer Science,1996 [34] Boichut Y,Genet T,Jensen T,et al.Rewriting approximations for fast prototyping of static analyzers[M]∥Term Rewriting and Applications.Springer Berlin Heidelberg,2007:48-62 [35] Clarke E M,Grumberg O,Peled D.Model checking[M].MIT Press,1999 [36] Paulson L C.Isabelle:A generic theorem prover[M].Springer Science & Business Media,1994 [37] Sangiorgi D,Walker D.The pi-calculus:a Theory of MobileProcesses[M].Cambridge University Press,2003 [38] Abadi M,Gordon A D.A calculus for cryptographic protocols:The spi calculus[C]∥Proceedings of the 4th ACM Conference on Computer and Communications Security.ACM,1997:36-47 [39] Bolignano D.An approach to the formal verification of cryptographic protocols[C]∥Proceedings of the 3rd ACM Conference on Computer and Communications Security.ACM,1996:106-118 [40] Goldwasser S,Micali S.Probabilistic encryption[J].Journal of Computer and System Sciences,1984,28(2):270-299 [41] Bellare M,Rogaway P.Random oracles are practical:A paradigm for designing efficient protocols[C]∥Proceedings of the 1st ACM Conference on Computer and Communications Security.ACM,1993:62-73 [42] Bellare M,Rogaway P.Entity authentication and key distribution[M]∥Advances in Cryptology—CRYPTO’93.Springer Berlin Heidelberg,1994:232-249 [43] Bellare M,Rogaway P.Provably secure session key distribution:the three party case[C]∥Proceedings of the twenty-seventh Annual ACM Symposium on Theory of Computing.ACM,1995:57-66 [44] Bellare M,Pointcheval D,Rogaway P.Authenticated key ex-change secure against dictionary attacks[M]∥Advances in Cryptology—Eurocrypt 2000.Springer Berlin Heidelberg,2000:139-155 [45] Bresson E,Chevassut O,Pointcheval D.Provably authenticated group Diffie-Hellman key exchange—the dynamic case[M]∥Advances in Cryptology—ASIACRYPT 2001.Springer Berlin Heidelberg,2001:290-309 [46] Abdalla M,Fouque P A,Pointcheval D.Password-based authenticated key exchange in the three-party setting[M]∥Public Key Cryptography-PKC 2005.Springer Berlin Heidelberg,2005:65-84 [47] Bellare M,Canetti R,Krawczyk H.A modular approach to the design and analysis of authentication and key exchange protocols[C]∥Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing.ACM,1998:419-428 [48] Canetti R,Krawczyk H.Analysis of key-exchange protocols and their use for building secure channels[M]∥Advances in Cryptology—EUROCRYPT 2001.Springer Berlin Heidelberg,2001:453-474 [49] Canetti R.Universally composable security:A new paradigm for cryptographic protocols[C]∥42nd IEEE Symposium on Foundations of Computer Science,2001.IEEE,2001:136-145 [50] Abadi M,Rogaway P.Reconciling two views of cryptography[C]∥Proceedings of the IFIP International Conference on Theoretical Computer Science.2000:3-22 [51] Micciancio D,Warinschi B.Completeness Theorems for theAbadi-Rogaway Language of Encrypted Expressions[J].Journal of Computer Security,2004,12(1):99-129 [52] Horvitz O,Gligor V.Weak key authenticity and the computational completeness of formal encryption[M]∥Advances in Cryptology－CRYPTO 2003.Springer Berlin Heidelberg,2003:530-547 [53] Bana G.Soundness and Completenss of Formal Logics of Symmetric[D].University of Pennsylvania,2005 [54] Adao P,Bana G,Scedrov A.Computational and information-theoretic soundness and completeness of formal encryption[C]∥18th IEEE Workshop Computer Security Foundations,2005.IEEE,2005:170-184 [55] Herzog J.Computational soundness for standard assumptions of formal cryptography[D].Massachusetts Institute of Technology,2004 [56] Herzog J.A computational interpretation of Dolev-Yao adver-saries[J].Theoretical Computer Science,2005,340(1):57-81 [57] Abadi M,Jürjens J.Formal eavesdropping and its computational interpretation[M]∥Theoretical Aspects of Computer Software.Springer Berlin Heidelberg,2001:82-94 [58] Micciancio D,Panjwani S.Adaptive security of symbolic encryption[M]∥Theory of Cryptography.Springer Berlin Heidelberg,2005:169-187 [59] Micciancio D,Warinschi B.Soundness of formal encryption inthe presence of active adversaries[M]∥Theory of Cryptography.Springer Berlin Heidelberg,2004:133-151 [60] Cortier V,Warinschi B.Computationally sound,automatedproofs for security protocols[M]∥Programming Languages and Systems.Springer Berlin Heidelberg,2005:157-171 [61] Canetti R,Herzog J.Universally composable symbolic securityanalysis[J].Journal of Cryptology,2011,24(1):83-147 [62] Cortier V,Kremer S,Küsters R,et al.Computationally sound symbolic secrecy in the presence of hash functions[M]∥FSTTCS 2006:Foundations of Software Technology and Theoretical Computer Science.Springer Berlin Heidelberg,2006:176-187 [63] Janvier R,Lakhnech Y,Mazaré L.Computational soundness of symbolic analysis for protocols using hash functions[J].Electronic Notes in Theoretical Computer Science,2007,186:121-139 [64] Backes M,Pfitzmann B,Waidner M.A general composition theo-rem for secure reactive systems[M]∥Theory of Cryptography.Springer Berlin Heidelberg,2004:336-354 [65] Datta A,Derek A,Mitchell J C,et al.Probabilistic polynomial-time semantics for a protocol security logic[M]∥Automata,Languages and Programming.Springer Berlin Heidelberg,2005:16-29 [66] Datta A,Derek A,Mitchell J C,et al.A derivation system for security protocols and its logical formalization[C]∥16th IEEE Computer Security Foundations Workshop,2003.IEEE,2003:109-125 [67] Abadi M,Gordon A D.A calculus for cryptographic protocols:The spi calculus[C]∥Proceedings of the 4th ACM Conference on Computer and Communications Security.ACM,1997:36-47 [68] Milner R,Parrow J,Walker D.A Calculus of Mobile Processes,I[J].Information and Computation,1992,100(1):1-40 [69] Abadi M,Fournet C.Mobile values,new names,and secure communication[J].ACM SIGPLAN Notices,2001,36(3):104-115 [70] Baudet M,Cortier V,Kremer S.Computationally sound implementations of equational theories against passive adversaries[M]∥Automata,Languages and Programming.Springer Berlin Heidelberg,2005:652-663 [71] Adao P,Fournet C.Cryptographically sound implementationsfor communicating processes[M]∥Automata,Languages and Programming.Springer Berlin Heidelberg,2006:83-94 [72] Comon-Lundh H,Cortier V.Computational soundness of observational equivalence[C]∥Proceedings of the 15th ACM Confe-rence on Computer and Communications Security.ACM,2008:109-118 [73] Guttman J D,Thayer F J,Zuck L D.The faithfulness of abstract protocol analysis:Message authentication[C]∥Proceedings of the 8th ACM Conference on Computer and Communications Security.ACM,2001:186-195 [74] Laud P.Encryption cycles and two views of cryptography[C]∥Proceedings of the 7th Nordic Workshop on Secure IT Systems (NORDSEC).2002:85-100 [75] Herzog J C.The Diffie-Hellman key-agreement scheme in thestrand-space model[C]∥16th IEEE Computer Security Foundations Workshop,2003.IEEE,2003:234-247 [76] Laud P.Semantics and program analysis of computationally secure information flow[M]∥Programming Languages and Systems.Springer Berlin Heidelberg,2001:77-91 [77] Impagliazzo R,Kapron B M.Logics for reasoning about cryptographic constructions[C]∥44th Annual IEEE Symposium on Foundations of Computer Science,2003.IEEE,2003:372-383 [78] Barthe G,Daubignard M,Kapron B,et al.Computational indistinguishability logic[C]∥Proceedings of the 17th ACM Confe-rence on Computer and Communications Security.ACM,2010:375-386 [79] Lincoln P,Mitchell J,Mitchell M,et al.A probabilistic poly-time framework for protocol analysis[C]∥Proceedings of the 5th ACM Conference on Computer and Communications Security.ACM,1998:112-121 [80] Mitchell J C,Ramanathan A,Scedrov A,et al.A probabilisticpolynomial-time process calculus for the analysis of cryptographic protocols[J].Theoretical Computer Science,2006,353(1):118-164 [81] Shoup V.Sequences of games:a tool for taming complexity in security proofs[J].IACR Cryptology ePrint Archive,2004,2004:332 [82] Blanchet B.A computationally sound mechanized prover for security protocols[J].IEEE Transactions on Dependable and Secure Computing,2008,5(4):193-207 [83] IEC 61850:Communication networks and system in substations,part 1 to part 10 [S].1999 [84] http://www.iec.ch/smartgrid/standards/ [85] 曹阳,姚建国,杨胜春,等.智能电网核心标准 IEC61970 最新进展[J].电力系统自动化,2011,35(17):1-4 [86] Mcmorran A W.An Introduction to IEC 61970-301 & 61968-11:The Common Information Model[D].University of Strathclyde,2007 |
| No related articles found! |
|
||
Home