A formal specification of the MIDP 2.0 security model
This paper overviews a formal specification, using the Calculus of Inductive Constructions, of the application security model defined by the Mobile Information Device Profile 2.0 for Java 2 Micro Edition. We present an abstract model of the state of the device and security-related events that allows...
Gardado en:
| Autor Principal: | |
|---|---|
| Outros autores: | , |
| Formato: | report |
| Publicado: |
2006
|
| Subjects: | |
| Acceso en liña: | http://hdl.handle.net/20.500.12008/3538 |
| Tags: |
Sen Etiquetas, Sexa o primeiro en etiquetar este rexistro!
|
| _version_ | 1868890153667264512 |
|---|---|
| author | Zanella Béguelin, Santiago |
| author2 | Betarte, Gustavo Luna, Carlos |
| author2_role | author author |
| author_browse | Betarte, Gustavo Luna, Carlos Zanella Béguelin, Santiago |
| author_facet | Zanella Béguelin, Santiago Betarte, Gustavo Luna, Carlos |
| author_role | author |
| collection | COLIBRI |
| dc.creator.none.fl_str_mv | Zanella Béguelin, Santiago Betarte, Gustavo Luna, Carlos |
| dc.date.none.fl_str_mv | 2006 2014-12-02T16:07:44Z 2014-12-02T16:07:44Z 20141202 |
| dc.format.none.fl_str_mv | 10 p. application/pdf |
| dc.identifier.none.fl_str_mv | ZANELLA BÉGUELIN, S., BETARTE, G., LUNA, C. "A formal specification of the MIDP 2.0 security model". Reportes Técnicos 06-09. UR. FI – INCO, 2006. 0797-6410 http://hdl.handle.net/20.500.12008/3538 |
| dc.language.none.fl_str_mv | in |
| dc.publisher.none.fl_str_mv | UR. FI – INCO. |
| dc.relation.none.fl_str_mv | Reportes Técnicos 06-09 |
| dc.rights.none.fl_str_mv | info:eu-repo/semantics/openAccess Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
| dc.source.none.fl_str_mv | reponame:COLIBRI instname:Universidad de la República instacron:Universidad de la República |
| dc.subject.none.fl_str_mv | Calculus of Inductive Constructions Formal specification MIDP 2.0 Security Coq |
| dc.title.none.fl_str_mv | A formal specification of the MIDP 2.0 security model |
| dc.type.none.fl_str_mv | Reporte técnico info:eu-repo/semantics/report info:eu-repo/semantics/publishedVersion |
| description | This paper overviews a formal specification, using the Calculus of Inductive Constructions, of the application security model defined by the Mobile Information Device Profile 2.0 for Java 2 Micro Edition. We present an abstract model of the state of the device and security-related events that allows to reason about the security properties of theplatform where the model is deployed. We then state and sketch the proof of some desirable properties of this model. |
| eu_rights_str_mv | openAccess |
| format | report |
| id | anni_a36a320a38f7bcf789c91be593eef76e |
| identifier_str_mv | ZANELLA BÉGUELIN, S., BETARTE, G., LUNA, C. "A formal specification of the MIDP 2.0 security model". Reportes Técnicos 06-09. UR. FI – INCO, 2006. 0797-6410 |
| instacron_str | Universidad de la República |
| institution | Universidad de la República |
| instname_str | Universidad de la República |
| language_invalid_str_mv | in |
| network_acronym_str | anni |
| network_name_str | oai-lr-anni |
| oai_identifier_str | oai:colibri.udelar.edu.uy:20.500.12008/3538 |
| publishDate | 2006 |
| publishDateSort | 2006 |
| publisher.none.fl_str_mv | UR. FI – INCO. |
| reponame_str | COLIBRI |
| repository.mail.fl_str_mv | |
| repository.name.fl_str_mv | |
| repository_id_str | |
| rights_invalid_str_mv | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
| spelling | A formal specification of the MIDP 2.0 security modelZanella Béguelin, SantiagoBetarte, GustavoLuna, CarlosCalculus of Inductive ConstructionsFormal specificationMIDP 2.0SecurityCoqThis paper overviews a formal specification, using the Calculus of Inductive Constructions, of the application security model defined by the Mobile Information Device Profile 2.0 for Java 2 Micro Edition. We present an abstract model of the state of the device and security-related events that allows to reason about the security properties of theplatform where the model is deployed. We then state and sketch the proof of some desirable properties of this model.UR. FI – INCO.2014-12-02T16:07:44Z2014-12-02T16:07:44Z200620141202Reporte técnicoinfo:eu-repo/semantics/reportinfo:eu-repo/semantics/publishedVersion10 p.application/pdfZANELLA BÉGUELIN, S., BETARTE, G., LUNA, C. "A formal specification of the MIDP 2.0 security model". Reportes Técnicos 06-09. UR. FI – INCO, 2006.0797-6410http://hdl.handle.net/20.500.12008/3538reponame:COLIBRIinstname:Universidad de la Repúblicainstacron:Universidad de la RepúblicainReportes Técnicos 06-09Las obras depositadas en el Repositorio se rigen por la Ordenanza de los Derechos de la Propiedad Intelectual de la Universidad De La República. (Res. Nº 91 de C.D.C. de 8/III/1994 – D.O. 7/IV/1994) y por la Ordenanza del Repositorio Abierto de la Universidad de la República (Res. Nº 16 de C.D.C. de 07/10/2014)info:eu-repo/semantics/openAccessLicencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)oai:colibri.udelar.edu.uy:20.500.12008/35382026-04-14T10:16:15Z |
| spellingShingle | A formal specification of the MIDP 2.0 security model Zanella Béguelin, Santiago Calculus of Inductive Constructions Formal specification MIDP 2.0 Security Coq |
| status_str | publishedVersion |
| title | A formal specification of the MIDP 2.0 security model |
| title_full | A formal specification of the MIDP 2.0 security model |
| title_fullStr | A formal specification of the MIDP 2.0 security model |
| title_full_unstemmed | A formal specification of the MIDP 2.0 security model |
| title_short | A formal specification of the MIDP 2.0 security model |
| title_sort | A formal specification of the MIDP 2.0 security model |
| topic | Calculus of Inductive Constructions Formal specification MIDP 2.0 Security Coq |
| url | http://hdl.handle.net/20.500.12008/3538 |