Uma Análise Formal Automatizada dos Protocolos de Envio e Confirmação de Processamento da Nota Fiscal Eletrônica Brasileira

• Jean Everson Martina University of Cambridge
• Luiz Augusto Chaves Boal DF-e Tecnologia

DOI: https://doi.org/10.5753/sbseg.2008.20895

Abstract

The Brazilian Electronic Bill of Sale(NF-e) is a taxing legislation that establishes an electronic system to replace the actual paper-based goods taxing system. It is used to declare to the government operations related with buying and selling goods between companies in real time, replacing the actual paperwork. This paper aims to formalise and analise the message exchange protocols established by the legislation. We formalise the messages of sending and confirmation sub-protocols, then we use a consolidated method to automatically analise security protocols. A conceptual problem is found. We then evaluate the impact and propose modifications in the protocols to avoid this problem.

References

de Souza, T. C. S., Martina, J. E., and Custódio, R. F. (2008). Audit and backup procedures for hardware security modules. In IDtrust ’08, New York, NY, USA. ACM.

Dolev, D. and Yao, A. (1983). On the security of public key protocols. Information Theory, IEEE Transactions on, 29(2):198–208.

Gorges, A. J. (2006). O Seu Plantão Fiscal - Dicionário de ICMS de A a Z. CENOFISCO, 8 edition.

Martina, J. E., de Souza, T. C. S., and Custódio, R. F. (2007). Openhsm: An open key life cycle protocol for public key infrastructure’s hardware security modules. In EuroPKI’07, LNCS. Springer-Verlag Berlin Heidelberg.

Needham, R. M. and Schroeder, M. D. (1978). Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993–999.

NIST, N. I. o. S. (2002). Fips pub 140-2 - security requirements for cryptographic modules.

Paulson, L. C. (1999a). Inductive analysis of the internet protocol tls. ACM Trans. Inf. Syst. Secur., 2(3):332–351.

Paulson, L. C. (1999b). Proving security protocols correct. In LICS ’99: Proceedings of the 14th Annual IEEE Symposium on Logicin Computer Science, page 370, Washington, DC, USA. IEEE Computer Society.

Presidência da República (2001). Medida provisória número 2.200-2.

Projeto NF-e (2007). Manual de integração do contribuinte - padrões técnicos de comunicação. Technical Report 2.0.2, ENCAT.

Secretaría de Hacienda y Crédito Público México (2008). Factura eletrónica - faq. http://www.sat.gob.mx/sitio_internet/e_sat/comprobantes_fiscales/15_6606.html.

Servicio de Impuestos Internos - Chile (2003). Resolucion exenta sii no.45. http://www.sii.cl/documentos/resoluciones/2003/res_ind2003.htm/.

SRF, S. d. R. F. (2007). Portal nacional da nota fiscal eletrônica. http://www.nfe.fazenda.gov.br/.

Weidenbach, C. (1999). Towards an automatic analysis of security protocols in first-order logic. In CADE-16: Proceedings of the 16th International Conference on Automated Deduction, pages 314–328, London, UK. Springer-Verlag.

Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., and Topic, D. (2002). SPASS version 2.0. In 18th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence. Springer.