Verification of Content-Centric Networking Using Proof Assistant

2016 ◽  
Vol E99.B (11) ◽  
pp. 2297-2304
Author(s):  
Sosuke MORIGUCHI ◽  
Takashi MORISHIMA ◽  
Mizuki GOTO ◽  
Kazuko TAKAHASHI
2018 ◽  
Vol 2018 ◽  
pp. 1-12
Author(s):  
Sangwon Hyun ◽  
Hyoungshick Kim

Content-Centric Networking (CCN) is considered as a promising alternative to traditional IP-based networking for vehicle-to-everything communication environments. In general, CCN packets must be fragmented and reassembled based on the Maximum Transmission Unit (MTU) size of the content delivery path. It is thus challenging to securely protect fragmented packets against attackers who intentionally inject malicious fragments to disrupt normal services on CCN-based vehicular networks. This paper presents a new secure content fragmentation method that is resistant to Denial-of-Service (DoS) attacks in CCN-based vehicular networks. Our approach guarantees the authenticity of each fragment through the immediate fragment verification at interim nodes on the routing path. Our experiment results demonstrate that the proposed approach provides much stronger security than the existing approach named FIGOA, without imposing a significant overhead in the process. The proposed method achieves a high immediate verification probability of 98.2% on average, which is 52% higher than that of FIGOA, while requiring only 14% more fragments than FIGOA.


2011 ◽  
Vol 21 (4) ◽  
pp. 827-859 ◽  
Author(s):  
FRÉDÉRIC BLANQUI ◽  
ADAM KOPROWSKI

Termination is an important property of programs, and is notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years, many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring the reliability of those tools is therefore an important issue.In this paper we present a library formalising important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.The sources are freely available athttp://color.inria.fr/.


2012 ◽  
Vol 16 (9) ◽  
pp. 1380-1383 ◽  
Author(s):  
Marica Amadeo ◽  
Claudia Campolo ◽  
Antonella Molinaro

Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.


Sign in / Sign up

Export Citation Format

Share Document