An Improved Method for Formal Security Verification of Cryptographic Protocols
スポンサーリンク
概要
- 論文の詳細を見る
We have devised a polynomial time algorithm to decide the security of cryptographic protocols formally under certain conditions, and implemented the algorithm on a computer as a supporting system for deciding the security. In this paper, a useful approach is presented to decide security problems which do not satisfy some of the above-mentioned conditions by using the system. For its application, we consider a basic security problem of Kerberos protocol, whether or not an enemy can obtain the session key between a client and a server by using any information not protected in communication channels and using any operation not prohibited in the system. It is shown that Kerberos is secure for this problem.
- 社団法人電子情報通信学会の論文
- 1996-07-25
著者
-
Watanabe Hajime
岡山大学 理学部
-
Fujiwara T
Osaka University
-
Fujiwara Toru
Department Of Multimedia Engineering Graduate School Of Information Science And Technology Osaka Uni
-
KASAMI Tadao
Graduate School of Information Science, Nara Institute of Science and Technology
-
Fujiwara Toru
Faculty of Engineering Science, Osaka University
-
Kasami Tadao
Graduate School Of Information Science Nara Institute Of Science And Technology
-
Koumoto Takuya
Okayama University
-
Fujiwara Toru
Faculty Of Engineering Science Osaka University
-
WATANABE Hajime
Graduate School of Information Science, Nara Institute of Science and Technology
-
Fujiwara T
Department Of Multimedia Engineering Graduate School Of Information Science And Technology Osaka Uni
-
Watanabe H
Department Of Bioenvironmental Research Center For Integrative Bioscience Okazaki National Research
-
Koumoto T
Hiroshima City Univ. Hiroshima Jpn
-
Watanabe Hajime
Graduate School Of Agricultural Science Tohoku University:(present Office)faculty Of Agriculture Nii
関連論文
- Formation of Tissue Masses on Floral Inflorescence in A. thaliana Plants That Accumulate Reduced Levels of MT2a mRNA
- Formation of Tissue Masses on Floral Inflorescence in A. thaliana Plants That Accumulate Reduced Levels of MT2a mRNA (Plant Nutrition)
- Composition of Seed Storage Proteins Changed by Glutathione Treatment of Soybeans(Biochemistry & Molecular Biology)
- Independent roles of glutathione and O-acetyl-L-serine in regulation of sulfur-responsive gene expression in Arabidopsis thaliana
- Quantitative estimation of the contribution of the phloem in cadmium transport to grains in rice plants (Oryza sativa L.)(Plant Nutrition)
- Arabidopsis SNRK2.3 protein kinase is involved in the regulation of sulfur-responsive gene expression and O-acetyl-L-serine accumulation under limited sulfur supply(Plant Nutrition)
- Differential Distribution of Proteins Expressed in Companion Cells in the Sieve Element-Companion Cell Complex of Rice Plants
- Detection of nifH Sequences in Sugarcane (Saccharum officinarum L.) and Pineapple (Ananas comosus [L.] Merr.) (Soil Biology)
- Isolation and Characterization of a Novel Arabidopsis thaliana Mutant That Requires a High Concentration of Boron
- Expression of a Single-Chain Antibody against GA_ in Vascular Tissues Induces Dwarf Phenotype for Rice Plants(Plant Nutrition)
- Identification of Several Rice Genes Regulated by Si Nutrition(Plant Nutrition)
- Cloning of the Phloem-Specific Small Heat-Shock Protein from Leaves of Rice Plants(Plant Nutrition)
- Upregulation of the Genes for Ferritin, RNase, and DnaJ in Leaves of Rice Plants in Response to Sulfur Deficiency(Plant Nutrition)
- Cadmium Concentrations in the Phloem Sap of Rice Plants (Oryza saliva L.) Treated with a Nutrient Solution Containing Cadmium (Environment)
- Regulation of Sulfur-Responsive Gene Expression by Exogenously Applied Cytokinins in Arabidopsis thaliana
- Unlinkable Delivery System for Interactive Dramas(Application)(Cryptography and Information Security)
- MAP and LogMAP Decoding Algorithms for Linear Block Codes Using a Code Structure(Special Section on Information Theory and Its Applications)
- A Recursive Maximum Likelihood Decoding Algorithm for Some Transitive Invariant Binary Block Codes
- A Sufficient Condition for Ruling Out Some Useless Test Error Patterns in Iterative Decoding Algorithms
- Low Weight Subtrellises for Binary Linear Block Codes and Their Applications
- Error Performance of Multilevel Block Coded 8-PSK Modulations Using Unequal Error Protection Codes for the Rayleigh Fading Channel
- An Improved Union Bound on Block Error Probability for Closest Coset Decoding
- On Branch Labels of Parallel Components of the L-Section Minimal Trellis Diagrams for Binary Linear Block Codes
- On Structural Complexity of the L-Section Minimal Trellis Diagrams for Binary Linear Block Codes (Special Section on Information Theory and Its Applications)
- Structural Analysis of Minimum Weight Codewords of the Extended (32, 21, 6) and (64, 45, 8) BCH Codes Using Invariance Property(HISC2006)
- The structure of the set of minimum weight codewords of the extended (32,21,6) and (64,45,8) BCH codes
- Sufficient Conditions for Ruling-Out Useless Iterative Steps in a Class of Iterative Decoding Algorithms (Special Section on Information Theory and Its Applications)
- The Weight Distributions of Cosets of the Second-Order Reed-Muller Code of Length 128 in the Third-Order Reed-Muller Code of Length 128
- A Method for Computing the Weight Distribution of a Block Code by Using Its Trellis Diagram (Special Section on Information Theory and Its Applications)
- EFFECT OF STEROID HORMONES, GROWTH FACTORS AND CYTOKINES ON THE EXPRESSION OF MATRIX METALLOPROTEINASE mRNAS IN THE MOUSE UTERUS
- An Improved Method for Formal Security Verification of Cryptographic Protocols
- A System for Deciding the Security of Cryptographic Protocols (Special Section on Cryptography and Information Security)
- A Private and Consistent Data Retrieval Scheme with Log-Squared Communication(Application,Cryptography and Information Security)
- Performance Analysis for Binary Image of Linear Block Codes over an Extended Field of GF(2)
- Adaptive Recursive Maximum Likelihood Decoding Based on the Coarsest Parallel Concatenation Decomposition : Evaluation of the Decoding Complexity by Simulation
- Soft-Input Soft-Output Decoding Algorithm Based on Iterative Minimum Distance Search for Reed-Muller Codes
- Selecting the Search Centers of h-Chase Decoding Algorithms by Simulation
- The Optimal Sectionalized Trellises for the Generalized Version of Viterbi Algorithm of Linear Block Codes and Its Application to Reed-Muller Codes
- Average Complexity Evaluation of an MLD Algorithm Using the Trellis Structure for a Linear Block Code
- Isolation of Arabidopsis thaliana cDNAs That Confer Yeast Boric Acid Tolerance
- Cloning of cDNAs Encoding Isopropylmalate Dehydrogenase from Arabidopsis thaliana and Accumulation Patterns of Their Transcripts
- Cloning of a Cytochrome P450 Gene Induced by Ethylene Treatment in Deepwater Rice (Oryza sativa L.)(Crop Physiology & Ecology)
- An Anonymous Bidding Protocol without Any Reliable Center (特集 情報セキュリティの理論と応用)
- A Linkable Group Signature and Its Application to Secret Voting
- Assignment of Data Types to Words in a Natural Language Specification
- Implementation of Natural Language Specifications of Communication Protocols by Executable Specifications
- A Translation Method from Natural Language Specifications of Communication Protocols into Algebraic Specifications Using Contextual Dependencies
- RNA Pseudoknotted Structure Prediction Using Stochastic Multiple Context-Free Grammar
- On the Generative Power of Grammars for RNA Secondary Structure(Foundations of Computer Science)
- EFFECTS OF BISPHENOL-A AND NONYLPHENOL ON DEVELOPING XENOPUS LAEVIS
- Highly Boron Deficiency-Tolerant Plants Generated by Enhanced Expression of NIP5;1, a Boric Acid Channel
- A Soft-Decision Iterative Decoding Algorithm Using a Top-Down and Recursive Minimum Distance Search(Special Section on Information Theory and Its Applications)
- An Evaluation Method of the Block Error Probability by Using a Low-Weight Sub-Trellis Diagram
- Syntactic Unification Problems under Constrained Substitutions
- A Polynomial Time Learning Algorithm for Recognizable Series
- A Watermarking System with Two Servers which can Detect Server's Corruption
- A Polynomial-Time Recognizable Subclass of Lexical-Functional Grammars
- A Note on Inadequacy of the Model for Learning from Queries
- Finite State Translation Systems and Parallel Multiple Context-Free Grammars
- The Universal Recognition Problems for Multiple Context-Free Grammars and for Linear Context-Free Rewriting Systems
- Selection of Test Patterns in an Iterative Erasure and Error Decoding Algorithm for Non-binary Block Codes(Coding Theory)
- Selection Method of Test Patterns in Soft-Decision Iterative Bounded Distance Decoding Algorithms(Coding Theory)(Information Theory and Its Applications)
- Selection of Search Centers in Iterative Soft-Decision Decoding Algorithms(Special Section on Information Theory and Its Applications)
- An Improvement to GMD-Like Decoding Algorithms(Special Section on Information Theory and Its Applications)
- Reduced Complexity Iterative Decoding Using a Sub-Optimum Minimum Distance Search(Cording Theory)(Information Theory and Its Applications)
- Quadrupole Effects of Vacancy Orbital in Boron-Doped Silicon
- RNA Pseudoknotted Structure Prediction Using Stochastic Multiple Context-Free Grammar