Loading...
Please wait, while we are loading the content...
Similar Documents
A Formal Approach for Automatic Verification of Imperfect Cryptographic Protocols
| Content Provider | Semantic Scholar |
|---|---|
| Author | Hoang, Long Nguyen |
| Copyright Year | 2007 |
| Abstract | In simplest form, security protocols comprise messages exchanged between agents to achieve security goals such as confidentiality and integrity of data, or authentication of the identity. Despite that simple fact, designing security protocols has been considered critical task since the protocols should work in the presence of powerful adversary over the network. Analyzing security protocols is non-trivial as it exploits undiscovered security holes. Technically, one security protocol can be modeled and analyzed in two perspectives: the formal model and the computational model. The former approach assumes perfect cryptography: having an encrypted message {M}K , there is no way to recover original message M without knowing secret key K ; also it is infeasible to retrieve knowledge of K from {M}K . Over the years, based on this assumption, such effective methods and automated tools have been developed and studied to help us to analyze the design of protocols. However, while assumption of perfect cryptography strengthens the process of security protocol analyzing in logically and mathematically, it also restricts us to a limited, fixed security model. There are situations that applications of one security protocol are not perfectly secure as they are proved because of the gap between the representation of encryption in formal and its concrete implementation. Computational model, on the other hand, defines security properties in terms of the probability and computational complexity of successful attacks. Hence perfect encryption assumption and adversary power have been relaxed, respectively. In computational view, good security protocols are those in which adversaries cannot cause harm too often and efficiently enough. Each approach above has its own advantages and drawbacks. These models, unfortunately, are quite distinct as they are developed by two separated communities. Such efforts have been proposed to take benefit from both models |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.ut.ee/~Jan/kryptoseminar/seminar07/seminar-paper-LongNguyen.pdf |
| Alternate Webpage(s) | https://courses.cs.ut.ee/2007/crypto-seminar-fall/papers/seminar-paper-LongNguyen.pdf |
| Alternate Webpage(s) | https://courses.cs.ut.ee/2007/crypto-seminar-fall/papers/long_final.pdf |
| Alternate Webpage(s) | http://www.cs.ut.ee/~jan/kryptoseminar/long_final.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
