Vai ai contenuti. | Spostati sulla navigazione | Spostati sulla ricerca | Vai al menu | Contatti | Accessibilità

logo del sistema bibliotecario dell'ateneo di padova

Ceccato, Alessia (2003) Analisi statica dello Spi-calcolo. [Laurea vecchio ordinamento]

Full text disponibile come:

[img]
Preview
PDF
372Kb

Abstract

In questo lavoro ci proponiamo quindi di analizzare i protocolli di comunicazione, utilizzando lo Spi-calcolo come modello per poterli rappresentare. Lo Spi-calcolo estende un particolare modello per la connessione dei sistemi interattivi (il Ï€-calcolo) al quale vengono aggiunte le operazioni comuni nei protocolli di sicurezza. Vi sono molti dialetti dello Spi-calcolo, noi considereremo quello proposto in [3] che utilizza una semantica di tipo “late” [26]

Item Type:Laurea vecchio ordinamento
Corsi di Laurea vecchio ordinamento:Facoltà di Scienze MM. FF. NN. > DU Informatica
Additional Information:Corso di Laurea in Matematica
Subjects:Area 01 - Scienze matematiche e informatiche > INF/01 Informatica
Codice ID:275
Relatore:Filè, Gilberto
Data della tesi:2003
Biblioteca:Polo di Scienze > Biblioteca del Seminario Matematico
Tipo di fruizione per il documento:on-line per i full-text
Tesi sperimentale (Si) o compilativa (No)?:No

Bibliografia

I riferimenti della bibliografia possono essere cercati con Cerca la citazione di AIRE, copiando il titolo dell'articolo (o del libro) e la rivista (se presente) nei campi appositi di "Cerca la Citazione di AIRE".
Le url contenute in alcuni riferimenti sono raggiungibili cliccando sul link alla fine della citazione (Vai!) e tramite Google (Ricerca con Google). Il risultato dipende dalla formattazione della citazione e non da noi.

[1] Mart’´Ä±n Abadi. Secrecy by typing in security protocols. In Proceedings of Theoretical Aspects of Computer Software, Third International Symposium LNCS 1281, 1997. Cerca con Google

[2] Mart’´Ä±n Abadi. Security protocols and their properties. In F. Bauer e R. Steinbrueggen, editor, Cerca con Google

Foundations of Secure Computation, NATO Science Series, pagine 36-60, IOS Press, 2000. Cerca con Google

[3] Mart’´Ä±n Abadi e Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pagine 33-34, ACM Press, 2002. Cerca con Google

[4] Mart’´Ä±n Abadi e Bruno Blanchet. Secrecy types for asymmetric communication. In F. Honsell e M. Miculan, editor, Foundations of Software Science and Computation Structures (FoSSaCS 2001), volume 2030 of Lecture Notes in Computer Science, pagine 25-41, Springer-Verlag, 2001. Cerca con Google

[5] Mart’´Ä±n Abadi e C. Fournet. Mobile values, new names, and secure communication. In Proceedings of the 28th Annual ACM Symposium on Principles of Programming Languages (POPL’01), pagine 104-115, 2001. Cerca con Google

[6] Mart’´Ä±n Abadi e Andrew Gordon. A calculus for cryptographic protocols: the spi-calculus. Information and Computation, 148(4):1-70, 1999. Cerca con Google

[7] Bruno Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pagine 82-96, 2001. Cerca con Google

[8] Chiara Bodei, Pierpaolo Degano, Flemming Nielson e Hanne Riis Nielson. Static analysis for the π-caclulus with application to security. Information and Computation,165:68-92, 2001. Cerca con Google

[9] Gerard Boudol e Ilaria Castellani. Noninterference for concurrent programs and thread systems. Theoretical Computer Science, 281(1):109-130, 2002. Cerca con Google

[10] L. Cardelli, G. Ghelli e A. Gordon. Secrecy and group creation. In C. Palamidessi, editor, CONCUR 2000: Concur-Springer-Verlag, 2000 . Cerca con Google

[11] L. Cardelli e A. Gordon. Mobile ambients: foundations of system specification and computation structures. Lecture Notes in Computer Science Vol 1378, pagine 140-155, Springer-Verlag, 1998. Cerca con Google

[12] I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell e A. Scedrov. A meta-notation for protocol analysis. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW’99), pagine 55-69, 1999. Cerca con Google

[13] Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of 4th ACM POPL, pagine 238-252, 1977. Cerca con Google

[14] M. Debabbi, M. Mejri, N. Tawbi e I. Yahmadi. A new algorithm for the automatic verification of authentication protocols: From specifications to flaws and attack scenarios. In Proceedings of the DIMACS Workshop on Design and Formal Verification of Security protocols, Rutgers University, New Jersey, 1997. Cerca con Google

[15] G. Denker, J. Meseguer e C. Talcott. Protocol specification and anlysis in Maude. In N. Haintze e J. Wing, editor, Proceedings of Workshop on Formal Methods and Security Protocols, 1998. Cerca con Google

[16] Gilberto Fil’´e e Alberto Griggio. A simple control flow anlysis of the Ï€-calculus. Manoscritto, 2003. Cerca con Google

[17] Gilberto Fil’´e e Alberto Griggio. How to account for the context while checking secrecy of Ï€-calculus processes. Manoscritto, 2003. Cerca con Google

[18] Riccardo Focardi, Roberto Gorrieri e Fabio Martinelli. Noninterference for the analysis of criptographic protocols. In UgoMontanari, editor, Proceedings of the 27th ICALP,numero 1853 in LNCS, 2000. Cerca con Google

[19] A. Gordon e A. Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pagine 145-159, 2001. Cerca con Google

[20] M. Hennesy e J. Riely. Information flow vs. resource access in the asyncronus π-calculus. In Proceedings of the 27th International Colloquium on Automata, Language e Programming, Lecture Cerca con Google

Notes in Computer Science, pagine 415-427, Springer-Verlag, 2000. Cerca con Google

[21] Kohei Honda, Vasco Vasconcelos e Nobuko Yoshida. Secure information flow as typed program behaviour. In Smolka E., editor, Proceedings of the 9th ESOP,numero 1782 in LNCS, Springer-Verlag, 2000. Cerca con Google

[22] Robin Milner. Science, Springer-Verlag, 1980. Cerca con Google

[23] Robin Milner. Communication and Concurrency, Prentice Hall, 1989. Cerca con Google

[24] Robin Milner. Communicating and mobile systems: the π-calculus, Cambridge University Press, 1999. Cerca con Google

[25] Robin Milner, Joachim Parrow e David Walker. A calculus of mobile processes (i e ii). Information and Computation, 100(1):1-77, 1992. Cerca con Google

[26] Robin Milner, Joachim Parrow e David Walker. Modal Logics for mobile processes. Theoretical Computer Science, 114(1):149-171, 1993. Cerca con Google

[27] Flemming Nielson, Hanne Riis Nielson e Chris Hankin. Principles of Program Analysis, Springer-Verlag, 1999. Cerca con Google

[28] Davide Sangiorgi e David Walker. The π-calculus: a Theory of Mobile Processes, Cambridge University Press, 2001. Cerca con Google

[29] C. Weidenbach. Towards an automatic analysis of security protocols in first-order logic. In H. Ganzin- ger, editor, 16th International Conference on Automated Deduction (CADE-16), volume 1632 di Lecture Notes in Artificial Intelligence, pagine 314-328, Springer-Verlag, 1999. Cerca con Google

Solo per lo Staff dell Archivio: Modifica questo record

EPrints Logo
Padua@Thesis is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.