Formalizing Routing Models in ACL2

Abstract

We present two preliminary formalizations of router networks, both expressed in the logic of the ACL2 theorem prover. One formalization focuses on connectivity requirements by formalizing validity, visibility, and a trivial example routing policy, and demonstrates the ability to execute specifications. The other formalization focuses on network security properties, specifically information-flow and non-interference, and includes theorems demonstrating these properties for a simple formalization of a router network.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 19, 2008
Accession Number
AD1024606

Entities

People

  • Matt Kaufmann
  • Robert B. Krug
  • Sandip Ray
  • Warren Jr A. Hunt

Organizations

  • University of Texas at Austin

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Autonomous Systems
  • Bodies
  • Computations
  • Computer Network Security
  • Computer Networks
  • Computer Science
  • Network Protocols
  • Network Topology
  • Networks
  • Routing Protocols
  • Security
  • Sequences
  • Simulations
  • Specifications
  • Transitions
  • Visibility

Fields of Study

  • Computer science

Readers

  • Computer Networking
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • Cyber