-
Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin
Authors:
Di Long Li,
Jim de Groot,
Alwen Tiu
Abstract:
Automated security protocol verifiers such as ProVerif and Tamarin have been increasingly applied to verify large scale complex real-world protocols. While their ability to automate difficult reasoning processes required to handle protocols at that scale is impressive, there remains a gap in the modeling languages used. In particular, providing support for writing and maintaining large protocol sp…
▽ More
Automated security protocol verifiers such as ProVerif and Tamarin have been increasingly applied to verify large scale complex real-world protocols. While their ability to automate difficult reasoning processes required to handle protocols at that scale is impressive, there remains a gap in the modeling languages used. In particular, providing support for writing and maintaining large protocol specifications. This work attempts to fill this gap by introducing a high-level protocol modeling language, called Tamgram, with a formal semantics that can be translated to the multiset rewriting semantics of Tamarin. Tamgram supports writing native Tamarin code directly, but also allows for easier structuring of large specifications through various high-level constructs, in particular those needed to manipulate states in protocols. We prove the soundness and the completeness of Tamgram with respect to the trace semantics of Tamarin, discuss different translation strategies, and identify an optimal strategy that yields performance comparable to manually coded Tamarin specifications. Finally we show the practicality of Tamgram with a set of small case studies and one large scale case study.
△ Less
Submitted 23 August, 2024;
originally announced August 2024.
-
Joint Channel Estimation and Equalization in Massive MIMO Using a Single Pilot Subcarrier
Authors:
Danilo Lelin Li,
Arman Farhang
Abstract:
The focus of this letter is on the reduction of the large pilot overhead in orthogonal frequency division multiplexing (OFDM) based massive multiple-input multiple-output (MIMO) systems. We propose a novel joint channel estimation and equalization technique that requires only one pilot subcarrier, reducing the pilot overhead by orders of magnitude. We take advantage of the coherent bandwidth spann…
▽ More
The focus of this letter is on the reduction of the large pilot overhead in orthogonal frequency division multiplexing (OFDM) based massive multiple-input multiple-output (MIMO) systems. We propose a novel joint channel estimation and equalization technique that requires only one pilot subcarrier, reducing the pilot overhead by orders of magnitude. We take advantage of the coherent bandwidth spanning over multiple subcarrier bands. This allows for a band of subcarriers to be equalized with the channel frequency response (CFR) at a single subcarrier. Subsequently, the detected data symbols are considered as virtual pilots, and their CFRs are updated without additional pilot overhead. Thereafter, the remaining channel estimation and equalization can be performed in a sliding manner. With this approach, we use multiple channel estimates to equalize the data at each subcarrier. This allows us to take advantage of frequency diversity and improve the detection performance. Finally, we corroborate the above claims through extensive numerical analysis, showing the superior performance of our proposed technique compared to conventional methods.
△ Less
Submitted 15 December, 2022;
originally announced December 2022.
-
OTFS Without CP in Massive MIMO: Breaking Doppler Limitations with TR-MRC and Windowing
Authors:
Danilo Lelin Li,
Arman Farhang
Abstract:
Orthogonal time frequency space (OTFS) modulation has recently emerged as an effective waveform to tackle the linear time-varying channels. In OTFS literature, approximately constant channel gains for every group of samples within each OTFS block are assumed. This leads to limitations for OTFS on the maximum Doppler frequency that it can tolerate. Additionally, presence of cyclic prefix (CP) in OT…
▽ More
Orthogonal time frequency space (OTFS) modulation has recently emerged as an effective waveform to tackle the linear time-varying channels. In OTFS literature, approximately constant channel gains for every group of samples within each OTFS block are assumed. This leads to limitations for OTFS on the maximum Doppler frequency that it can tolerate. Additionally, presence of cyclic prefix (CP) in OTFS signal limits the flexibility in adjusting its parameters to improve its robustness against channel time variations. Therefore, in this paper, we study the possibility of removing the CP overhead from OTFS and breaking its Doppler limitations through multiple antenna processing in the large antenna regime. We asymptotically analyze the performance of time-reversal maximum ratio combining (TR-MRC) for OTFS without CP. We show that doubly dispersive channel effects average out in the large antenna regime when the maximum Doppler shift is within OTFS limitations. However, for considerably large Doppler shifts exceeding OTFS limitations, a residual Doppler effect remains. Our asymptotic derivations reveal that this effect converges to scaling of the received symbols in delay dimension with the samples of a Bessel function that depends on the maximum Doppler shift. Hence, we propose a novel residual Doppler correction (RDC) windowing technique that can break the Doppler limitations of OTFS and lead to a performance close to that of the linear time-invariant channels. Finally, we confirm the validity of our claims through simulations.
△ Less
Submitted 14 January, 2022; v1 submitted 24 September, 2021;
originally announced September 2021.
-
Watershed of Artificial Intelligence: Human Intelligence, Machine Intelligence, and Biological Intelligence
Authors:
Li Weigang,
Liriam Enamoto,
Denise Leyi Li,
Geraldo Pereira Rocha Filho
Abstract:
This article reviews the "Once learning" mechanism that was proposed 23 years ago and the subsequent successes of "One-shot learning" in image classification and "You Only Look Once - YOLO" in objective detection. Analyzing the current development of Artificial Intelligence (AI), the proposal is that AI should be clearly divided into the following categories: Artificial Human Intelligence (AHI), A…
▽ More
This article reviews the "Once learning" mechanism that was proposed 23 years ago and the subsequent successes of "One-shot learning" in image classification and "You Only Look Once - YOLO" in objective detection. Analyzing the current development of Artificial Intelligence (AI), the proposal is that AI should be clearly divided into the following categories: Artificial Human Intelligence (AHI), Artificial Machine Intelligence (AMI), and Artificial Biological Intelligence (ABI), which will also be the main directions of theory and application development for AI. As a watershed for the branches of AI, some classification standards and methods are discussed: 1) Human-oriented, machine-oriented, and biological-oriented AI R&D; 2) Information input processed by Dimensionality-up or Dimensionality-reduction; 3) The use of one/few or large samples for knowledge learning.
△ Less
Submitted 7 May, 2021; v1 submitted 27 April, 2021;
originally announced April 2021.
