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
Keyword(s):  
Proof Assistant ◽  
Content Centric Networking

scholarly journals Secure and DoS-Resilient Fragment Authentication in CCN-Based Vehicular Networks

2018 ◽  
Vol 2018 ◽  
pp. 1-12
Author(s):  
Sangwon Hyun ◽  
Hyoungshick Kim
Keyword(s):  
Vehicular Networks ◽  
Denial Of Service ◽  
Content Delivery ◽  
Dos Attacks ◽  
Promising Alternative ◽  
Content Centric Networking ◽  
Transmission Unit ◽  
Communication Environments ◽  
Maximum Transmission

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.

scholarly journals CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

2011 ◽  
Vol 21 (4) ◽  
pp. 827-859 ◽  
Author(s):  
FRÉDÉRIC BLANQUI ◽  
ADAM KOPROWSKI
Keyword(s):  
Term Rewriting ◽  
Automated Verification ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Active Subject ◽  
Turing Complete

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/.

CRoWN: Content-Centric Networking in Vehicular Ad Hoc Networks

2012 ◽  
Vol 16 (9) ◽  
pp. 1380-1383 ◽  
Author(s):  
Marica Amadeo ◽  
Claudia Campolo ◽  
Antonella Molinaro
Keyword(s):  
Ad Hoc Networks ◽  
Vehicular Ad Hoc Networks ◽  
Ad Hoc ◽  
Content Centric Networking ◽  
Hoc Networks

Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

2021 ◽  
pp. 1-20
Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro
Keyword(s):  
Type Theory ◽  
Lambda Calculus ◽  
Proof Assistant ◽  
First Order ◽  
Constructive Type Theory ◽  
Fundamental Part ◽  
Constructive Type ◽  
Free Variables ◽  
The Church ◽  
Theoretical Results

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